release 1.7.3 #2132
release 1.7.3 #2132
Conversation
To fix agda/agda#6654, we've decided that large indices will no longer be allowed by default. There is an infective flag `--large-indices` to bring them back, but none of the uses of large indices in the standard library were essential: to avoid complicated mutually-recursive PRs across repos, I adjusted the levels to check with `--no-large-indices` instead of adding the flag to the modules that used them.
andreasabel
force-pushed
the
release-1.7.3
branch
from
b34652b
to
3bdb4ef
Compare
Also: - install alex and happy - bump Agda heap to -M6G
andreasabel
force-pushed
the
release-1.7.3
branch
from
3bdb4ef
to
3f869a3
Compare
There was a problem hiding this comment.
Thanks for getting this off the ground!
Get CI to run: CI runs at https://github.com/andreasabel/agda-stdlib/actions
I'm afraid my expertise at CI wrangling pales in comparison to yours so I'm maybe you have better ideas why its failing than me? I have to confess I've never dug deeply into the CI code myself.
Implement missing points described in the release guide
Happy to do this once we have the content thrashed out.
Consider additions for forward-compatibility with v2.0: #2129 (comment)
Could you make a separate PR onto this branch with your proposed changes?
CHANGELOG/ is missing changelogs for v1.7 and v1.7.1
Hmm so they're present on master. Not quite sure why they never made it to this branch. I'll copy them from there.
| if [[ '${{ github.ref }}' == 'refs/heads/master' \ | ||
| || '${{ github.ref }}' == 'refs/heads/experimental' ]]; then | ||
| echo "AGDA_DEPLOY=true" >> $GITHUB_ENV | ||
| fi |
There was a problem hiding this comment.
So I imagine that we'd be merging this branch back into master at some point. While a lot of the changes to this CI file are enhancements (e.g. bumping versions), can we avoid removing functionality like this?
In particular it's important that if we're on the experimental branch, we install a different version of Agda!
There was a problem hiding this comment.
Oh, apologies, I didn't know this would be merged back into master.
What are the reasons for merging it in there?
master already contains the relevant patch to remove the use of large indices (I cherry-picked it from there).
E.g. for the release of Agda-2.6.4, I am not merging the release branch back in. It only contains changes that are relevant for the release. The tag v2.6.4 will sit on some leaf three commits away from the trunk. Is there a problem with this approach I have chosen?
There was a problem hiding this comment.
Well on principle, I don't think we should be making any changes that we don't want to merge back across. Furthermore you're making various improvements to the CI for example right? Bumping versions etc. it would nice if those were added back across. I guess we can cherry-pick them...
There was a problem hiding this comment.
The versions are already bumped in master, the last CI bumps are in:
| @@ -6,79 +6,144 @@ | |||
| # | |||
| # haskell-ci regenerate | |||
| # | |||
| # For more information, see https://github.com/haskell-CI/haskell-ci | |||
| # For more information, see https://github.com/andreasabel/haskell-ci | |||
There was a problem hiding this comment.
Could you explain why we're switching to your own fork? Have to confess I'm a bit reluctant to, unless strictly necessarily. If it necessary, then documentation as to the reason should be added here.
There was a problem hiding this comment.
My fork uses the ubuntu-20.04 image rather than the ubuntu-18.04 image which allows it to use the latest version of action/checkout. Otherwise, it is interchangeable, and you could as well regenerate the CI with the original haskell-ci.
There was a problem hiding this comment.
And why do we need the latest version of action/checkout?
There was a problem hiding this comment.
Not needed.
But you might get harassed by dependabot if you don't use it...
If it matters to you, I can install the original haskell-ci and recreate this workflow. But this is anyway just customary CI for 1.7.3 which won't end up in master.
There was a problem hiding this comment.
Yes, I guess that's my real question! Why are we trying to make a custom CI pass for v1.7.3?
There was a problem hiding this comment.
I don't want to release without having run CI. But I now I am passing the bucket to you, so I make #2141 without CI changes.
Actually I'm a bit confused about the setup for this whole PR. When I try to checkout |
What do you get with |
…-1.7.3-base Restricting to branch release-1.7.3-base will hopefully stop duplicate CI runs.
bump to 1.7.3 in - standard-library.agda-lib - README.agda - installation-guide.txt
andreasabel
force-pushed
the
release-1.7.3
branch
from
38bd240
to
8c753ad
Compare
andreasabel
force-pushed
the
release-1.7.3
branch
from
8c753ad
to
3d2002b
Compare
Unfortunately I don't have |
|
@andreasabel would you be free to briefly join the standard library dev ((https://meet.google.com/trh-fpbj-kfi)) meeting at https://time.is/1200_12_Oct_2023_in_UTC today? |
Yes, thanks for the invitation! I will join, but have only like 50min because of another meeting. |
Some objects will get a new name in v2.0. We add some of these names already here to ease the transition to v2.0: - add modules `Effect.*` reexporting `Category.*` - add `IO.Primitive.pure` as alias for `IO.Primitive.return`
|
I added a commit with aliases for forward compatibility as proposed by @jamesmckinna in: @MatthewDaggitt: I'll make a new PR that does not touch CI. |
|
Superseded by #2141 which does not make an attempt at running it through CI. |
Branched off tag
v1.7.2(branchrelease-1.7.3-base) to gather commits forv1.7.3.TODO:
* CI runs at https://github.com/andreasabel/agda-stdlib/actions
* Deploys to: https://andreasabel.github.io/agda-stdlib/v1.7.3/
v2.0: 1.7.2 errors with Agda 2.6.4 #2129 (comment)CHANGELOG/is missing changelogs forv1.7andv1.7.1Commits:
--large-indices(Put indexed data types in the right universes #2030)