Coq Platform and opam version lags

[mikeshulman]

I'm working with a student who installed the library according to the recommended method with Coq Platform, and then was very confused to discover that not all the definitions he saw in the library source code on GitHub were available. Perhaps it would be a good idea to add a warning to the installation instructions that the Coq Platform version is not the most recent one?

Also, is it still true that there's a development version of the library available in opam? We tried adding the coq-extra-dev opam repository but then opam install coq-hott installed the 8.13.dev version which looks older than the 8.19 version available in coq-released.

[Alizter]

The coq-extra-dev channel hasn't been updated for a while. If you want to use the latest version, then the recommended method would be to do opam install . in the cloned HoTT repo. I will update the README.md and INSTALL.md to mention this.

I will also mention that the Coq Platform is released at each major Coq version (so biyearly). This means that there will be some delay between master and the platform.

[SkySkimmer]

coq-hott.dev in extra-dev requires coq.dev, so it won't get installed when you have a released Coq.

I'm working with a student who installed the library according to the recommended method with Coq Platform, and then was very confused to discover that not all the definitions he saw in the library source code on GitHub were available.

That sounds normal, >99% of the time the released version of software is behind the repository since not every commit causes a new release.

[mikeshulman]

But I think it's natural to have somewhat different expectations from a library of formal proofs as from "software".

[Alizter]

Now that #2047 has been merged, do we consider this issue resolved?

[mikeshulman]

Fine with me.