Use full_path for absolute paths more consistently #20371

SkySkimmer · 2025-03-18T17:04:03Z

In particular, the module and section nametabs use full_path instead
of dirpath, and the libobject object_prefix contains a full_path
instead of a dirpath.

Note that the comment on Lib.current_dirpath false was apparently
incorrect (or maybe this changed semantics at some point?)

Overlays:

…_module)

… returning full_path)

Adapt to rocq-prover/rocq#20371 (Libnames.dirpath deprecated)

This check is anyway redundant with the kernel side check. For a modtype T it would check for T.T. Also the nametabs for modules and for modtypes are separate and it would only check one, but the kernel puts modules and modtypes in the same namespace.

(the synterp side are used by synterp-only functions)

We deprecated [Libnames.dirpath] because it is confusing when [dirpath_of_path] has a different meaning.

In particular, the module and section nametabs use full_path instead of dirpath, and the libobject object_prefix contains a full_path instead of a dirpath. Note that the comment on `Lib.current_dirpath false` was apparently incorrect (or maybe this changed semantics at some point?)

ppedrot

Nothing out of the ordinary.

ppedrot · 2025-03-26T09:58:47Z

@coqbot bench

coqbot-app · 2025-03-26T22:43:47Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                           rocq-elpi │   12.66    12.77  -0.86 │    91258068056     91271493697  -0.01 │  485828   479544   1.31 │
│ coq-neural-net-interp-computed-lite │  233.68   235.64  -0.83 │  2247200171408   2246909160605   0.01 │  858904   870772  -1.36 │
│                        coq-coqprime │   51.04    51.37  -0.64 │   352780871970    352230956552   0.16 │  800304   796568   0.47 │
│                         coq-unimath │ 2280.37  2293.37  -0.57 │ 18167330003669  18164229484885   0.02 │ 1119152  1084100   3.23 │
│             coq-metacoq-safechecker │  342.57   344.08  -0.44 │  2594300921490   2593049953547   0.05 │ 1748944  1730400   1.07 │
│              coq-mathcomp-ssreflect │   84.04    84.41  -0.44 │   569914152670    569811276347   0.02 │ 1498576  1501200  -0.17 │
│                        coq-compcert │  309.26   310.48  -0.39 │  2032162252071   2031077316509   0.05 │ 1145204  1101036   4.01 │
│               coq-engine-bench-lite │  124.65   125.02  -0.30 │   934243071972    937501535262  -0.35 │ 1077516  1077468   0.00 │
│               coq-mathcomp-solvable │   79.56    79.74  -0.23 │   548676503045    548180994388   0.09 │  910548   905656   0.54 │
│                       coq-fiat-core │   57.16    57.28  -0.21 │   351504476210    351313322501   0.05 │  477528   474144   0.71 │
│               coq-mathcomp-fingroup │   22.90    22.94  -0.17 │   149074777144    148960874458   0.08 │  503368   500908   0.49 │
│                      coq-verdi-raft │  532.12   533.01  -0.17 │  3715035852714   3713332152915   0.05 │  832788   827712   0.61 │
│                   coq-metacoq-utils │   22.76    22.78  -0.09 │   150747368248    149930542879   0.54 │  584704   583156   0.27 │
│                  coq-mathcomp-field │   92.52    92.59  -0.08 │   669173248719    668129330233   0.16 │ 1337020  1330404   0.50 │
│              coq-mathcomp-odd-order │  482.80   483.15  -0.07 │  3491514446347   3489602920796   0.05 │ 1674608  1671044   0.21 │
│          coq-performance-tests-lite │  896.37   897.01  -0.07 │  7264214321180   7268564006970  -0.06 │ 2475324  1938548  27.69 │
│                             coq-vst │  865.50   866.02  -0.06 │  6547920938341   6541230905111   0.10 │ 2227668  2228544  -0.04 │
│        coq-fiat-crypto-with-bedrock │ 6049.71  6052.17  -0.04 │ 49266733002454  49246486387769   0.04 │ 3148148  3178768  -0.96 │
│                 coq-metacoq-erasure │  514.19   514.36  -0.03 │  3547801647156   3544522487825   0.09 │ 1771892  1744624   1.56 │
│                        coq-bedrock2 │  340.38   340.49  -0.03 │  2857452883498   2853575721841   0.14 │  889736   889528   0.02 │
│                       coq-fourcolor │ 1311.92  1312.24  -0.02 │ 12213392906313  12214317274557  -0.01 │  774140   773804   0.04 │
│                         rocq-stdlib │  209.33   209.38  -0.02 │  1318471869770   1316982421876   0.11 │  578908   577616   0.22 │
│                   coq-iris-examples │  379.62   379.68  -0.02 │  2550344199528   2546008862313   0.17 │ 1077124  1061528   1.47 │
│                    coq-fiat-parsers │  273.50   273.52  -0.01 │  2121410579846   2116342238911   0.24 │ 2286704  2282860   0.17 │
│                            coq-corn │  669.56   669.34   0.03 │  4598493866280   4594744015961   0.08 │  709212   716880  -1.07 │
│                           coq-color │  245.11   244.98   0.05 │  1543144073881   1541134377601   0.13 │ 1092536  1063472   2.73 │
│                        rocq-bignums │   29.84    29.82   0.07 │   191759448508    191449160129   0.16 │  480244   480712  -0.10 │
│                           coq-verdi │   44.13    44.10   0.07 │   297013287374    296487720209   0.18 │  533448   524748   1.66 │
│               coq-mathcomp-analysis │  571.58   571.18   0.07 │  4195202692508   4191226405522   0.09 │ 1498308  1499120  -0.05 │
│                   coq-metacoq-pcuic │  645.30   644.31   0.15 │  4161065442809   4155651380824   0.13 │ 2286592  2285244   0.06 │
│                coq-metacoq-template │  144.40   144.17   0.16 │   970725370644    968827906861   0.20 │  953876   961520  -0.79 │
│                        rocq-runtime │   73.48    73.34   0.19 │   530683199104    530515932913   0.03 │  486784   485916   0.18 │
│                            coq-hott │  155.83   155.42   0.26 │  1087393406537   1086749523777   0.06 │  470200   470292  -0.02 │
│                 coq-category-theory │  594.85   593.26   0.27 │  4381296835617   4380432902923   0.02 │  953028   952008   0.11 │
│                        coq-rewriter │  335.68   334.18   0.45 │  2504522398319   2503815312311   0.03 │ 1303284  1301020   0.17 │
│                  coq-metacoq-common │   64.62    64.33   0.45 │   418603425289    417378349406   0.29 │  908980   911604  -0.29 │
│                      coq-coquelicot │   37.67    37.48   0.51 │   227494732501    226376166489   0.49 │  823888   822200   0.21 │
│                           rocq-core │    6.63     6.59   0.61 │    40906630134     40910732405  -0.01 │  438112   437648   0.11 │
│         coq-rewriter-perf-SuperFast │  481.08   477.96   0.65 │  3746156494369   3744545460035   0.04 │ 1238160  1245936  -0.62 │
│                coq-mathcomp-algebra │  171.25   170.03   0.72 │  1206851947753   1205216190076   0.14 │ 1102692  1099084   0.33 │
│                         coq-coqutil │   44.37    44.04   0.75 │   279487450815    279143387195   0.12 │  557836   556780   0.19 │
│                    coq-math-classes │   86.35    85.66   0.81 │   530501459825    529741804545   0.14 │  509164   508896   0.05 │
│            coq-metacoq-translations │   16.28    16.14   0.87 │   116212112554    115818995721   0.34 │  760444   760772  -0.04 │
│              coq-mathcomp-character │   69.92    69.31   0.88 │   481487331823    480993432696   0.10 │ 1158024  1153980   0.35 │
│                            coq-core │    2.89     2.84   1.76 │    19632092517     19627017424   0.03 │   91696    91876  -0.20 │
│                      rocq-equations │    9.07     8.88   2.14 │    62408339800     62403231130   0.01 │  400828   400504   0.08 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SLOW DOWNS                                                           │
│                                                                                                                                      │
│   OLD      NEW     DIFF     %DIFF     Ln                    FILE                                                                     │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│      119     121  1.9945      1.67%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                    │
│     9.04    9.63  0.5884      6.51%   434  coq-mathcomp-odd-order/theories/PFsection12.v.html                                        │
│     93.4    94.0  0.5329      0.57%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                               │
│   42.015  42.447  0.4320      1.03%   834  coq-vst/veric/binop_lemmas4.v.html                                                        │
│     1.73    2.15  0.4222     24.44%   635  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                               │
│     1.28    1.67  0.3888     30.32%  2103  coq-fiat-parsers/src/Parsers/BooleanRecognizerOptimized.v.html                            │
│     15.4    15.8  0.3570      2.31%   618  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html   │
│   11.474  11.814  0.3400      2.96%   126  coq-vst/veric/binop_lemmas6.v.html                                                        │
│    31.84  32.178  0.3380      1.06%    97  coq-vst/veric/binop_lemmas5.v.html                                                        │
│     36.6    36.9  0.3174      0.87%   974  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                      │
│     29.3    29.6  0.3117      1.06%    12  coq-fourcolor/theories/proof/job001to106.v.html                                           │
│     11.0    11.3  0.2700      2.46%   705  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                      │
│     15.3    15.6  0.2675      1.74%   620  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html   │
│     2.88    3.14  0.2642      9.18%   597  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/SetGroupoidComprehension.v.html │
│     23.0    23.2  0.2511      1.09%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html        │
│     32.4    32.7  0.2439      0.75%    12  coq-fourcolor/theories/proof/job439to465.v.html                                           │
│     79.5    79.7  0.2429      0.31%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                   │
│  0.00730   0.244  0.2364   3239.74%   171  coq-mathcomp-analysis/theories/trigo.v.html                                               │
│  0.00205   0.234  0.2320  11295.08%   157  coq-metacoq-erasure/erasure/theories/Typed/ExtractionCorrectness.v.html                   │
│  0.00168   0.234  0.2319  13768.82%   159  coq-metacoq-erasure/erasure/theories/Typed/Erasure.v.html                                 │
│   0.0127   0.242  0.2293   1805.87%   115  coq-mathcomp-analysis/theories/lebesgue_measure.v.html                                    │
│ 0.000862   0.228  0.2272  26353.83%   287  coq-metacoq-erasure/erasure/theories/Typed/Erasure.v.html                                 │
│     25.1    25.4  0.2186      0.87%    12  coq-fourcolor/theories/proof/job223to226.v.html                                           │
│     12.3    12.6  0.2181      1.77%    14  coq-fiat-crypto-with-bedrock/src/Language/IdentifiersGENERATED.v.html                     │
│  0.00329   0.221  0.2173   6616.01%   194  coq-mathcomp-analysis/theories/derive.v.html                                              │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                 │
│                                                                                                                                                 │
│  OLD     NEW     DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    179     174  -4.9875   -2.79%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│    202     200  -2.0027   -0.99%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│   18.4    17.5  -0.9123   -4.97%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                               │
│   65.1    64.2  -0.8523   -1.31%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│    236     235  -0.7563   -0.32%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│   38.6    38.0  -0.5076   -1.32%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                          │
│    133     133  -0.5040   -0.38%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│   22.2    21.7  -0.4815   -2.17%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│ 15.654   15.24  -0.4140   -2.64%  1208  coq-vst/floyd/Component.v.html                                                                          │
│   14.9    14.5  -0.3891   -2.62%  3153  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                                     │
│   22.3    22.0  -0.3736   -1.67%    12  coq-fourcolor/theories/proof/job303to306.v.html                                                         │
│   99.5    99.2  -0.3702   -0.37%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│   4.10    3.75  -0.3492   -8.51%  1127  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERSubobjectClassifier.v.html           │
│   45.8    45.5  -0.3313   -0.72%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                              │
│   24.1    23.7  -0.3217   -1.34%    12  coq-fourcolor/theories/proof/job486to489.v.html                                                         │
│   42.8    42.5  -0.3216   -0.75%   579  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│   11.4    11.1  -0.3153   -2.76%   410  coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html                                    │
│   38.3    38.0  -0.3140   -0.82%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│   64.3    64.0  -0.3119   -0.49%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│   11.8    11.5  -0.3097   -2.61%  2864  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                                     │
│   28.7    28.4  -0.3092   -1.08%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│   2.85    2.55  -0.3079  -10.79%  1001  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│ 33.729  33.424  -0.3050   -0.90%   194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│   4.79    4.49  -0.3016   -6.30%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                       │
│   56.7    56.4  -0.3000   -0.53%   731  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ppedrot · 2025-03-27T10:21:33Z

