Keep track of which variables are section variables and use this info to fix bugs by SkySkimmer · Pull Request #21987 · rocq-prover/rocq

SkySkimmer · 2026-04-30T15:17:46Z

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):

Adapt to rocq-prover/rocq#21987 (clear checks that ids are bound even when from match goal) AbsInt/CompCert#582
Adapt to rocq-prover/rocq#21987 (destruct clears non section variable even when reusing a section variable's name) HoTT/Coq-HoTT#2363
Adapt to rocq-prover/rocq#21987 (secvar status) mit-plv/kami#49
Adapt to rocq-prover/rocq#21987 (secvar status) mit-plv/coqutil#164
Adapt to rocq-prover/rocq#21987 (secvar status) mit-plv/bedrock2#533
Adapt to rocq-prover/rocq#21987 (secvar status) mit-plv/fiat-crypto#2334

Overlays (.v, not backwards compatible)

Adapt to rocq-prover/rocq#21987 (secvar status) MetaRocq/metarocq#1271

Overlays (.ml):

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

SkySkimmer · 2026-04-30T17:56:34Z

hott failure is because they workaround #18858 by explcitly clearing

SkySkimmer · 2026-04-30T17:56:52Z

@coqbot ci minimize ci-stdlib

coqbot-app · 2026-05-22T01:52:36Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│          rocq-metarocq-translations │   15.24    15.39  -0.97 │   108460900058    108609591636  -0.14 │  782208   781632   0.07 │
│                       coq-fiat-core │   54.90    55.35  -0.81 │   334154378506    334644223973  -0.15 │  480160   482504  -0.49 │
│                        rocq-runtime │   75.59    76.17  -0.76 │   551410968211    550922017918   0.09 │  495056   494896   0.03 │
│                      rocq-equations │    8.47     8.52  -0.59 │    58319595974     58518152257  -0.34 │  400344   400212   0.03 │
│                  rocq-mathcomp-boot │   39.16    39.36  -0.51 │   231969433356    232442981272  -0.20 │  657692   655736   0.30 │
│               rocq-mathcomp-algebra │  330.40   331.54  -0.34 │  2432940352490   2433806535747  -0.04 │ 1347144  1360400  -0.97 │
│                rocq-metarocq-common │   41.12    41.25  -0.32 │   267617046045    267866051879  -0.09 │  900376   902100  -0.19 │
│              rocq-mathcomp-solvable │   98.40    98.60  -0.20 │   665728961428    666805049002  -0.16 │ 1094696  1096816  -0.19 │
│              rocq-metarocq-template │   81.53    81.68  -0.18 │   559588924291    559874292906  -0.05 │ 1100704  1082180   1.71 │
│                   coq-iris-examples │  363.47   364.11  -0.18 │  2379643001097   2384579112909  -0.21 │ 1059756  1067968  -0.77 │
│          coq-performance-tests-lite │  881.44   882.75  -0.15 │  7089798296812   7087419523580   0.03 │ 1302476  1312280  -0.75 │
│                           rocq-elpi │   16.13    16.15  -0.12 │   116659004245    116510622687   0.13 │  449060   448928   0.03 │
│                        coq-rewriter │  329.06   329.32  -0.08 │  2456218305352   2452520091356   0.15 │ 1395576  1434316  -2.70 │
│                       coq-fourcolor │ 1353.33  1354.23  -0.07 │ 12425073313317  12426692408134  -0.01 │ 1021376  1017940   0.34 │
│                         rocq-stdlib │  420.77   420.97  -0.05 │  1506367884302   1508173986396  -0.12 │  633932   629796   0.66 │
│                    coq-fiat-parsers │  272.07   272.18  -0.04 │  2088094563887   2087195747934   0.04 │ 2037228  2033048   0.21 │
│                         coq-unimath │ 1817.86  1816.32   0.08 │ 15133699230466  15155142494046  -0.14 │ 1093312  1086004   0.67 │
│                           coq-verdi │   42.87    42.83   0.09 │   286403582420    286743633665  -0.12 │  523820   524684  -0.16 │
│                        rocq-bignums │   24.85    24.82   0.12 │   158470550764    157974596779   0.31 │  462864   465264  -0.52 │
│                            coq-hott │  157.18   156.98   0.13 │  1057878602215   1058596266315  -0.07 │  459684   479100  -4.05 │
│                         coq-coqutil │   46.92    46.86   0.13 │   290875193258    290134341513   0.26 │  566216   566408  -0.03 │
│                 coq-category-theory │  634.37   633.35   0.16 │  4768399318424   4773509223214  -0.11 │ 6749640  6746864   0.04 │
│                      coq-coquelicot │   38.67    38.58   0.23 │   233838289080    234185145551  -0.15 │  831040   828208   0.34 │
│          rocq-mathcomp-finite-group │   26.47    26.40   0.27 │   172260889722    172612313793  -0.20 │  568308   570264  -0.34 │
│                    coq-math-classes │   81.98    81.74   0.29 │   497761204869    499375877590  -0.32 │  514104   513588   0.10 │
│                            coq-corn │  636.68   633.84   0.45 │  4318892781675   4325359351728  -0.15 │  617480   617548  -0.01 │
│                           coq-color │  229.87   228.80   0.47 │  1452936418620   1454548575157  -0.11 │ 1162168  1153772   0.73 │
│                           rocq-core │    6.86     6.82   0.59 │    41325325268     41342326472  -0.04 │  444388   444668  -0.06 │
│         coq-rewriter-perf-SuperFast │  467.50   464.74   0.59 │  3650304122373   3651399363648  -0.03 │ 1242888  1242500   0.03 │
│                      coq-verdi-raft │  491.07   487.99   0.63 │  3389266567109   3385976702947   0.10 │  812316   818316  -0.73 │
│               coq-engine-bench-lite │  128.30   127.41   0.70 │   950508632069    947579659387   0.31 │ 1006772  1103620  -8.78 │
│             rocq-mathcomp-ssreflect │    1.16     1.15   0.87 │     7668175346      7666564116   0.02 │  593400   595324  -0.32 │
│                 rocq-mathcomp-order │   81.83    81.11   0.89 │   600789254782    600847920485  -0.01 │ 1606708  1606592   0.01 │
│                 rocq-metarocq-utils │   24.52    24.30   0.91 │   159253262439    158932609226   0.20 │  590872   591032  -0.03 │
│ coq-neural-net-interp-computed-lite │  237.19   234.80   1.02 │  2262033058691   2262694519178  -0.03 │  878440   880976  -0.29 │
│                            coq-core │    2.76     2.72   1.47 │    18573834271     18570373810   0.02 │   90844    90704   0.15 │
│                        coq-coqprime │   57.07    56.18   1.58 │   392100839280    390433200382   0.43 │  818080   820008  -0.24 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-mathcomp-field (in NEW)
coq-compcert (dependency install failed in NEW)
rocq-metarocq-pcuic (in NEW)
coq-bedrock2 (in NEW)
coq-fiat-crypto-with-bedrock (in NEW)

