Fix Rocq dev compatibility and LibHyps logical mapping - #20
Draft
JasonGross wants to merge 5 commits into
Draft
Conversation
Rocq dev added a new `Constr.Unsafe.in_context` primitive with an extra
`constr option` argument (the optional let-binding body), keeping the
old three-argument `Constr.in_context` as an Ltac2-level wrapper.
`LibHypsNaming.v` does `Import Constr.Unsafe.`, so the unqualified
`in_context` now resolves to the new four-argument `Unsafe` version:
Error: This expression has type unit -> unit
but an expression was expected of type constr option
Qualify the three call sites as `Constr.in_context`, which names the
same function on Coq 8.x / Rocq 9.0-9.3 as well.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
map_all_hyps, map_all_hyps_rev and then_eachnh_gen all reach
Control.hyps via all_hyps_ident. Control.hyps is a single-goal
primitive and raises Init.Not_focussed whenever more than one goal is
under focus, so any script writing
1-4: onAllHyps (fun h => idtac h)
all: onAllHypsRev (fun h => idtac h)
fails. In 4.0 these tactics were pure Ltac1 and a range selector
dispatched them goal-wise automatically; 5.0 routes them through an
ltac2:() quotation, which evaluates in the multi-goal context instead.
Wrap each entry point in Control.enter, which reinstates the goal-wise
dispatch rather than choosing new semantics. then_eachnh_gen already
had an inner Control.enter, but it guarded only hyps_after -- hyps_before
was computed in the caller's context and hit the exception one line
earlier.
Verified against rocq-dev 9.4+alpha:
- five repros covering onAllHyps / onAllHypsRev / then_eachnh under
`1-4:` and `all:` fail before and pass after; the single-focused-goal
case passed both before and after, which is why this went unnoticed
- tests/ is unchanged: all 14 files give byte-identical exit codes
before and after (3 pass, 9 pre-existing `no Ltac named rename_depth`,
2 pre-existing timeouts). The 3 that pass are the ones exercising
onAllHyps -- demo.v, LibHypsTest.v, LibHypsRegression.v
- coq-matching-logic, which broke at Syntax.v:2968 on `1-3: wf_auto2`,
now builds 87/87 with `dune build -p coq-matching-logic` (rc=0),
matching what it reaches against LibHyps 4.0.0
Found by port-frozen's 4.0-vs-5.0 A/B.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
The two rocq-dev branches are complementary — one commit each off the shared Constr.in_context compat commit — so this PR now carries both: 0b5851b resources/coq_project.{libhyps,tests}: -R . LibHyps.LibHyps -> -R . LibHyps, so the modules install at user-contrib/LibHyps/*.vo as the released versions do rather than one level deeper at user-contrib/LibHyps/LibHyps/*.vo. a07b5cc map_all_hyps, map_all_hyps_rev and then_eachnh_gen all reach Control.hyps via all_hyps_ident. Control.hyps is a single-goal primitive and raises Init.Not_focussed under multi-goal focus, so `1-4: onAllHyps (...)` and `all: onAllHypsRev (...)` failed. In 4.0 these were pure Ltac1; 5.0 routes them through an ltac2:() quotation, which is what exposed it. Each entry point is now wrapped in Control.enter. The install depth in the first commit matters beyond tidiness: the coq-libhyps and rocq-libhyps opam packages install into overlapping prefixes, and the deeper layout made the two write disjoint path sets, so installing one left the other's recorded files absent from disk while opam still reported both installed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
The repo ships only rocq-libhyps.opam, so `opam pin add coq-libhyps
<this-repo>` finds nothing repo-local and silently falls back to the
package's *repository-cache* definition, keeping only the pin URL. On
every switch here that fallback is the pre-split standalone recipe
build: [ ["./configure.sh"] [make "-j%{jobs}%"] ]
install: [make "install"]
depends: [ "coq" {>= "8.11"} ]
which builds the tree a second time and installs its own copy of the
modules over the ones rocq-libhyps put there. After 0b5851b both
packages target user-contrib/LibHyps/, so this is now a direct
collision: opam lists both twins as installed while one of them has
none of its recorded files on disk. It is not a loadpath problem --
`logpath:` in tags: is documentation for the archive website and does
not affect where anything is written; the install prefix comes from
`-R . LibHyps` in resources/coq_project.libhyps.
Mirror the two archive rows so a pin of either name behaves the way the
archive does:
coq-libhyps.opam a pure wrapper -- no build:, no install:, one
dependency `"rocq-libhyps" { = version }`. It
installs nothing, so the collision cannot happen.
rocq-libhyps.opam gains `conflicts: [ "coq-libhyps" { != version } ]`,
which permits the matching wrapper and rejects any
real coq-libhyps, i.e. exactly the pairs that would
write the same paths.
Both files are copies of
extra-dev/packages/{coq,rocq}-libhyps/*.dev/opam at opam-coq-archive
master (56ed7c2), consistent with the header comment both files already
carry. Neither gets a `version:` field -- the archive rows supply the
version, and hard-coding "dev" here would break the released tags.
`opam lint` passes on both.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
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.
Supersedes #19. Commit 9574016, produced by a Claude coding agent, qualifies three Ltac2 calls as
Constr.in_context, fixing Rocq 9.4+alpha name resolution. Commit 0b5851b, produced by OpenAI Codex, changes the mapping fromLibHyps.LibHypstoLibHyps; with source fileLibHyps.v, the old mapping producedLibHyps.LibHyps.LibHypsinstead of the requiredLibHyps.LibHyps.Against
rocq-dev-testing,./configure.sh,make clean,./configure.sh, andmake -j8 allpass, as doROCQPATH=/data/jason/codex-libhyps dune clean --root matching-logicandROCQPATH=/data/jason/codex-libhyps dune build --root matching-logic src/wftactics.vo. This does not install into or mutate the opam switch.Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.
Wordsmithed by Codex.