[ rc ] Idris2 v0.7.0

[CodingCellist]

Description

RELEASE CANDIDATE! 👀
If I have followed the Release/CHECKLIST correctly (along with my own added details), this should hopefully build without any issue.

• Why 0.6.9 and not 0.7.0 ?
  • Because I am a child / For the memes Because I am not entirely sure that this will work. And if it doesn't, and we don't want the meme version (fair enough btw), then I can fix whatever went wrong thanks to the insights here, and 0.7.0 will emerge from the ashes as an actual release.

edit: Now it is v0.7.0 ! Much more appropriate ^^

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[CodingCellist]

Hmm. AFAICT, spec001 is failing because the machine names are different. Problem is, when I run it locally it passes without any issue; when going the bootstrap -> install -> self-host route...

[dunhamsteve]

I don't know why the names are different, but this recent change would be one way to work around it: 1aff26e

And RE the version number, maybe we can take the TeX approach and do: 0.69, 0.693, 0.6931, ...

[mattpolzin]

@CodingCellist perhaps you already noticed, but spec001 is broken already in the main branch, so not a result of what you're working on in this branch.

[mattpolzin]

I definitely would like to see the next version be 0.7.0. Less because the alternative is 0.6.9 and more because not bumping the middle number offends my delicate semver sensibilities (yes, I realize things are not strictly defined prior to 1.0.0, but I still take comfort in there being some sort of tangible difference between a minor and patch version bump).

I don't take issue with your idea to attempt an 0.6.9 release and if it succeeds then mark it as 0.7.0, aside from wondering if that isn't going to end up being more work than its worth (basically, will it be more work than just releasing and then retagging quickly before announcing anything if the release is broken).

[mattpolzin]

And thank you for taking on the release checklist and fleshing out less obvious details!

[mattpolzin]

A curious error in the pack tests: required base >= 0.5.1 but no matching version is installed. I wonder if it's possible that a bug in the version comparison logic considered 0.6.0 to be greater than or equal to 0.5.1 but not 0.6.9. Or otherwise if there is some other unobvious thing going on. I checked the logs and it installed base into the expected base-0.6.9 folder.

[stefan-hoeck]

A curious error in the pack tests: required base >= 0.5.1 but no matching version is installed. I wonder if it's possible that a bug in the version comparison logic considered 0.6.0 to be greater than or equal to 0.5.1 but not 0.6.9. Or otherwise if there is some other unobvious thing going on. I checked the logs and it installed base into the expected base-0.6.9 folder.

I'm quite sure this is because the compiler version is hard-coded in the HEAD.toml file of the pack collection. This is of course not ideal, and I'll have to think about how to fix this in the long run. I'm currently building the new compiler frow @CodingCellist 's fork locally. If all goes well, I suggest I adjust the pack collection as soon as this is merged and we ignore the failing pack test till then.

[stefan-hoeck]

I can confirm that what I described above is the issue at hand with the pack tests. This is the output of pack info on my machine now:

Package Collection  : nightly-231217
Idris2 URL          : https://github.com/CodingCellist/Idris2
Idris2 Version      : 0.6.9
Idris2 Commit       : c22eaaf92fce6590378b0c77e58ed236ad7fadd4
Scheme Executable   : chez
Pack Commit         : bb0cdc067da0d8be7922e7eb016c3fccd93059cb

So, the failing pack tests can be ignored. Once this is merged, I update the Idris version in the pack collection and we should get a nightly with the new compiler the next day.

[CodingCellist]

I definitely would like to see the next version be 0.7.0. Less because the alternative is 0.6.9 and more because not bumping the middle number offends my delicate semver sensibilities (yes, I realize things are not strictly defined prior to 1.0.0, but I still take comfort in there being some sort of tangible difference between a minor and patch version bump).

I don't take issue with your idea to attempt an 0.6.9 release and if it succeeds then mark it as 0.7.0, aside from wondering if that isn't going to end up being more work than its worth (basically, will it be more work than just releasing and then retagging quickly before announcing anything if the release is broken).

Any reason not to do a 0.6.9 is more than enough to not do it and just go with 0.7.0 ^^
I want to have fun with Idris as much as anyone, but we should probably still treat this as the serious research project it is, especially if there is a practical reason not to do a silly version ^^

[CodingCellist]

