port patch from AutoRocq (77d335c..2079f15): drop pre-9.0 Rocq compat - #10
Draft
dingf3ng wants to merge 1 commit into
Draft
port patch from AutoRocq (77d335c..2079f15): drop pre-9.0 Rocq compat#10dingf3ng wants to merge 1 commit into
dingf3ng wants to merge 1 commit into
Conversation
LemmaNet's proof-search/{coqpyt,backend/coq_interface.py,...} still
mirror AutoRocq at 77d335c (PR#3) 1:1 for everything that isn't the
lemma-discovery add-on. AutoRocq has since moved to Rocq 9.0.0 and
dropped pre-9.0 compatibility (e9cdbb0 "add support to rocq 9.0",
2079f15 "fix tests; update readme"). Port that patch onto this
mirror so it stays a pure superset of AutoRocq's own interface,
rather than layering it onto LemmaNet's later multi-backend
refactor (see sync-autorocq-rocq-wired for that variant).
Applied AutoRocq's diff directly wherever LemmaNet's file was
byte-identical to the pre-image (coqpyt/*, proof-search/tests/*,
proof-search/coqpyt/tests/*, deps.opam, run_tests.py removal); hand
merged the handful of files LemmaNet had already diverged on
(README, dockerfile, context_manager.py's coq_version, coq_utils.py's
import detection, and the worked example .v files, where only the
`From Coq`/`Coq.` import headers move to `From Stdlib`/`Stdlib.`,
proof bodies untouched). Bumped the AutoRocq-bench submodule to the
commit AutoRocq itself now pins.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
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
1 participant
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.
LemmaNet's proof-search/{coqpyt,backend/coq_interface.py,...} still mirror AutoRocq at 77d335c (PR#3) 1:1 for everything that isn't the lemma-discovery add-on. AutoRocq has since moved to Rocq 9.0.0 and dropped pre-9.0 compatibility (e9cdbb0 "add support to rocq 9.0", 2079f15 "fix tests; update readme"). Port that patch onto this mirror so it stays a pure superset of AutoRocq's own interface, rather than layering it onto LemmaNet's later multi-backend refactor (see sync-autorocq-rocq-wired for that variant).
Applied AutoRocq's diff directly wherever LemmaNet's file was byte-identical to the pre-image (coqpyt/, proof-search/tests/, proof-search/coqpyt/tests/*, deps.opam, run_tests.py removal); hand merged the handful of files LemmaNet had already diverged on (README, dockerfile, context_manager.py's coq_version, coq_utils.py's import detection, and the worked example .v files, where only the
From Coq/Coq.import headers move toFrom Stdlib/Stdlib., proof bodies untouched). Bumped the AutoRocq-bench submodule to the commit AutoRocq itself now pins.