Fix goal-tactic association in typeclass search

[Janno]

The code was written by GPT-5.5 based on the findings from my debugging attempts in #21044. I have not changed the LLM's code yet. I hope the change is small enough to be reviewable. If the mechanism is acceptable, I will polish the code.

This change introduces a notion of search "generations" to search_fixpoint. This allows us to track precisely which goals have been stuck for how long and which ones need to be retried when we make any kind of progress. Then, to make sure that goals and tactics stay properly aligned in the presence of goal reorderings, we look up the evar's index in the proofview goals and focus that index explicitly.

The lookup is currently a linear search through the list of goals. I have previously tried to work with goal state instead. My idea was to keep an index in the goal that maps to a tactic in some kind of array/map. But Class_tactics drops goal state in several places and I could not make the change work. The LLM might have a better chance so I am happy to try that if the linear search is a problem and there is no easy workaround.

The change has been tested on skylabs code where it brings a very modest 0.1% overall speedup with no significant slowdowns. Full report

Fixes / closes #21044

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[Janno]

@coqbot run full ci

[mattam82]

@coqbot bench

[Janno]

It seems the job got stuck somehow? Does it make sense to try again?

[SkySkimmer]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                            coq-core │    2.73     2.84  -3.87 │    18573508308     18561249235   0.07 │   91276    91460  -0.20 │
│                           rocq-elpi │   16.22    16.45  -1.40 │   116656422147    116617804758   0.03 │  450328   450040   0.06 │
│                         rocq-stdlib │  435.44   439.77  -0.98 │  1556121045808   1555930946748   0.01 │  632416   630368   0.32 │
│                        rocq-runtime │   75.76    76.22  -0.60 │   550963483255    550762566231   0.04 │  493604   494832  -0.25 │
│                  rocq-mathcomp-boot │   39.39    39.58  -0.48 │   233141884587    233168907090  -0.01 │  658196   658328  -0.02 │
│         coq-rewriter-perf-SuperFast │  474.92   476.58  -0.35 │  3714535196111   3714188157770   0.01 │ 1249736  1244120   0.45 │
│                        rocq-bignums │   25.28    25.33  -0.20 │   160268347352    160206377199   0.04 │  460532   460196   0.07 │
│                           coq-verdi │   43.36    43.39  -0.07 │   288773331914    288926503183  -0.05 │  528084   526492   0.30 │
│               coq-engine-bench-lite │  128.67   128.65   0.02 │   956766743213    959335207359  -0.27 │ 1106232  1106468  -0.02 │
│                 rocq-mathcomp-field │  194.08   193.85   0.12 │  1453870983279   1454028040093  -0.01 │ 2301620  2303532  -0.08 │
│                         coq-unimath │ 1831.08  1828.88   0.12 │ 15245901282445  15249528894886  -0.02 │ 1094036  1095924  -0.17 │
│               rocq-mathcomp-algebra │  332.38   331.61   0.23 │  2436092813548   2435956427873   0.01 │ 1345452  1346024  -0.04 │
│                       coq-fourcolor │ 1358.38  1353.48   0.36 │ 12447830347299  12447179996836   0.01 │ 1017872  1017808   0.01 │
│              rocq-mathcomp-solvable │   99.95    99.56   0.39 │   674146307425    674173451020  -0.00 │ 1123616  1123636  -0.00 │
│                            coq-hott │  159.41   158.76   0.41 │  1075074265098   1074981865150   0.01 │  466156   470384  -0.90 │
│          rocq-mathcomp-finite-group │   26.74    26.63   0.41 │   173277362034    173277062114   0.00 │  574636   576420  -0.31 │
│  rocq-mathcomp-group-representation │  104.51   104.06   0.43 │   731365828374    731388081893  -0.00 │ 1717332  1713840   0.20 │
│                           coq-color │  232.26   231.22   0.45 │  1467322806771   1467007341434   0.02 │ 1170424  1165636   0.41 │
│               coq-mathcomp-analysis │ 1159.72  1153.77   0.52 │  8423645949472   8424106723721  -0.01 │ 1965776  1965704   0.00 │
│                    coq-fiat-parsers │  277.88   276.42   0.53 │  2122177118977   2122109709521   0.00 │ 2272544  2270292   0.10 │
│          coq-performance-tests-lite │  903.91   899.08   0.54 │  7227583482630   7229321325918  -0.02 │ 1224284  1227320  -0.25 │
│                        coq-rewriter │  333.40   331.61   0.54 │  2471442111785   2471456126836  -0.00 │ 1458828  1466832  -0.55 │
│                      coq-verdi-raft │  495.73   492.90   0.57 │  3423365168335   3423969305152  -0.02 │  812052   810332   0.21 │
│                    coq-math-classes │   83.18    82.67   0.62 │   503438160117    503166107589   0.05 │  513812   514192  -0.07 │
│                 rocq-mathcomp-order │   81.32    80.82   0.62 │   599952093327    599914961701   0.01 │ 1601880  1602404  -0.03 │
│                      coq-coquelicot │   39.14    38.89   0.64 │   236675983205    236599883093   0.03 │  832120   830480   0.20 │
│              coq-mathcomp-odd-order │  609.30   605.37   0.65 │  4311160845747   4311646625654  -0.01 │ 2638568  2641916  -0.13 │
│                        coq-bedrock2 │  360.87   358.12   0.77 │  2991940873322   2991927471687   0.00 │  833528   834180  -0.08 │
│                   coq-iris-examples │  367.97   365.06   0.80 │  2391418000834   2391609296617  -0.01 │ 1086072  1084268   0.17 │
│                        coq-coqprime │   53.61    53.16   0.85 │   362554293826    362527446752   0.01 │  824016   824128  -0.01 │
│                       coq-fiat-core │   55.89    55.37   0.94 │   337118808851    336924833126   0.06 │  484736   484980  -0.05 │
│                         coq-coqutil │   47.66    47.08   1.23 │   292462944601    292376964473   0.03 │  565192   563812   0.24 │
│                           rocq-core │    6.80     6.71   1.34 │    41674753823     41652452769   0.05 │  445856   446964  -0.25 │
│                            coq-corn │  667.50   658.07   1.43 │  4454619800406   4454309693304   0.01 │  768308   769616  -0.17 │
│             rocq-mathcomp-ssreflect │    1.13     1.10   2.73 │     7132987512      7131370157   0.02 │  593756   593616   0.02 │
│ coq-neural-net-interp-computed-lite │  243.34   236.47   2.91 │  2264157766425   2264427220016  -0.01 │  878708   878536   0.02 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-compcert (dependency install failed in NEW)
rocq-equations (in NEW)
coq-fiat-crypto-with-bedrock (in NEW)