And sorry, I didn't notice main had already been merged until I tried to push locally. The merges went ahead without any issues, so hopefully nothing's been overwritten : )

[CodingCellist]

Okay! Everything seems good apart from the (afaiu anticipated) pack failures (@stefan-hoeck , would you mind verifying this?). I will leave it until noon UTC tomorrow (or roughly then) and then add the tag and complete the release if everyone's happy with that? : )
If anyone is off on holidays, please stay off on holiday. The release is not that urgent ^^

[buzden]

I will leave it until noon UTC tomorrow (or roughly then) and then add the tag and complete the release if everyone's happy with that?

I recently made couple of fixes which I think would be really nice to have before the release

[CodingCellist]

I will leave it until noon UTC tomorrow (or roughly then) and then add the tag and complete the release if everyone's happy with that?

I recently made couple of fixes which I think would be really nice to have before the release

#3166 is obviously one (I think), and I just merged #3169. Anything else? : )

[buzden]

#3166 is obviously one (I think), and I just merged #3169. Anything else? :)

This PR is also a worthing fix: #3165

[stefan-hoeck]

Okay! Everything seems good apart from the (afaiu anticipated) pack failures (@stefan-hoeck , would you mind verifying this?). I will leave it until noon UTC tomorrow (or roughly then) and then add the tag and complete the release if everyone's happy with that? : ) If anyone is off on holidays, please stay off on holiday. The release is not that urgent ^^

I can confirm that with HEAD.toml updated, pack builds fine with Idris 0.7.0, which is what I'm running on my system now! So yes, as soon as this is shipped, I'll update the pack collection.

[mattpolzin]

All referenced prerequisite PRs have been merged. Not rushing things, but we can carry on.

[mattpolzin]

And, come to think of it, the bootstrap code doesn't even need to be regenerated again, does it? I had confused myself a bit thinking we wanted to update that scheme code (which we did) but it'll build the Idris source just fine without e.g the bug fixes we just merged.

[CodingCellist]

I'm regenerating it anyways. Part of me would be slightly bothered if I didn't, have the release be as proper as can be, and I've got it all automated at this point ^^

[CodingCellist]

Right, that's the updated version, along with a tag (don't know if that'll apply on merging this PR; I hope it does, but we'll sort it if not). I'm going to go ahead and say that release is now just pending CI 🚀

[mattpolzin]

🙌

[CodingCellist]

And with that, it's done! 🙌

The tag didn't follow the PR (til) so I deleted the one on my fork and local repo, created the right one for the merged commit, and pushed that to upstream. Seems to have worked flawlessly : )

We still need to figure out how to update the website docs; I've created an issue so we don't lose track of that: #3173.

Thank you to everyone who made this possible and to the community in general for being helpful and supportive. Have fun and happy holidays! 🎆

[buzden]

As far as I can see, there were two forgotten steps for the release:

• Release the sources here: https://www.idris-lang.org/idris2-src/idris2-0.7.0.tgz
• Update IDRIS2_MINIMUM_COMPAT_VERSION in .github/workflows/ci-idris2-and-libs.yml

I tried to do post-release cleanup in #3174, and updated the variable in CI, after which I've found that the sources tarball was not published

[mattpolzin]

@buzden

The first step was not forgotten but rather we are not sure how to accomplish it. Either Edwin can upload the file or else we can switch the location over to a new page that GitHub or other maintainers can upload to.

The second step is not inherently part of a release. We intend to be able to build the Idris compiler with as early of a previous version as possible. We accept that it is currently worth bumping the minimum often so that we can make rapid progress on the compiler codebase itself, but this is not a given facet of every release. Instead, a separate PR post-release is welcome to bump the minimum and make its case for doing so.

[buzden]

The first step was not forgotten but rather we are not sure how to accomplish it. Either Edwin can upload the file or else we can switch the location over to a new page that GitHub or other maintainers can upload to.

Okay, I see now

The second step is not inherently part of a release. We intend to be able to build the Idris compiler with as early of a previous version as possible. We accept that it is currently worth bumping the minimum often so that we can make rapid progress on the compiler codebase itself, but this is not a given facet of every release. Instead, a separate PR post-release is welcome to bump the minimum and make its case for doing so.

Yeah, it means that, probably, post-release cleanup PR is a good place to bump this variable, as I tried to do. I agree that this seems to be the better place rather than in the release checklist.