rocq-mathcomp-group-representation (dependency rocq-mathcomp-field failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-field failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-field failed)
rocq-metarocq-safechecker (dependency rocq-metarocq-pcuic failed)
rocq-metarocq-erasure (dependency rocq-metarocq-pcuic failed)
coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SLOW DOWNS                                                           │
│                                                                                                                                       │
│   OLD     NEW    DIFF    %DIFF     Ln                    FILE                                                                         │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│     200    202  2.4482     1.23%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│    17.5   18.3  0.7390     4.22%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                     │
│   0.930   1.64  0.7097    76.28%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│    48.6   49.2  0.6097     1.25%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│    36.8   37.3  0.5113     1.39%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                  │
│    18.2   18.6  0.3905     2.14%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                             │
│   0.192  0.546  0.3546   184.91%   592  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│    38.1   38.5  0.3497     0.92%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                │
│    38.8   39.1  0.3479     0.90%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                    │
│    25.3   25.7  0.3285     1.30%    13  coq-fourcolor/theories/proof/job618to622.v.html                                               │
│   0.807   1.13  0.3271    40.54%   200  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                            │
│    9.44   9.74  0.3074     3.26%    87  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                         │
│    21.1   21.4  0.3007     1.43%    13  coq-fourcolor/theories/proof/job219to222.v.html                                               │
│   0.278  0.577  0.2988   107.31%   163  rocq-stdlib/theories/Numbers/HexadecimalPos.v.html                                            │
│    26.4   26.7  0.2965     1.12%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                   │
│   0.196  0.478  0.2820   143.57%  1187  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│    25.7   26.0  0.2421     0.94%    13  coq-fourcolor/theories/proof/job499to502.v.html                                               │
│   0.238  0.477  0.2394   100.68%    13  rocq-stdlib/theories/micromega/ZCoeff.v.html                                                  │
│   0.220  0.456  0.2368   107.84%  1982  rocq-stdlib/theories/FSets/FMapFacts.v.html                                                   │
│    3.38   3.62  0.2357     6.97%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                          │
│ 0.00563  0.239  0.2330  4137.55%   380  coq-fourcolor/theories/proof/dedekind.v.html                                                  │
│ 0.00551  0.237  0.2317  4207.90%   402  coq-fourcolor/theories/proof/finitize.v.html                                                  │
│   0.386  0.616  0.2300    59.58%    19  rocq-stdlib/theories/ZArith/Zcompare.v.html                                                   │
│    17.4   17.6  0.2285     1.31%    13  coq-fourcolor/theories/proof/job550to553.v.html                                               │
│  0.0231  0.247  0.2235   967.85%   341  coq-fourcolor/theories/proof/discretize.v.html                                                │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SPEED UPS                                                               │
│                                                                                                                                             │
│  OLD     NEW      DIFF     %DIFF    Ln                     FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  90.7      89.4  -1.2399   -1.37%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  90.2      89.2  -1.0445   -1.16%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│ 0.756     0.291  -0.4650  -61.54%   484  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                               │
│  1.34     0.887  -0.4557  -33.94%   702  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                               │
│ 0.692     0.292  -0.4006  -57.87%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                     │
│  25.5      25.1  -0.3816   -1.50%    13  coq-fourcolor/theories/proof/job279to282.v.html                                                    │
│  7.63      7.29  -0.3427   -4.49%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html     │
│ 0.901     0.563  -0.3384  -37.55%   816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                          │
│  26.8      26.5  -0.3143   -1.17%    13  coq-fourcolor/theories/proof/job399to438.v.html                                                    │
│  16.8      16.5  -0.2962   -1.77%    13  coq-fourcolor/theories/proof/job235to238.v.html                                                    │
│ 0.652     0.357  -0.2947  -45.21%    11  rocq-stdlib/theories/ZArith/Zpow_alt.v.html                                                        │
│  20.2      19.9  -0.2929   -1.45%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html                 │
│ 0.598     0.316  -0.2822  -47.19%    14  rocq-stdlib/theories/extraction/ExtrOcamlZBigInt.v.html                                            │
│ 0.698     0.421  -0.2768  -39.69%  1604  rocq-stdlib/theories/micromega/Tauto.v.html                                                        │
│  7.22      6.96  -0.2604   -3.61%   604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
│  26.9      26.7  -0.2570   -0.95%    13  coq-fourcolor/theories/proof/job190to206.v.html                                                    │
│  26.0      25.7  -0.2554   -0.98%    13  coq-fourcolor/theories/proof/job466to485.v.html                                                    │
│ 0.236  0.000953  -0.2348  -99.60%   376  coq-fourcolor/theories/proof/dedekind.v.html                                                       │
│  21.0      20.8  -0.2332   -1.11%    13  coq-fourcolor/theories/proof/job307to310.v.html                                                    │
│ 0.544     0.312  -0.2320  -42.61%    13  rocq-stdlib/theories/ZArith/Zmin.v.html                                                            │
│ 0.238   0.00781  -0.2302  -96.72%   400  coq-fourcolor/theories/proof/finitize.v.html                                                       │
│ 0.258    0.0295  -0.2288  -88.57%   543  coq-fourcolor/theories/proof/dedekind.v.html                                                       │
│  18.3      18.1  -0.2272   -1.24%    13  coq-fourcolor/theories/proof/job271to278.v.html                                                    │
│ 0.508     0.282  -0.2257  -44.41%    16  rocq-stdlib/theories/micromega/EnvRing.v.html                                                      │
│ 0.220   0.00147  -0.2190  -99.33%   287  coq-fourcolor/theories/proof/approx.v.html                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

