Release Agda 2.5.1.2

[UlfNorell]

The commit abcde44 fixes compilation with ghc-8.0.2. We should cherry-pick this to release-2.5.1 and release 2.5.1.2.

[ilovezfs]

Yes please. Also the constraint on alex needs to be bumped.

[UlfNorell]

Are you referring to this commit: 5f98517?

[ilovezfs]

Yup. Otherwise (without additional interventions), we get

setup: The program 'alex' version >=3.1.0 && <3.2 is required but the version
found at
/private/tmp/agda-20161122-14873-dnjh8g/agda-2.5.1.1/.cabal-sandbox/bin/alex
is version 3.2.1

[UlfNorell]

Cherry-picked abcde44 and 5f98517. Waiting for Travis.

[gallais]

Shouldn't we be blocking on #2225? The current agda.sty leads to building pdfs with a lot of missing characters. Which also begs the question: should travis grep for missing characters when checking that TeX files produced by the backend build correctly?

[UlfNorell]

This is a critical bug fix release on top of 2.5.1.1. It doesn't contain anything from current stable other than the two patches I mentioned above. Are you saying LaTeX generation is broken on 2.5.1.1?

[ilovezfs]

https://gist.github.com/ilovezfs/2df4fc2d2d4cc4c33252397314fd501a

[ilovezfs]

That is with GHC 8.0.1.20161114, which is nearly the same as 8.0.2, so LGTM.

[gallais]

The generated LaTeX itself is fine but the agda.sty interacts badly with recent versions of texlive which means the pdf generated by xelatex is missing a lot of unicode characters (λ, ℕ, and ℤ for instance). At least that's my current understanding of the issue.

[ilovezfs]

@gallais did #2225 (comment) turn out to make it work as expected?

[gallais]

It works for me (haven't tested it with lualatex) except that the code is now using a serif font which is arguably ugly. Ideally we would probably want a sans serif by default and a fallback (e.g. XITS) for unicode symbols.

[UlfNorell]

I'd rather hold off on #2225 since it sounds like there are still some questions about how to fix it. If you have a commit that you are certain isn't breaking anything I'd be happy to throw it in there.

[asr]

Various issues were fixed and new features were added in the current stable-2.5 (see release notes for 2.5.2).

On the other hand, there are six open regressions. Why not try to fix these regressions and make a full release supporting GHC 8.0.2?

[ilovezfs]

@asr they're not mutually exclusive. This should ship as-is IMO.

[asr]

they're not mutually exclusive.

Right, but keep in mind the time needed for making a release. In addition, for releasing 2.5.1.2 we need to merge the fix to #2121. Otherwise Agda 2.5.1.2 would not be part of Stackage.

[ilovezfs]

keep in mind the time needed for making a release.

from brew perspective a simple github tag will do the trick, but I hear you.

[UlfNorell]

If merging #2121 is too much work, wouldn't it be better to release a non-stackage 2.5.1.2 than not releasing at all?

The work on the 2.5.2 release is progressing, but the time frame for that is "before the holidays", and it'd be nice if we could get 2.5.1.2 out quicker.

[asr]

The work on the 2.5.2 release is progressing, but the time frame for that is "before the holidays", and it'd be nice if we could get 2.5.1.2 out quicker.

In any case, we need to wait the release of GHC 8.0.2...

[ilovezfs]

In any case, we need to wait the release of GHC 8.0.2

8.0.2-rc1 bindist is already out, and agda is dead in the water without these patches.

[asr]

8.0.2-rc1 bindist is already out

Really? I haven't seen any announce. I just asked Ben Gamari about it. I know there is tarball, though.

[UlfNorell]

The 2.5.2 release should wait for ghc-8.0.2 (unless it gets pushed back a lot), but 2.5.1.2 should go out asap.

[asr]

but 2.5.1.2 should go out asap.

Really? You want to release 2.5.1.2 because there is a commit fixing the compilation with GHC 8.0.2, but you don't see to necessary to wait the release of GHC 8.0.2 for realising 2.5.1.2. I don't follow you.

[UlfNorell]

8.0.2 fixes a bug which let completely incorrect type signatures through the type checker. Some of those signatures we had in Agda. It makes sense to push out a release with those types fixed as soon as possible. Without the #2121 fix it's just two patches so making release isn't much work. I'll do it if you feel you don't have the time.

[asr]

8.0.2 fixes a bug...

Which 8.0.2? This is my point.

[UlfNorell]

What do you mean? Are you worried that there will be last minute changes to 8.0.2 that breaks compilation in a different way?

[asr]

Are you worried that there will be last minute changes to 8.0.2 that breaks compilation in a different way?

Yes, but I wouldn't talk of "last minute changes". How many release candidates for 8.0.2 there will be? Nobody knows. Has the GHC Team enough feedback from 8.0.2 RC1? No, because this RC hasn't announced. (Ben Gamari told me the announce of 8.0.2 RC1 will be in a week or so).

[asr]

Ben Gamari told me the announce of 8.0.2 RC1 will be in a week or so.

N.B. I'm not talking about 8.0.2 but 8.0.2 RC1.

[UlfNorell]

8.0.2 is a bug fix release. They don't usually break things. Anyway, I don't see the problem with having more releases of Agda. We've spent more time talking in this thread than it would take to finish up the release notes and push 2.5.1.2 to Hackage.

[asr]

I disagree in making a release without testing 8.0.2 (and without supporting Stackage). I guess you will make the release anyway, so please remember:

• Test the release in Windows, Mac OS and Linux
• Keep in mind Travis is not testing 8.0.2 RC1

We've spent more time talking in this thread than it would take to finish up the release notes

Right because we haven't anything to add in the release notes :-)

[UlfNorell]

Released

[asr]

I'm updating the wiki...

[asr]

I couldn't find a tarball for 2.5.1.2 in the releases list.

[asr]

@UlfNorell did you tag the release? Did you forget to push the tag?

[UlfNorell]

Forgot to push the tag. Fixed now.

[asr]

I'm updating the wiki...

Done.

[ilovezfs]

@UlfNorell thanks. Upgrade now shipped on Homebrew: Homebrew/homebrew-core#7233