Fix "tip not cached" anomaly when there are open proofs at file end

[SkySkimmer]

Fix #16335

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

@coqbot bench

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌──────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                              │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │
│                              │                         │                                       │                                       │                         │
│         package_name         │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├──────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│     coq-metacoq-translations │   17.41    17.82  -2.30 │    78141958055     79902412799  -2.20 │   128828667704    128858141666  -0.02 │  915340   912824   0.28 │
│             coq-math-classes │   84.77    86.19  -1.65 │   383880037993    390346298737  -1.66 │   543109023962    543157052427  -0.01 │  519708   519648   0.01 │
│                    coq-color │  222.77   225.34  -1.14 │  1005126994677   1019767603209  -1.44 │  1478987520859   1478878699363   0.01 │ 1172584  1172848  -0.02 │
│                  coq-bignums │   27.78    28.10  -1.14 │   126546784124    128255681889  -1.33 │   182659578159    182632855732   0.01 │  487068   486712   0.07 │
│                coq-fourcolor │ 1514.86  1531.59  -1.09 │  6908544160372   6985288420985  -1.10 │ 12485491574687  12484458327082   0.01 │ 2292868  2292976  -0.00 │
│                     coq-corn │  777.55   783.99  -0.82 │  3539638550993   3569531880022  -0.84 │  5515222617497   5514782103695   0.01 │  852220   850316   0.22 │
│                  coq-coqutil │   39.00    39.32  -0.81 │   174340123938    176232871942  -1.07 │   254897633165    254896143609   0.00 │  558492   558504  -0.00 │
│                     coq-hott │  147.92   149.10  -0.79 │   669825311297    673531439080  -0.55 │  1062918940736   1062888772093   0.00 │  620136   620112   0.00 │
│         coq-metacoq-template │  163.17   164.45  -0.78 │   730422798833    736977120986  -0.89 │  1169766467723   1169934527469  -0.01 │ 1271772  1273432  -0.13 │
│                coq-fiat-core │   59.51    59.95  -0.73 │   255076050748    257897773266  -1.09 │   379232479408    379201710128   0.01 │  492540   491712   0.17 │
│                 coq-bedrock2 │  312.15   314.38  -0.71 │  1425121512354   1435067223716  -0.69 │  2805902958516   2806079126752  -0.01 │  877064   877072  -0.00 │
│             coq-fiat-parsers │  326.25   328.37  -0.65 │  1465334363855   1477979278186  -0.86 │  2457899591784   2458111126664  -0.01 │ 2733200  2735544  -0.09 │
│            coq-metacoq-pcuic │  616.96   620.71  -0.60 │  2801376112681   2822714906681  -0.76 │  4189479357616   4188735904011   0.02 │ 2090980  2095128  -0.20 │
│                coq-perennial │ 5723.59  5754.94  -0.54 │ 26098119346249  26246945385878  -0.57 │ 43595505748425  43594601538303   0.00 │ 2318968  2319104  -0.01 │
│                 coq-compcert │  283.18   284.64  -0.51 │  1281573689540   1290530773152  -0.69 │  1952167682889   1952418125245  -0.01 │ 1131424  1132824  -0.12 │
│  coq-rewriter-perf-SuperFast │  732.18   735.94  -0.51 │  3328955547941   3347615846805  -0.56 │  5799731404128   5799958898641  -0.00 │ 1445292  1444300   0.07 │
│                  coq-unimath │ 1492.43  1500.02  -0.51 │  6799869952482   6835573802368  -0.52 │ 12818514123189  12818399602630   0.00 │ 1330368  1332072  -0.13 │
│                   coq-geocoq │  606.48   609.25  -0.45 │  2760412707797   2773738606898  -0.48 │  4356341216903   4356604330687  -0.01 │  931856   931736   0.01 │
│          coq-category-theory │  714.32   717.31  -0.42 │  3259384744423   3274005636839  -0.45 │  5620064457363   5620836037963  -0.01 │  924284   924256   0.00 │
│          coq-metacoq-erasure │  329.71   330.95  -0.37 │  1497130799795   1504026906892  -0.46 │  2438094530567   2438054202788   0.00 │ 2676120  2671536   0.17 │
│         coq-mathcomp-algebra │  590.78   592.76  -0.33 │  2700554870701   2709798265049  -0.34 │  4767368346600   4767285886894   0.00 │ 1427428  1427744  -0.02 │
│        coq-mathcomp-solvable │  147.61   148.05  -0.30 │   673540093267    675418485661  -0.28 │  1087485603435   1087470719281   0.00 │ 1726088  1724228   0.11 │
│       coq-mathcomp-ssreflect │  242.81   243.48  -0.28 │  1111656306060   1114811015347  -0.28 │  1962111797098   1962056266788   0.00 │ 1478608  1478728  -0.01 │
│               coq-coquelicot │   37.58    37.68  -0.27 │   167918578880    169171682239  -0.74 │   234157781294    234125831372   0.01 │  802016   802160  -0.02 │
│                 coq-rewriter │  347.67   348.43  -0.22 │  1583747173756   1587423462734  -0.23 │  2635570571410   2635288146646   0.01 │ 1336548  1336760  -0.02 │
│ coq-fiat-crypto-with-bedrock │ 6105.77  6117.22  -0.19 │ 27732061079912  27795581739338  -0.23 │ 51043760949695  51045441916625  -0.00 │ 2406616  2406876  -0.01 │
│       coq-mathcomp-odd-order │  948.08   949.65  -0.17 │  4339771096910   4347017968946  -0.17 │  7432395356128   7432541607849  -0.00 │ 1658528  1658476   0.00 │
│            coq-iris-examples │  480.11   480.59  -0.10 │  2179664716955   2182977871063  -0.15 │  3345646813171   3345510154850   0.00 │ 1070048  1068028   0.19 │
│                    coq-verdi │   46.83    46.86  -0.06 │   212249785707    211937894122   0.15 │   325171134873    325126616479   0.01 │  526580   527584  -0.19 │
│        coq-engine-bench-lite │  156.98   157.04  -0.04 │   672555261997    673439093886  -0.13 │  1255059100911   1253803609358   0.10 │ 1211648  1212020  -0.03 │
│                 coq-coqprime │   45.49    45.49   0.00 │   204804088785    205796025879  -0.48 │   315268243174    315230452104   0.01 │  776996   778436  -0.18 │
│       coq-mathcomp-character │  157.46   157.41   0.03 │   720093297025    719852547288   0.03 │  1129637102616   1129823640371  -0.02 │ 1283924  1283652   0.02 │
│                     coq-core │  114.05   114.01   0.04 │   473168277477    474965681713  -0.38 │   484506593926    484355787450   0.03 │  289300   289832  -0.18 │
│           coq-mathcomp-field │  241.44   241.19   0.10 │  1103007394088   1102370038046   0.06 │  1902388256088   1901464669993   0.05 │ 1348844  1350760  -0.14 │
│               coq-verdi-raft │  561.81   561.05   0.14 │  2564190050064   2560008314276   0.16 │  3991192932398   3992003364725  -0.02 │  820696   819820   0.11 │
│   coq-performance-tests-lite │  759.68   757.79   0.25 │  3442250395806   3432185004073   0.29 │  6061703771021   6061639749481   0.00 │ 1870628  1870564   0.00 │
│      coq-metacoq-safechecker │  375.65   374.58   0.29 │  1717729983044   1712796761839   0.29 │  2870942715245   2870914467250   0.00 │ 2080428  2080684  -0.01 │
│        coq-mathcomp-fingroup │   37.59    37.44   0.40 │   171415735437    170975644166   0.26 │   262490256319    262446577359   0.02 │  559840   559216   0.11 │
│                   coq-stdlib │  406.60   404.56   0.50 │  1747873486305   1735474590509   0.71 │  1447450773165   1447334714566   0.01 │  638228   638240  -0.00 │
│                      coq-vst │  878.99   874.34   0.53 │  3995644809682   3975602900283   0.50 │  6578824311208   6575117326257   0.06 │ 2116652  2116828  -0.01 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SLOW DOWNS                                                          │
│                                                                                                                                    │
│   OLD       NEW      DIFF   %DIFF   Ln                    FILE                                                                     │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  24.3760   25.6990  1.3230  5.43%    20  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                  │
│  24.4110   25.6470  1.2360  5.06%    25  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                  │
│ 128.6690  129.8970  1.2280  0.95%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│ 128.4780  129.6780  1.2000  0.93%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│  41.5480   42.6490  1.1010  2.65%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │
│  41.8610   42.9010  1.0400  2.48%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                │
│  40.7320   41.7690  1.0370  2.55%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html            │
│  19.0950   20.0810  0.9860  5.16%    28  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                  │
│  49.3240   50.1980  0.8740  1.77%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                         │
│  29.5530   30.4130  0.8600  2.91%   515  coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html                               │
│  40.0510   40.7840  0.7330  1.83%   827  coq-vst/veric/binop_lemmas4.v.html                                                        │
│  40.6370   41.3270  0.6900  1.70%   368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                         │
│  35.9230   36.6130  0.6900  1.92%   522  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html                      │
│  51.8890   52.5250  0.6360  1.23%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html      │
│  12.7430   13.3610  0.6180  4.85%    15  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                  │
│   5.4310    5.9730  0.5420  9.98%   167  coq-vst/veric/binop_lemmas6.v.html                                                        │
│  52.6680   53.2020  0.5340  1.01%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html      │
│  19.6900   20.1490  0.4590  2.33%  1073  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                       │
│  13.2680   13.6640  0.3960  2.98%   187  coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html                          │
│  65.4970   65.8350  0.3380  0.52%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                       │
│  41.6970   41.9900  0.2930  0.70%  1002  coq-perennial/src/program_proof/simplepb/pb_apply_proof.v.html                            │
│  11.0420   11.3310  0.2890  2.62%    55  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/Field25519.v.html                 │
│  26.6520   26.9360  0.2840  1.07%   898  coq-perennial/src/program_proof/simplepb/admin_proof.v.html                               │
│  32.5980   32.8800  0.2820  0.87%   673  coq-mathcomp-odd-order/theories/wielandt_fixpoint.v.html                                  │
│   7.4620    7.7390  0.2770  3.71%   703  coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html    │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF    %DIFF    Ln                     FILE                                                                            │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 125.6900  124.3460  -1.3440  -1.07%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                            │
│ 143.1250  141.9100  -1.2150  -0.85%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                     │
│  36.9580   36.2290  -0.7290  -1.97%    12  coq-fourcolor/theories/job439to465.v.html                                                         │
│  23.4990   22.8030  -0.6960  -2.96%    12  coq-fourcolor/theories/job307to310.v.html                                                         │
│  80.3410   79.6620  -0.6790  -0.85%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│ 213.0180  212.4150  -0.6030  -0.28%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                        │
│  80.8830   80.3210  -0.5620  -0.69%   618  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html     │
│  33.1000   32.5940  -0.5060  -1.53%    12  coq-fourcolor/theories/job323to383.v.html                                                         │
│  30.0190   29.5250  -0.4940  -1.65%    12  coq-fourcolor/theories/job287to290.v.html                                                         │
│  21.8300   21.3540  -0.4760  -2.18%    12  coq-fourcolor/theories/job490to494.v.html                                                         │
│  25.9310   25.4580  -0.4730  -1.82%    12  coq-fourcolor/theories/job495to498.v.html                                                         │
│  28.0080   27.5360  -0.4720  -1.69%    12  coq-fourcolor/theories/job535to541.v.html                                                         │
│  45.2230   44.7680  -0.4550  -1.01%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  28.0990   27.6500  -0.4490  -1.60%    12  coq-fourcolor/theories/job223to226.v.html                                                         │
│  33.4660   33.0230  -0.4430  -1.32%    12  coq-fourcolor/theories/job165to189.v.html                                                         │
│  81.2260   80.7950  -0.4310  -0.53%   618  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                       │
│ 122.4790  122.0560  -0.4230  -0.35%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                        │
│  27.0440   26.6260  -0.4180  -1.55%    12  coq-fourcolor/theories/job503to506.v.html                                                         │
│  20.7150   20.3050  -0.4100  -1.98%    12  coq-fourcolor/theories/job311to314.v.html                                                         │
│  26.0030   25.6070  -0.3960  -1.52%    12  coq-fourcolor/theories/job554to562.v.html                                                         │
│  24.5910   24.1950  -0.3960  -1.61%    12  coq-fourcolor/theories/job303to306.v.html                                                         │
│  20.3980   20.0110  -0.3870  -1.90%    12  coq-fourcolor/theories/job271to278.v.html                                                         │
│  31.9180   31.5350  -0.3830  -1.20%    12  coq-fourcolor/theories/job107to164.v.html                                                         │
│  34.3710   33.9940  -0.3770  -1.10%    12  coq-fourcolor/theories/job254to270.v.html                                                         │
│  19.3950   19.0230  -0.3720  -1.92%    12  coq-fourcolor/theories/job550to553.v.html                                                         │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

@coqbot run full ci

[Alizter]

@coqbot merge now

[Zimmi48]

This PR is difficult to backport as it conflicts (in particular) with #17059. I would appreciate it if someone takes care of preparing a backport.

[SkySkimmer]

#17750

[coqbot-app]

This PR was postponed. Please update accordingly the milestone of any issue that this fixes as this cannot be done automatically.

[SkySkimmer]

Why postpone this?

[Zimmi48]

It's not. Your backport PR will be merged in 8.17, so this PR won't be backported using the script.

[SkySkimmer]

So when the backport is merged this PR will get re-milestoned?

[Zimmi48]

This wasn't planned. Is that a problem? FWIW, the closed issue is still in the 8.17.1 milestone and I have added the link from the issue to the backport PR.

[SkySkimmer]

Maybe I misunderstood what the PR milestone is supposed to mean

[Zimmi48]

It's tracking where this specific PR ended up first. In case there is a different PR with a backport, it is the latter that gets the milestone marking where it was merged. I agree that this edge case is maybe not handled as well as it could be.