Repository navigation
Migrate the proofs to Rocq 9.2; keep the published Coq 8.20.1 version in coq-legacy/ - #1
Merged
Merged
Conversation
… verbatim in coq-legacy/ - coq-legacy/: the Coq 8.20.1 development exactly as published (tree identical to main:coq), checked by check-legacy.sh / Dockerfile.legacy in the same digest-pinned coqorg/coq:8.20.1 image. - coq/: the Rocq 9.2 version. Changes are imports only (From Coq -> From Stdlib, Coq.* -> Stdlib.* paths); no definition, statement or proof changed. - check.sh / Dockerfile: rocq makefile, rocqchk, rocq c; rocq/rocq-prover:9.2 pinned by digest. - CI: two jobs, the Rocq check and the legacy Coq check. - README: section on the migration and the legacy version. Both checks pass locally: rocqchk and coqchk each report no axioms, no type-in-type, no unsafe fixpoints, no assumed positivity. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019VctApPTf4Vkbc7JRkGiXb
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What changes
coq-legacy/: the Coq 8.20.1 development exactly as published. Its git tree is identical tomain:coq. It keeps its own one-command check,docker build -f Dockerfile.legacy ., which runscheck-legacy.shin the same digest-pinnedcoqorg/coq:8.20.1image as before.coq/: the same development on Rocq 9.2. The changes are imports only:From Coq Require ...becomesFrom Stdlib Require ...;Coq.*stdlib paths becomeStdlib.*.No definition, lemma, theorem statement or proof changed.
check.sh/Dockerfile:rocq makefile,rocqchk,rocq c;rocq/rocq-prover:9.2, pinned by digest;CI: two jobs,
rocqchk(Rocq) andcoqchk-legacy(Coq 8.20.1).README: a section on the migration and the legacy version.
Verification (local)
docker build .(Rocq 9.2):OK: all checks passed,Axioms: <none>, no type-in-type, no unsafe fixpoints, no assumed positivity.docker build -f Dockerfile.legacy .(Coq 8.20.1):OK: all checks passed, with the same coqchk summary.diff -r coq-legacy coq: every differing line is an import line.🤖 Generated with Claude Code
https://claude.ai/code/session_019VctApPTf4Vkbc7JRkGiXb
Generated by Claude Code