search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.83k stars 646 forks source link

Incorrect search order of plugins for Findlib #16406

Closed silene closed 2 years ago

silene commented 2 years ago

When loading a plugin, Coq/Findlib first looks in the system directories and then in the directories specified by option -I on the command line. As a consequence, if a plugin with the same name (e.g., an older version) happens to be installed in a system directory, Coq will load it instead of the one explicitly specified on the command line.

This makes plugin development especially cumbersome. Indeed, one has to first remove any other installed version of the plugin (e.g., opam remove). Otherwise, Coq will silently load an outdated version of the plugin.

I think that replacing ml_path @ opts.pre.ml_includes by opts.pre.ml_includes @ ml_path in Coqargs.build_load_path is sufficient to fix this bug, but I have yet to test it. (This also begs the question of whether vo_path @ opts.pre.vo_includes on the following line suffers from a similar bug.)

Since it involves the Findlib machinery, this bug only exists in Coq 8.16 for now.

ppedrot commented 2 years ago

IMO this is an annoying enough problem to delay a bit the release of Coq 8.16.0.

gares commented 2 years ago

I've seen this bug too, but I'm not so sure the fix is OK. The line of code you point to predates findlib: https://github.com/coq/coq/blame/master/sysinit/coqargs.ml#L451

SkySkimmer commented 2 years ago

I think it's rather the way we initialize findlib which is incorrect https://github.com/coq/coq/blob/7f2e4bfc0ec0e2e6ff24a91e9060933e06c31d46/sysinit/coqinit.ml#L148-L156 If we do -I A -I B ml_load_path is ["A";"B"] (the system load paths are like having some extra -I at the beginning, later -I should have priority) The List.iter (for legacy loading and Drop) is in the correct order, but for the OCAMLPATH env variable we produce $OCAMLPATH:A:B where we should produce B:A:$OCAMLPATH as it wants the highest priority at the beginning. I'll try a PR.

silene commented 2 years ago

We want A:B:$OCAMLPATH, since the de facto standard in the compiler world is to parse -I options left-to-right.