SkySkimmer · 2026-05-22T13:57:57Z

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 · 2026-05-22T20:48:02Z

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 · 2026-05-23T10:10:30Z

Can be turned into a bug on master #22057

SkySkimmer · 2026-05-26T15:02:01Z

Rocq call: seems like the right direction

gares · 2026-05-27T20:29:47Z

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

Close rocq-prover#6773

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

Fix rocq-prover#12304

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`

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

when this invariant is broken secvar checking produces another assert failure later

Close rocq-prover#21104

gares

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

gares · 2026-06-01T14:50:51Z

  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? *)


because some new evars may be pruned already wrt that id

gares · 2026-06-01T18:57:28Z

@coqbot merge now

coqbot-app · 2026-06-01T18:57:36Z

@gares: Please take care of the following overlays:

21987-SkySkimmer-context-secvar.sh

SkySkimmer requested review from a team as code owners April 30, 2026 15:17

SkySkimmer added the needs: merge of dependency This PR depends on another PR being merged first. label Apr 30, 2026

SkySkimmer requested review from a team as code owners April 30, 2026 15:17

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 requested review from a team as code owners April 30, 2026 15:17

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 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026

SkySkimmer force-pushed the context-secvar branch from b3a9eeb to 38aca30 Compare April 30, 2026 15:49

SkySkimmer requested a review from a team as a code owner April 30, 2026 15:49

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 added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 30, 2026

SkySkimmer force-pushed the context-secvar branch from 38aca30 to 7551c70 Compare April 30, 2026 15:53

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

This was referenced May 22, 2026

Adapt to rocq-prover/rocq#21987 (secvar status) mit-plv/bedrock2#533

Merged

Adapt to rocq-prover/rocq#21987 (secvar status) mit-plv/fiat-crypto#2334

Merged

Adapt to rocq-prover/rocq#21987 (secvar status) Lysxia/coq-ceres#32

Open

SkySkimmer added 16 commits May 28, 2026 12:55

Keep track of variable status (secvar or not) in named contexts

980c7ea

Close rocq-prover#6773

Error instead of renaming section variable mentioned through a global

0c35e6b

Fix rocq-prover#12304

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`

