-
Notifications
You must be signed in to change notification settings - Fork 367
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Release Agda 2.6.1 release candidate 1 #4212
Comments
Hi Jesper, please take a look at my latest comment at #4122 (comment) (maybe I should have opened a new issue for it). It makes using Prop much harder than it was before (and is a regression on master). |
Hi Jesper, see my summary on this issue: #2009 (comment). |
We should add to the list of critical issues the support of new versions in the tool-chain (GHC, cabal-install, stack, alex, happy, etc). I filed #4216. |
Should we have a label for classifying these issues perhaps? That would make it easier to tell which issues should definitely not be bumped. |
Why not #3855? Oh, because it is an enhancement. Well, I think it makes sense to document I removed the |
A new regression: #4253. (Instead of manually listing things to fix in this ticket, wouldn't it be better to change the milestones of the things that we do not plan to fix before the release?) |
I am planning to do this very soon, but as noted in the original post I wanted to give people the chance to pick up issues they want to see fixed before changing all milestones. Maybe it would make more sense to change all the milestones first and then change it back if necessary (something to think about for next release). |
Another new regression: #4254. |
Thank you to everyone for your hard work so far. I bumped all the remaining unassigned non-critical issues to 2.6.2 (except for a few that I assigned to myself). This leaves us with 40 remaining open issues, of which:
Let's continue the hard work so we can get our Christmas release of Agda! |
That code has presumably been released under the same licence as Agda. (At least that was my intention, I have not asked other contributors.) However, I am still sceptical towards moving |
Okay, thanks. Now I put it into the ice box, so I don’t have any open issue assigned to me for now. |
I need to catch up with all the recent changes to the CI as preparation for the release. I'll create the |
Travis is reporting the following error in the
Any idea what is wrong? |
My bad. Please remove the bar Line 190 in 29790fa
|
Done. Thanks! |
I added the list of current closed issues to the |
The CHANGELOG.md is way too big. I think it's good to split it (version-per-file or some-versions-per-file or something) |
@asr do you have a script for generating the "closed issues" section? |
I am trying to get a version of 2.6.1 compiling locally, so that I can test Just to get started: should I be using the |
It does not matter. Both routes are working. |
@JacquesCarette, |
Ok. I'll work on it systematically, in the hopes of being able to file reproducible bugs (in separate tickets). I'll have time this afternoon and tomorrow. |
@JacquesCarette, thanks for thinking on test |
I'll be without Internet access from 25th of December to January 1st. I think the I suggest to release the release candidate today. In this way, we could release a second release candidate or the final version in the first weeks of January. |
I'm in favour of bringing out a release candidate today! It will make for a nice Christmas present. |
I've found at least 2 regressions - will post some reports as soon as I've managed to make reasonably minimal examples. |
I'm starting the preparation of the release candidate from the current master (40034c5), so the |
I couldn't prepare the release candidate for 2.6.1 using |
@L-TChen I can definitely report that I was able to get going, with a minimum of fuss, with The good news is that I was able to apply a workaround to both regressions, so that agda-categories currently works with both 2.6.0.1 and 2.6.1 (and stdlib-1.2). |
* Removed `-Werror`. * Removed `-fprof-auto`. * Removed Cabal test-suite. * Added `doc/user-manual.pdf`.
I uploaded to Hackage the release candidate Agda-2.6.0.1.20191219 and I tested its installation on Ubuntu with
Could someone test the installation on macOS and Windows using the following instructions: $ cabal get https://hackage.haskell.org/package/Agda-2.6.0.1.20191219/candidate/Agda-2.6.0.1.20191219.tar.gz
$ cd Agda-2.6.0.1.20191219
$ cabal install |
The middle command should be
```
cd Agda-2.6.0.1.20191219
```
Installing gave me
```
$ cabal install
cabal: Unknown target '.'.
There is no component '.'.
The project has no package directory '.'.
```
Not sure what this is.
I am on MacOS X High Sierra,
```
[nix-shell:~/agda/Agda-2.6.0.1.20191219]$ cabal --version
cabal-install version 3.0.0.0
compiled using version 3.0.0.0 of the Cabal library
[nix-shell:~/agda/Agda-2.6.0.1.20191219]$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.6.5
```
When I try
```
$ cabal v2-install agda agda-mode --installdir=/Users/ggreif/.cabal/bin
Wrote tarball sdist to
/Users/ggreif/agda/dist-newstyle/sdist/Agda-2.6.1.tar.gz
Wrote tarball sdist to
/Users/ggreif/agda/dist-newstyle/sdist/fix-agda-whitespace-0.0.4.tar.gz
Resolving dependencies...
Up to date
Symlinking 'agda'
Symlinking 'agda-mode'
```
it seems like all build artefacts are already built... Strange.
When I do `cabal v2-build agda agda-mode` it starts to build. It chugs along...
And it succeeds building!
…On 12/20/19, Andrés Sicard-Ramírez ***@***.***> wrote:
I uploaded to Hackage the release candidate
[Agda-2.6.0.1.20191219](https://hackage.haskell.org/package/Agda-2.6.0.1.20191219/candidate)
and I tested its installation on Ubuntu with
[snip...]
|
Oops! Fixed. Thanks! |
I could reproduce the error by installing Please move |
Yep, that seems to work:
|
Thanks for testing. In your case I guess something like
should be enough. |
Could someone test the release candidate on Windows? |
I'll added the label |
I updated the list of other closed issues in the |
Done. Released the release candidate. |
The time for the next release is coming close. We will not make our (optimistic) 1 December deadline, but it would be nice if we could release 2.6.1 before Christmas (or at least have a RC).
To avoid the delays and crunch period we had with the release of 2.6.0, I want to propose a policy to decide which issues must be fixed and which ones can be bumped. Let's define a critical issue as one in the following categories:
regression on master
): Another regression related to piSort #3960, Regression related to abstract #4005, Performance regression #4040, Internal error with instance and variable #4149, The GHC backend generates code that is rejected by GHC #4169regression in 2.6.0
): Reduction missing during LHS checking #3054, Regression: Rewrite rule involving constructors rejected in parametrized module #3538, Solving blocked terms loses the user-written code #4067type: bug
andnot-in-changelog
): New pattern guards do not support case splitting #3995, Reflexive constraint involving erased projection not solved #4137, The GHC backend generates code that is rejected by GHC #4169, Restrict pattern matching for erased arguments of single-constructor data types #4172, Missing modality check in unifier leads to segfaults #4174, Modalities not set correctly for instantiated lhs variables #4195, Constructors can be marked as erased #4200All other issues I consider non-critical.
I would like to ask everyone who has at least one open issue with the 2.6.1 milestone (@UlfNorell @andreasabel @asr @gallais @Saizan @ice1000 @xekoukou @L-TChen @hborum @mortberg @fredrikNordvallForsberg @Blaisorblade) to go over the list of 2.6.1 issues (https://github.com/agda/agda/issues?q=is%3Aopen+is%3Aissue+milestone%3A2.6.1) assigned to you and do the following:
If you have the time, it would also be greatly appreciated if you could do a pass over the unassigned issues with 2.6.1 milestone (https://github.com/agda/agda/issues?q=is%3Aopen+is%3Aissue+milestone%3A2.6.1+no%3Aassignee) to decide if there are any you want to see fixed, and either assign yourself or post a comment asking if someone else can take it.
To avoid delays, please try to do these things before December the 1st. After that, I will start mercilessly bumping non-critical issues with no owner to 2.6.2.
Also please let me know if there are other categories of critical issues that I have missed, or if you have other comments about this proposed policy.
The text was updated successfully, but these errors were encountered: