Stop adding user-contrib, xgd dirs and COQPATH to ml loadpath #19842
Conversation
coqbot-app
bot
added
the
needs: full CI
We still add coq-core for coq#15607 (coqc installed in a non-findlib location, typically calling _build/install/default/bin/coqc without going through `dune exec`)
SkySkimmer
added
kind: cleanup
SkySkimmer
force-pushed
the
no-ml-misc-dirs
branch
from
e8620ae to
6b7283d
Compare
coqbot-app
bot
removed
request: full CI
|
Does that mean that findlib will now ignore |
What Coq package is using the "install META next to .vo files" pattern? I guess Gaëtan assumed that this no longer the case. The progress here is that we are (actually already did) phasing out the Coq custom ML library handling infra for Whether this is a good tradeoff is indeed a good question, I think so. |
|
@coqbot bench |
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 63.3940 65.5420 2.1480 3.39% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 65.0110 66.3220 1.3110 2.02% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 3.3180 3.9400 0.6220 18.75% 551 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 34.3130 34.7910 0.4780 1.39% 120 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 46.5890 47.0590 0.4700 1.01% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 182.2850 182.7310 0.4460 0.24% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 119.7600 120.2050 0.4450 0.37% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 16.9000 17.3240 0.4240 2.51% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 36.3150 36.7350 0.4200 1.16% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 20.0540 20.4410 0.3870 1.93% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 38.9300 39.2900 0.3600 0.92% 236 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 26.6890 27.0380 0.3490 1.31% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 42.6500 42.9950 0.3450 0.81% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 22.7180 23.0590 0.3410 1.50% 79 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 32.7540 33.0810 0.3270 1.00% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 23.7850 24.1080 0.3230 1.36% 12 coq-fourcolor/theories/proof/job486to489.v.html │ │ 7.1860 7.5010 0.3150 4.38% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 25.0840 25.3980 0.3140 1.25% 12 coq-fourcolor/theories/proof/job223to226.v.html │ │ 21.6600 21.9680 0.3080 1.42% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 27.8030 28.0990 0.2960 1.06% 12 coq-fourcolor/theories/proof/job107to164.v.html │ │ 0.2650 0.5500 0.2850 107.55% 102 coq-metacoq-erasure/erasure/theories/EOptimizePropDiscr.v.html │ │ 0.2750 0.5560 0.2810 102.18% 111 coq-metacoq-erasure/erasure/theories/ECoInductiveToInductive.v.html │ │ 80.0270 80.3060 0.2790 0.35% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 36.1140 36.3880 0.2740 0.76% 673 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 27.1000 27.3690 0.2690 0.99% 12 coq-fourcolor/theories/proof/job287to290.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 200.4050 197.9550 -2.4500 -1.22% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 7.2190 5.7660 -1.4530 -20.13% 130 coq-category-theory/Functor/Strong/Product.v.html │ │ 5.0040 3.9190 -1.0850 -21.68% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 17.8500 17.2960 -0.5540 -3.10% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 57.0660 56.5510 -0.5150 -0.90% 731 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 38.8540 38.3830 -0.4710 -1.21% 1350 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 46.6240 46.2030 -0.4210 -0.90% 974 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 9.6200 9.2210 -0.3990 -4.15% 345 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 11.5930 11.2020 -0.3910 -3.37% 2103 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 0.9920 0.6430 -0.3490 -35.18% 813 coq-stdlib/MSets/MSetRBT.v.html │ │ 3.4790 3.1610 -0.3180 -9.14% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 5.0000 4.6880 -0.3120 -6.24% 2089 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 235.8000 235.5140 -0.2860 -0.12% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 31.0190 30.7510 -0.2680 -0.86% 12 coq-fourcolor/theories/proof/job254to270.v.html │ │ 0.8600 0.5950 -0.2650 -30.81% 170 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 0.4460 0.1830 -0.2630 -58.97% 128 coq-metacoq-erasure/erasure/theories/ECoInductiveToInductive.v.html │ │ 46.2770 46.0280 -0.2490 -0.54% 110 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 132.9470 132.6990 -0.2480 -0.19% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 94.0620 93.8220 -0.2400 -0.26% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 28.9690 28.7480 -0.2210 -0.76% 12 coq-fourcolor/theories/proof/job589to610.v.html │ │ 0.8150 0.5950 -0.2200 -26.99% 160 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 19.5870 19.3710 -0.2160 -1.10% 12 coq-fourcolor/theories/proof/job507to510.v.html │ │ 23.5340 23.3260 -0.2080 -0.88% 12 coq-fourcolor/theories/proof/job295to298.v.html │ │ 0.7350 0.5330 -0.2020 -27.48% 274 coq-metacoq-erasure/erasure/theories/EGenericMapEnv.v.html │ │ 1.2910 1.0930 -0.1980 -15.34% 27 coq-category-theory/Instance/Cones/Comma.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Mine, for instance. I have never seen the point of polluting the global OCaml namespace with my Coq plugins. Sure, not polluting the global OCaml namespace means that, if someone wanted to build a plugin on top of mine, they would have to set the
This is backward. META files have appeared because we have switched to findlib. Without findlib, there would be no need to store META files in the first place. So, this pull request will not help our switch to findlib, which already happened anyway, as you wrote. |
I'm unsure what to say, @SkySkimmer ? |
|
I think "polluting" is not a fitting description of putting ocaml files in the standard ocaml search path, and "they would have to set the OCAMLPATH environment variable" is an indication that not putting them in the standard search path is a mistake. |
I share this view. IMHO it is reasonable for Coq to fully rely on findlib without extra semantics. This seems clear and simple: "if you want your Coq plugin to work, make sure it is properly configured as a findlib library" Note that there was a discussion about the tradeoffs of relying on findlib, IIRC this downside was discussed. In particular, I think what Coq is doing today is closer to "polluting" OCAMLPATH by adding all these loadpaths that shouldn't be needed (I think the bench allows us to observe that indeed) Plugin authors willing to use a non-standard layout can do so, but they would be responsible of extending the several needed paths to accommodate the custom layout too. @silene I think that if you still don't agree with this PR we can schedule a Coq Call discussion, WDYT? p.s: Note that in
The progress I refer to is about cleaning up code that shouldn't be needed anymore, and in this case cleaning up the paths we add (mostly unnecessarily) to Coq. |
This argument works both ways. Installing Coq plugins inside the global findlib namespace might make Coq faster, but it also makes all the other OCaml programs slower. (And coq/rfcs#101 will make things even worse, since even plugin-free developments will then be installed in the global findlib namespace.) Also, note that I am not the only one to think that it is a poor idea. For example, think about the Nix packagers who are forced to do things like |
How does installing plugins in the regular ocaml library path make other ocaml programs slower?
I am not familiar with this, why do they need to do that? Is that something Coq-specific, or that applies to all OCaml / Dune packages? |
|
Ping @silene |
|
Re-ping @silene Note that I don't thing this could be a serious issue, but it seems large |
|
ping @silene @ejgallego |
|
Since @ejgallego was fine with the PR, I'm going to merge myself, so that we don't get a mess out of merge issues on Monday. @coqbot merge now |
|
I'm indeed fine with merging this, however an important question was not answered:
@silene do you have more information on this. Regarding Nix (cc: @Zimmi48 @vbgl and who else?) , note that indeed findlib becomes slower when [Note that this PR actually makes Coq faster, IIUTC] |
|
There is not much to say. Computers are not magical beasts that can perform any operation in O(1) time. The amount of entries in a directory directly impacts the performance of any program that needs to access anything in it. Even if operating systems work very hard to reduce this cost (B-trees, negative caches, etc), it still far from negligible. For example, Git tries hard to limit the number of entries in |
|
I see @silene , I didn't get you were talking about low-level filesystem performance. In my opinion this is hardly a factor at play here, and the overhead of Coq plugins adding a few more directory entries will be at most in the nanosecond category, so I'm surprised to see a discussion about impact. On the other hand, the impact of longer |
We still add coq-core (actually coq-core/.. du to findlib limitations) for #15607 (coqc installed in a non-findlib location, typically calling _build/install/default/bin/coqc without going through
dune exec)