Open
Description
This issue exists to track the issues on the package upstream repos to create tags for Coq 8.20.
This ticket is referenced in all package issues.
Discussions should take place in the individual upstream issues.
ToDo:
Issue links to non github projects
- https://gitlab.mpi-sws.org/iris/stdpp/-/issues/226
- https://gitlab.inria.fr/coquelicot/coquelicot/-/issues/11
- https://gitlab.inria.fr/flocq/flocq/-/issues/25
- https://gitlab.inria.fr/coqinterval/interval/-/issues/17
- https://gitlab.inria.fr/gappa/coq/-/issues/15
- https://gitlab.inria.fr/gappa/gappa/-/issues/17
- https://gitlab.inria.fr/fpottier/menhir/-/issues/76
- https://gitlab.inria.fr/fbesson/itauto/-/issues/36
- https://gitlab.mpi-sws.org/iris/iris/-/issues/583
Updates to be done
- Elpi 2.X
- EProver 3.2 (private communication with Stephan Schulz) (note done, too late)
- Update VST and CompCert (A COmpCert update is released, waiting for VST)
- Double check coq-coqprime-generator - the opam package looks wrong
- Update Coq to 8.20.1
Local opam packages to be removed
- coq-unimath.20240923
- coq-corn.8.20.0
- coq-coqprime-generator.1.1.2
Local opam packages to be merged upstream
Issues to be fixed
Checklist
- Update release in documentation
- Add new picks to documentation
- Update auto generated documentation
- Ensure that release builds for MacOS, Snap and Windows include large packages
- Ensure Mac installers work for older MacOS (by inspecting otool dump)