Coq 8.5

[spitters]

We should move to the stable version.
I haven't looked at it yet, but this is a reminder that we should.

[JasonGross]

Yes, I agree.

I've ported everything that builds before HoTT.Modalities.ReflectiveSubuniverse at this branch. @mikeshulman, could you take a look at ReflectiveSubuniverse and figure out how to deal with universe annotations? All definitions that use universe annotations now need to declare them at definition time (Definition foo@{a b} (A : Type@{a}) := Type@{b}.). The definition inO_sigma_from_O_ind seems to gain two universes not mentioned in its type in the course of its proof, and I haven't figured out where these universes come from / what to name them / where to specify them. (Most of the non-universe-declaration changes involve replacing refine with simple refine.)

I also have to track down some changes in timing, but I'd appreciate help with fixing the universes in the modalities bits.

[JasonGross]

I've fixed inO_sigma_from_O_ind; the biggest issue was the fact that f o g sometimes introduces new (and unnecessary) universes that fun x => f (g x) does not, if f or g have domain or codomain Type. Now I'm stuck on O_ind_from_inO_sigma, which seems to have somehow picked up a universe that does not show up in Set Printing All. Set Printing Universes.! @mattam82 @mikeshulman any ideas?

Also, @mattam82, there seems to be a minor bug in the universe minimization algorithm, where the universes displayed by Set Printing Universes. Show Proof. change when you execute - (a bullet). Is this expected? (There's another minor bug where sometimes unnamed universes (Top.nnnnn) are displayed in preference to named universes, when they are equated.)

[mikeshulman]

Unfortunately, I'm kind of swamped right now; it may be several weeks before I have a chance to look at this.

[JasonGross]

I've discovered Local Unset Strict Universe Declaration., which should take care of most of the things I can't figure out for now.

[JasonGross]

I now have a branch that compiles with 8.5 released, and the main remaining performance bug is Algebras/ooGroup, which is 25x slower. (I think it has something to do with rewrite and keyed unification; I'm currently minimizing it.)

[JasonGross]

Minimized and reported: bug 4544; Keyed Unification got more complete in 8.5 (it now finds some things it should have found but was not finding), but it also seems to do way too much work in some cases (unfolding things it should not). (@mattam82)

[JasonGross]

I have a version that's about on-par with 8.5beta2, but requires unsetting keyed unification in ooGroup.v. The timing diff (8.5beta2 -> 8.5 (coq/coq@22a2cc, which is a bit after the released version)):

After    | File Name                                                 | Before   || Change   
--------------------------------------------------------------------------------------------
3m43.21s | Total                                                     | 3m35.47s || +0m07.74s
--------------------------------------------------------------------------------------------
0m06.57s | categories/Adjoint/Pointwise                              | 0m24.01s || -0m17.44s
0m15.44s | hit/V                                                     | 0m11.04s || +0m04.40s
0m10.74s | Algebra/ooGroup                                           | 0m06.72s || +0m04.02s
0m06.47s | Spaces/BAut                                               | 0m02.41s || +0m04.05s
0m04.71s | contrib/HoTTBook                                          | 0m01.22s || +0m03.49s
0m14.21s | Spaces/BAut/Bool                                          | 0m11.50s || +0m02.71s
0m13.90s | categories/Category/Sigma/Univalent                       | 0m11.02s || +0m02.88s
0m07.13s | Spaces/No                                                 | 0m05.20s || +0m01.92s
0m06.90s | Spaces/Finite                                             | 0m05.67s || +0m01.23s
0m03.32s | hit/FreeIntQuotient                                       | 0m01.93s || +0m01.38s
0m02.35s | Spaces/BAut/Cantor                                        | 0m01.23s || +0m01.12s

[peterlefanulumsdaine]

Am I right in understanding that the only problem now with this is the need to locally unset keyed unification in ooGroup.v? If so, is that big enough to justify blocking the update to 8.5?

[JasonGross]

I believe all released versions of Coq after 8.5 beta 2 take three times as
long to compile HoTT, no matter what we do. I was planning on waiting for
8.5pl1, which will fix this problem. Alternate solutions include pinning
to the current v8.5 tip, or pinning to the current v8.5 tip and having
Travis enforce compatibility with released 8.5.

[mikeshulman]

Does 8.7pl1 have an ETA?

[peterlefanulumsdaine]

Ah, right — I’d missed the fact that your latest (non-slow) version was over the tip not over the 8.5 release itself. Yes, then I’m fine with waiting for 8.5pl1 — I have nothing urgent that need 8.5.

[spitters]

@matej-kosik asks whether we want HoTT as a contrib. I think we decided a while ago that we do.
Now that 8.5pl1 is out, are there any more obstacles (apart from actually updating to 8.5pl1?)

[JasonGross]

I don't know of any obstacles, and once #800 is merged, we'll work with 8.5pl1.

[andrejbauer]

Do contribs presume that the standard library is loaded?

[ghost]

I believe that it would be possible to have a coq-contrib that passes "-nois" parameter to coqc.

If all goes well, coq-contribs will be published as OPAM packages so maybe HoTT project can go in the same direction. In other words, I am not sure if I understand the motivation for adding HoTT to coq-contribs.

(I am not against it, I just do not understand why you might want to do that. Some of the responsibilities that coq-contribs had were acquired by OPAM platform which is more popular than coq-contribs).

[spitters]

I am aware of the discussion among the coqdevs about coq-contrib vs opam, but I have not seen a clear conclusion. What, I think, we would like is HoTT to be available for regression testing for the coq-developers. It's a mature library which is somewhat non-standard. So, it seems perfect for that.
It the same time, it is a library we are proud of and like to display on coq-contrib.
(I believe those are the two main use cases for coq-contrib).

HoTT is already in opam, but there is also some nice work by @ejgallego on loosening the connection of coq with std-lib. It should facilitate things in the future.
https://github.com/ejgallego/coq/tree/coqlib-cleanup

[ejgallego]

There was some discussion about solving the stdlib issue in the last Coq Working Group, but IMO it is not going to be ready for 8.6.

jsCoq ships HoTT is by using an overlay over the stdlib, this works well and indeed should be feasible to do for 8.6.

@matej-kosik note that indeed -nois may not be enough. As you can see in the cleanup patch, some parts of Coq indeed require an available stdlib.

[JasonGross]

We're now on 8.5pl1 (#800).