@coqbot merge now

coqbot-app · 2025-03-27T10:21:37Z

@ppedrot: Please take care of the following overlays:

20371-SkySkimmer-dirpath-full-path.sh

Adapt to rocq-prover/rocq#20371 (object_prefix moved to libobject)

Adapt to rocq-prover/rocq#20371 (dirpath_of_module -> path_of_module)

Adapt to rocq-prover/rocq#20371 (Nametab.dirpath_of_module -> path_of_module)

… returning full_path)

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 18, 2025

SkySkimmer requested review from a team as code owners March 18, 2025 17:04

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 18, 2025

SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Mar 18, 2025

SkySkimmer added a commit to SkySkimmer/QuickChick that referenced this pull request Mar 20, 2025

Adapt to rocq-prover/rocq#20371 (Lib.cwd is full_path)

054dac1

SkySkimmer added a commit to SkySkimmer/coq-dpdgraph that referenced this pull request Mar 20, 2025

Adapt to rocq-prover/rocq#20371 (Nametab.dirpath_of_module -> path_of…

44c0386

…_module)

SkySkimmer added a commit to SkySkimmer/coq-lsp that referenced this pull request Mar 20, 2025

Adapt to rocq-prover/rocq#20371 (object_prefix moved to libobject)

d44f12c

