Tracker issue for 8.17 package tag creation

[MSoegtropIMC]

This issue exists to track the issues on the package upstream repos to create tags for Coq 8.17.

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/172
• https://gitlab.inria.fr/coquelicot/coquelicot/-/issues/7
• https://gitlab.inria.fr/flocq/flocq/-/issues/22
• https://gitlab.inria.fr/coqinterval/interval/-/issues/13
• https://gitlab.inria.fr/gappa/coq/-/issues/12
• https://gitlab.inria.fr/fpottier/menhir/-/issues/69
• https://gitlab.inria.fr/fbesson/itauto/-/issues/30
• https://gitlab.mpi-sws.org/iris/iris/-/issues/516

Updates to be done

• Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HoTT/Coq-HoTT#1727
• Coq 8.17.0 + remove opam dev repo
• E-prover 3.0 (postponed since there is no official release as yet)

Local opam packages to be removed

• coq-metacoq.1~preview+8.17 and sub packages
• coq-vst-32.2.12

Local opam packages to be merged upstream

• gappa.1.4.1 Added new version 1.4.1 for 'gappa' ocaml/opam-repository#23433
• z3_tptp.4.11.2 Add new version 4.11.2 for the TPTP front end for Z3 ocaml/opam-repository#23434
• KEEP-LOCAL (won't be merged upstream) ocamlfind relocation patch Patch to make ocamlfind relocatable (via a binary installer on macOS, Windows, Snap) ocaml/ocamlfind#60
• coq-coqprime Fix coq version restriction for coq-coqprime.1.2.0 opam#2496
• coq-compcert-32 coq-compcert-32: fix coq version restriction + editorial changes opam#2493 (comment)
• coq-math-classes Add new version 8.17.0 for coq-math-classes opam#2506
• coq-hott coq-hott.8.16: relax Coq version restriction to allow 8.17 opam#2508
• KEEP-LOCAL (missing in MinGW repo ) elpi
• coq-mathcomp-word Added new version 2.1 for coq-mathcomp-word opam#2509
• coq-reglang allow Coq 8.17 and MathComp 1.16.0 for coq-reglang.1.1.3 opam#2510 (comment)
• coq-unimath Create new version 20230321 for coq-unimath opam#2537
• coq-unicoq Create new version 1.6+8.17 for coq-unicoq opam#2538
• coq-mtac2 Create new version 1.4+8.17 for coq-mtac2 opam#2539
• coq-record-update Add bew version 0.3.2 for coq-record-update opam#2541
• fiat-crypto & dependencies Update fiat-crypto and dependencies with new versions opam#2540

Issues to be fixed

• Replace smoke test file for fingroup with mathcomp/fingroup/quotient.v Attend warning deprecated-hint-rewrite-without-locality math-comp/math-comp#892 (comment)
• CI: Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2, actions/upload-artifact@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/. (delayed, creates issue)
• Add path length check on root path on Windows (for serapi). (delayed, creates issue)

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)

[ejgallego]

Closing as this seems completed.