changelog for section variable status tracking

44ee3d2

better error message for ReferenceVariables for secvar status mismatch

d52593d

slightly streamline pr_context_of code

4efd00c

Move CompactedDecl to ppconstr

8d6ddc0

Debug flag for variable status

ff75bf4

uncomment assert in environ

f977070

when this invariant is broken secvar checking produces another assert failure later

bench auto overlays for metarocq

3452ac2

add is_section_var tactic

395a8d8

Close rocq-prover#21104

overlay

9fd9307

weaken assert in push_named

db31970

disable some not needed overlays

66dc56d

gares approved these changes Jun 1, 2026

View reviewed changes

Rename is_section_variable' -> is_section_variable_env

60156a0

yannl35133 mentioned this pull request Jun 3, 2026

lia does not terminate in the presence of a section variable #22093

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

SkySkimmer commented Apr 30, 2026 •

edited

Loading

Uh oh!

SkySkimmer commented Apr 30, 2026

Uh oh!

SkySkimmer commented Apr 30, 2026

Uh oh!

coqbot-app Bot commented May 22, 2026

Uh oh!

SkySkimmer commented May 22, 2026 •

edited

Loading

Uh oh!

gares commented May 22, 2026

Uh oh!

SkySkimmer commented May 23, 2026

Uh oh!

SkySkimmer commented May 26, 2026

Uh oh!

gares commented May 27, 2026

Uh oh!

gares left a comment

Uh oh!

Uh oh!

gares Jun 1, 2026

Uh oh!

gares commented Jun 1, 2026

Uh oh!

coqbot-app Bot commented Jun 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

SkySkimmer commented Apr 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SkySkimmer commented Apr 30, 2026

Uh oh!

SkySkimmer commented Apr 30, 2026

Uh oh!

coqbot-app Bot commented May 22, 2026

Uh oh!

SkySkimmer commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gares commented May 22, 2026

Uh oh!

SkySkimmer commented May 23, 2026

Uh oh!

SkySkimmer commented May 26, 2026

Uh oh!

gares commented May 27, 2026

Uh oh!

gares left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

gares Jun 1, 2026

Choose a reason for hiding this comment

Uh oh!

gares commented Jun 1, 2026

Uh oh!

coqbot-app Bot commented Jun 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

SkySkimmer commented Apr 30, 2026 •

edited

Loading

SkySkimmer commented May 22, 2026 •

edited

Loading