Skip to content

Keep track of which variables are section variables and use this info to fix bugs - #21987

Merged
coqbot-app[bot] merged 17 commits into
rocq-prover:masterfrom
SkySkimmer:context-secvar
Jun 1, 2026
Merged

Keep track of which variables are section variables and use this info to fix bugs#21987
coqbot-app[bot] merged 17 commits into
rocq-prover:masterfrom
SkySkimmer:context-secvar

Conversation

@SkySkimmer

@SkySkimmer SkySkimmer commented Apr 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Named declarations now contain an extra field status = SecVar | ProofVar. SecVar means it is a section variable.

To work this requires the invariant that if a variable is marked SecVar in an evar's context then that evar is always instantiated with that section variable.

Fix #18858
Fix #12304
Fix #11487
Fix #6773

Overlays (.v):

Overlays (.v, not backwards compatible)

Overlays (.ml):

Overlays not needed now that clear warns instead of error on unbound variable:

@SkySkimmer
SkySkimmer requested review from a team as code owners April 30, 2026 15:17
@SkySkimmer SkySkimmer added the needs: merge of dependency This PR depends on another PR being merged first. label Apr 30, 2026
@SkySkimmer
SkySkimmer requested review from a team as code owners April 30, 2026 15:17
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026
@SkySkimmer
SkySkimmer requested review from a team as code owners April 30, 2026 15:17
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026
@SkySkimmer
SkySkimmer requested a review from a team as a code owner April 30, 2026 15:49
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026
@SkySkimmer

SkySkimmer commented Apr 30, 2026

Copy link
Copy Markdown
Contributor Author

hott failure is because they workaround #18858 by explcitly clearing

@SkySkimmer

SkySkimmer commented Apr 30, 2026

Copy link
Copy Markdown
Contributor Author

@coqbot ci minimize ci-stdlib

@SkySkimmer SkySkimmer mentioned this pull request May 22, 2026
Open
@SkySkimmer

SkySkimmer commented May 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

https://github.com/math-comp/odd-order/blob/6afa795b9018c64ab5c7cd2f9b3c9ab5dd45d93f/theories/PFsection3.v#L1119 uexact Db21 is failing with "No such hypothesis: IH." (from the new check in Tactics.clear)
uexact is Tactic Notation "uexact" constr(IH) := apply: unsat_exact IH; exact isT. which is where the IH name comes from.
It seems like some code is failing to substitute ltac variables?

minimized:

Require Import ssreflect.

Axiom f : True -> False -> nat.

Tactic Notation "uexact" constr(IH) := apply: id IH; exact I.

Goal True -> nat.
Proof.
  intros x.
  uexact x.

@gares any ideas?

@gares

gares commented May 22, 2026

Copy link
Copy Markdown
Member

I think that it is possible that some SSR code does not substitute ltac variables correctly.
Also, apply: does some hacks to inject econstrs into constr_expr by injecting them in the ltac environment, IIRC.

@SkySkimmer

SkySkimmer commented May 23, 2026

Copy link
Copy Markdown
Contributor Author

Can be turned into a bug on master #22057

@SkySkimmer

SkySkimmer commented May 26, 2026

Copy link
Copy Markdown
Contributor Author

Rocq call: seems like the right direction

@gares

gares commented May 27, 2026

Copy link
Copy Markdown
Member

I've updated the elpi overlay.
@coqbot run full ci

SkySkimmer added 16 commits May 28, 2026 12:55
@SkySkimmer
Keep track of variable status (secvar or not) in named contexts
980c7ea 
Close rocq-prover#6773
@SkySkimmer
check_hyps_inclusion use variable status instead of conversion
45e9c60 
This lets us detect if a variable is some unrelated variable which got
renamed to the name of a previously cleared section variable.

It's also cheaper than conversion but that's not really the point of
this patch.

Fix rocq-prover#11487
@SkySkimmer
Error instead of renaming section variable mentioned through a global
0c35e6b 
Fix rocq-prover#12304
@SkySkimmer
Tactics.clear handle unbound ids
9eef589 
This is accessible through Ltac2 Std.clear which doesn't check the ids
before sending to Tactics.clear, and through ltac1 by abusing bound
values eg `Ltac foo := match goal with H : _ |- _ => clear H; clear H end`
@SkySkimmer
Use variable status to decide if a variable is section variable
78b65e7 
Termops.is_section_variable is deprecated and a new API
Termops.is_section_variable' is added because their types are the same
but they need different env arguments so changing in place would be too footgunny.

ssr still uses the old "is it in global env" because IDK what it is
doing.

Fix rocq-prover#18858
@SkySkimmer
changelog for section variable status tracking
44ee3d2
@SkySkimmer
better error message for ReferenceVariables for secvar status mismatch
d52593d
@SkySkimmer
slightly streamline pr_context_of code
4efd00c
@SkySkimmer
Move CompactedDecl to ppconstr
8d6ddc0
@SkySkimmer
Debug flag for variable status
ff75bf4
@SkySkimmer
uncomment assert in environ
f977070 
when this invariant is broken secvar checking produces another assert
failure later
@SkySkimmer
bench auto overlays for metarocq
3452ac2
@SkySkimmer
add is_section_var tactic
395a8d8 
Close rocq-prover#21104
@SkySkimmer
overlay
9fd9307
@SkySkimmer
weaken assert in push_named
db31970
@SkySkimmer
disable some not needed overlays
66dc56d
gares
gares approved these changes Jun 1, 2026
View reviewed changes

@gares gares left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good.
I'd rename the new API as suggested

Comment thread engine/termops.mli Outdated
Comment thread plugins/ssrmatching/ssrmatching.ml
let cl = Evd.evar_concl evi in
let relevance = Evd.evar_relevance evi in
let ans =
(* Why can this get called with an unknown id? *)

@gares gares Jun 1, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

because some new evars may be pruned already wrt that id

@gares

gares commented Jun 1, 2026

Copy link
Copy Markdown
Member

@coqbot merge now

@coqbot-app

coqbot-app Bot commented Jun 1, 2026

Copy link
Copy Markdown
Contributor

@gares: Please take care of the following overlays:

  • 21987-SkySkimmer-context-secvar.sh

@yannl35133 yannl35133 mentioned this pull request Jun 3, 2026
Closed
@SkySkimmer SkySkimmer mentioned this pull request Jul 21, 2026
Merged
@pi8027 pi8027 mentioned this pull request Jul 29, 2026
Merged
@JasonGross JasonGross mentioned this pull request Aug 6, 2026
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@yannl35133 yannl35133 yannl35133 left review comments
@gares gares gares approved these changes

Assignees

@gares gares

Labels

kind: fix This fixes a bug or incorrect documentation. kind: redesign The same functionality is being re-implemented in a different way. part: sections The section mechanism of Coq.

Projects

None yet

Milestone

9.3+rc1

6 participants

@SkySkimmer @gares @yannl35133 @ppedrot @Matafou @silene