SkySkimmer added a commit to SkySkimmer/coqhammer that referenced this pull request Mar 20, 2025

Adapt to rocq-prover/rocq#20371 (dirpath_of_module -> path_of_module,…

8f94baf

… returning full_path)

SkySkimmer added a commit to SkySkimmer/coq-tactician that referenced this pull request Mar 20, 2025

Adapt to rocq-prover/rocq#20371 (Libnames.dirpath deprecated)

26a0e00

SkySkimmer added a commit to SkySkimmer/vsrocq that referenced this pull request Mar 20, 2025

Adapt to rocq-prover/rocq#20371 (dirpath_of_module -> path_of_module)

5365bba

SkySkimmer added kind: internal API, ML documentation... request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Mar 20, 2025

SkySkimmer added this to the 9.1+rc1 milestone Mar 20, 2025

SkySkimmer force-pushed the dirpath-full-path branch from 24e6cc6 to 2460b07 Compare March 20, 2025 14:54

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 20, 2025

ppedrot self-assigned this Mar 20, 2025

LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Mar 21, 2025

Merge pull request #96 from SkySkimmer/dirpath-full-path

b8be788

Adapt to rocq-prover/rocq#20371 (Libnames.dirpath deprecated)

liyishuai pushed a commit to SkySkimmer/QuickChick that referenced this pull request Mar 24, 2025