rocq-metarocq-utils (dependency rocq-equations failed)
rocq-metarocq-common (dependency rocq-equations failed)
rocq-metarocq-template (dependency rocq-equations failed)
rocq-metarocq-pcuic (dependency rocq-equations failed)
rocq-metarocq-safechecker (dependency rocq-equations failed)
rocq-metarocq-erasure (dependency rocq-equations failed)
rocq-metarocq-translations (dependency rocq-equations failed)
coq-vst (dependency coq-compcert failed)
coq-category-theory (dependency rocq-equations failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                         │
│  OLD    NEW    DIFF    %DIFF    Ln                     FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   201    208  6.7809    3.37%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│  63.1   64.6  1.4659    2.32%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│  93.6   94.5  0.8384    0.90%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  7.96   8.64  0.6846    8.60%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                  │
│  2.07   2.55  0.4829   23.36%   213  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                                 │
│  7.07   7.53  0.4612    6.52%   604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
│  38.7   39.1  0.4193    1.08%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                         │
│  22.1   22.5  0.4129    1.87%    13  coq-fourcolor/theories/proof/job384to398.v.html                                                    │
│ 0.343  0.708  0.3654  106.64%    14  rocq-stdlib/theories/MSets/MSetToFiniteSet.v.html                                                  │
│  36.5   36.8  0.3625    0.99%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                       │
│ 0.384  0.739  0.3549   92.30%   596  rocq-stdlib/theories/Strings/Byte.v.html                                                           │
│  22.2   22.6  0.3433    1.54%    13  coq-fourcolor/theories/proof/job303to306.v.html                                                    │
│  9.37   9.70  0.3371    3.60%   435  coq-mathcomp-odd-order/theories/PFsection12.v.html                                                 │
│  18.3   18.6  0.3258    1.78%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                  │
│  48.3   48.6  0.3223    0.67%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│ 0.252  0.569  0.3177  126.25%   707  rocq-stdlib/theories/MSets/MSetList.v.html                                                         │
│  38.1   38.4  0.2972    0.78%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                     │
│  28.7   29.0  0.2944    1.03%    13  coq-fourcolor/theories/proof/job563to588.v.html                                                    │
│  16.7   17.0  0.2908    1.74%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                               │
│ 0.888   1.17  0.2848   32.05%   816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                          │
│  24.5   24.8  0.2735    1.12%    13  coq-fourcolor/theories/proof/job319to322.v.html                                                    │
│ 0.485  0.756  0.2707   55.82%   207  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                                 │
│  23.7   23.9  0.2612    1.10%    13  coq-fourcolor/theories/proof/job295to298.v.html                                                    │
│ 0.430  0.679  0.2497   58.14%   474  rocq-stdlib/theories/MSets/MSetWeakList.v.html                                                     │
│ 0.334  0.578  0.2435   72.87%    14  rocq-stdlib/theories/Numbers/Integer/Binary/ZBinary.v.html                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SPEED UPS                                                         │
│                                                                                                                                  │
│  OLD     NEW     DIFF     %DIFF    Ln                   FILE                                                                     │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  1.73    0.616  -1.1166  -64.43%  2109  rocq-stdlib/theories/FSets/FMapFacts.v.html                                              │
│ 0.622    0.197  -0.4251  -68.29%    16  rocq-stdlib/theories/Numbers/DecimalQ.v.html                                             │
│  1.47     1.06  -0.4114  -27.92%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                │
│  25.9     25.5  -0.3966   -1.53%    13  coq-fourcolor/theories/proof/job618to622.v.html                                          │
│ 0.641    0.293  -0.3478  -54.28%   586  rocq-stdlib/theories/Strings/Byte.v.html                                                 │
│ 0.349  0.00289  -0.3458  -99.17%   143  coq-mathcomp-analysis/theories/lebesgue_measure.v.html                                   │
│ 0.426    0.119  -0.3066  -72.03%   638  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                │
│ 0.556    0.253  -0.3027  -54.43%    11  rocq-stdlib/theories/ZArith/Zpow_alt.v.html                                              │
│ 0.556    0.271  -0.2850  -51.30%    12  rocq-stdlib/theories/ZArith/Znumtheory.v.html                                            │
│ 0.547    0.264  -0.2830  -51.73%    12  rocq-stdlib/theories/MSets/MSets.v.html                                                  │
│ 0.546    0.288  -0.2573  -47.15%    17  rocq-stdlib/theories/micromega/QMicromega.v.html                                         │
│  18.1     17.9  -0.2567   -1.42%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                │
│ 0.496    0.244  -0.2520  -50.84%     1  rocq-stdlib/theories/ZArith/Zcong.v.html                                                 │
│ 0.483    0.233  -0.2502  -51.80%    19  rocq-stdlib/theories/ZArith/Int.v.html                                                   │
│  18.2     18.0  -0.2281   -1.25%    32  coq-performance-tests-lite/src/pattern.v.html                                            │
│ 0.583    0.367  -0.2165  -37.10%    14  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html                                     │
│ 0.624    0.415  -0.2090  -33.50%  1161  rocq-stdlib/theories/Strings/Byte.v.html                                                 │
│  1.87     1.66  -0.2069  -11.07%   313  rocq-stdlib/theories/Strings/Byte.v.html                                                 │
│  12.3     12.1  -0.2058   -1.67%   324  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│  10.3     10.1  -0.2057   -1.99%   496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                             │
│ 0.535    0.332  -0.2033  -38.00%    15  rocq-stdlib/theories/micromega/ZifyInst.v.html                                           │
│  25.7     25.5  -0.2005   -0.78%    13  coq-fourcolor/theories/proof/job499to502.v.html                                          │
│  26.8     26.6  -0.2004   -0.75%    13  coq-fourcolor/theories/proof/job190to206.v.html                                          │
│ 0.259   0.0672  -0.1918  -74.05%   676  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                │
│  3.93     3.75  -0.1853   -4.71%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                            │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[Janno]

the failure in equations looks unrelated: https://coq.gitlabpages.inria.fr/-/coq/-/jobs/7348171/artifacts/_bench/logs/rocq-equations.NEW.opam_install.1.stderr.log

[mattam82]

The reasoning looks sound to me, and indeed it can fix the issue of goal / tactic desynchronization, so I'm happy with it. I don't have a better idea than the linear search ATM.

[Janno]

Great! Does this need any changes before it can go in?