Adapt to rocq-prover/rocq#20371 (Lib.cwd is full_path)

fbc1562

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 25, 2025

Remove unused libnames APIs

a420146

SkySkimmer added 10 commits March 25, 2025 14:02

Avoid uselessly going through full_path in funind

dc08138

Slightly simplify code for Ltac recursive definitions

42acdd7

Remove unused internal APIs in lib

965280c

(the synterp side are used by synterp-only functions)

fallback reference printer avoid going through full_path

afffc1e

Move type object_prefix to libobject from nametab

2f3c5e5

Remove unused Lib.oname_prefix

4d0d0b9

Add some full_path APIs

729c382

We deprecated [Libnames.dirpath] because it is confusing when [dirpath_of_path] has a different meaning.

Overlays for increased full_path usage

48ef29b

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 25, 2025

SkySkimmer force-pushed the dirpath-full-path branch from 2460b07 to 48ef29b Compare March 25, 2025 13:03

coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. request: full CI Use this label when you want your next push to trigger a full CI. labels Mar 25, 2025

ppedrot approved these changes Mar 26, 2025

View reviewed changes

coqbot-app bot merged commit fcb3a6a into rocq-prover:master Mar 27, 2025
6 checks passed

ppedrot added a commit to ejgallego/coq-lsp that referenced this pull request Mar 27, 2025

Merge pull request #932 from SkySkimmer/dirpath-full-path

23715b1

Adapt to rocq-prover/rocq#20371 (object_prefix moved to libobject)

ppedrot added a commit to rocq-prover/vsrocq that referenced this pull request Mar 27, 2025

Merge pull request #1068 from SkySkimmer/dirpath-full-path

19417e2

Adapt to rocq-prover/rocq#20371 (dirpath_of_module -> path_of_module)

ppedrot added a commit to rocq-community/coq-dpdgraph that referenced this pull request Mar 27, 2025

Merge pull request #143 from SkySkimmer/dirpath-full-path

f63ff8e

Adapt to rocq-prover/rocq#20371 (Nametab.dirpath_of_module -> path_of_module)

lukaszcz pushed a commit to lukaszcz/coqhammer that referenced this pull request Mar 27, 2025

Adapt to rocq-prover/rocq#20371 (dirpath_of_module -> path_of_module,…

e32de1a

… returning full_path)

SkySkimmer deleted the dirpath-full-path branch March 27, 2025 12:39

Lysxia pushed a commit to QuickChick/QuickChick that referenced this pull request Mar 27, 2025

Adapt to rocq-prover/rocq#20371 (Lib.cwd is full_path)

0ef93d9

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Use full_path for absolute paths more consistently #20371

Use full_path for absolute paths more consistently #20371

Uh oh!

SkySkimmer commented Mar 18, 2025 •

edited

Loading

Uh oh!

ppedrot left a comment

Uh oh!

ppedrot commented Mar 26, 2025

Uh oh!

coqbot-app bot commented Mar 26, 2025

Uh oh!

ppedrot commented Mar 27, 2025

Uh oh!

Uh oh!

coqbot-app bot commented Mar 27, 2025

Uh oh!

Uh oh!

Use full_path for absolute paths more consistently #20371

Use full_path for absolute paths more consistently #20371

Uh oh!

Conversation

SkySkimmer commented Mar 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ppedrot left a comment

Choose a reason for hiding this comment

Uh oh!

ppedrot commented Mar 26, 2025

Uh oh!

coqbot-app bot commented Mar 26, 2025

Uh oh!

ppedrot commented Mar 27, 2025

Uh oh!

Uh oh!

coqbot-app bot commented Mar 27, 2025

Uh oh!

Uh oh!

SkySkimmer commented Mar 18, 2025 •

edited

Loading