Fix ocamlpath order in findlib init #16428

SkySkimmer · 2022-08-29T11:14:10Z

SkySkimmer · 2022-08-29T11:14:38Z

Anyone know how to make a good test for this?
cc @silene @ppedrot @gares

gares · 2022-08-29T11:17:13Z

I don't have the time, sorry

The way I experience the bug is to run make install and have a plugin installed in ~/.opam/, then change the plugin (adding an assert false), run make, and see things working (since the old copy is found). IMO this is what we should reproduce, but if you start to export OCAMLPATH then you kind of bias the test.

silene · 2022-08-29T11:44:32Z

I think it is impossible to test it in Coq itself. But here is how I tested my patch manually:

foo.ml:

let _ = Mltop.add_known_module "coq-foo.foo"
let () = Printf.printf "foo 1\n%!"

foo.v:

Declare ML Module "coq-foo.foo".

META.coq-foo:

package "foo" (
  directory = "."
  description = "Coq Foo"
  plugin(native) = "foo.cmxs"
)
directory = "."

ocamlfind ocamlopt -package coq-core.toplevel -rectypes -thread -shared foo.ml -o foo.cmxs
coqc -I . foo.v
DIR=$(ocamlfind printconf destdir)/coq-foo
mkdir $DIR
cp foo.cmxs $DIR/
grep -v 'directory *=' META.coq-foo > $DIR/META
coqc foo.v
sed -i -e 's/foo 1/foo 2/' foo.ml
ocamlfind ocamlopt -package coq-core.toplevel -rectypes -thread -shared foo.ml -o foo.cmxs
coqc -I . foo.v

ejgallego · 2022-08-29T12:42:34Z

Anyone know how to make a good test for this?
cc @silene @ppedrot @gares

I think you can set the right env variables (see http://projects.camlcity.org/projects/dl/findlib-1.9.5/doc/ref-html/lib/Findlib.html) to have an alternate tree / config for findlib in the test suite which is reproducible.

silene · 2022-08-29T13:53:16Z

sysinit/coqinit.ml

-    try Sys.getenv "OCAMLPATH" ^ ocamlpathsep ^ ocamlpath
-    with Not_found -> ocamlpath in
+  let env_ocamlpath = try Sys.getenv "OCAMLPATH" :: ml_load_path with Not_found -> ml_load_path in
+  let env_ocamlpath = String.concat ocamlpathsep (List.rev env_ocamlpath) in


As mentioned in the issue, using List.rev is an unfortunate choice, since it causes -I directories to be scanned right-to-left, while the vast majority of compilers (e.g., gcc, ocamlc) use a left-to-right policy.

"Directories specified with -I options are scanned in left-to-right order."

"Directories added with -I are searched [...] in the order in which they were given on the command line"

SkySkimmer · 2022-08-29T14:28:17Z

I guess we don't document the effect of order for -I so either is technically correct, but shouldn't we keep the past behaviour?

SkySkimmer · 2022-08-31T14:38:09Z

Changed: when passed -I A -I B we produce A:B:$OCAMLPATH:$default_dirs (default_dirs is the list of install locations for the core plugins and other such stuff)

ppedrot · 2022-08-31T14:52:22Z

sysinit/coqargs.ml

@@ -448,7 +448,12 @@ let build_load_path opts =
    else
      let coqenv = Boot.Env.init () in
      Coqloadpath.init_load_path ~coqenv in
-  ml_path @ opts.pre.ml_includes ,
+  let ocamlpathsep = if Sys.unix then ':' else ';' in
+  let env_ocamlpath =


Didn't we say that when -boot is set, we don't use OCAMLPATH?

That is the opposite of what I understood.
-boot is about not binding the stdlib, so it is unrelated to OCAMLPATH

Yes, OCAMLPATH should always be used (e.g., critical on Nix). Otherwise, dependencies will not be found.

silene · 2022-08-31T15:27:58Z

Changed: when passed -I A -I B we produce A:B:$OCAMLPATH:$default_dirs (default_dirs is the list of install locations for the core plugins and other such stuff)

Will that not break the compilation of Coq when there is already a release of Coq installed on the system? Indeed, the currently compiled Coq will look for its plugins in $OCAMLPATH instead of $default_dirs and thus will find the wrong versions. (I am assuming that the not yet installed plugins are in $default_dirs.) If so, the order should be A:B:$default_dirs:$OCAMLPATH.

ejgallego · 2022-08-31T16:23:08Z

@silene compilation of Coq has moved to using less implicit stuff, so indeed the standard library is compiled using-boot and explicit -I paths.

ejgallego · 2022-08-31T16:24:26Z

Dune is also scheduled to use -boot for all user developments soon, this allows, among other things, for a crude way to hide selectively what is installed in user-contrib.

gares · 2022-08-31T16:44:04Z

Isn't dune setting OCAMLPATH to point to the _build directory?

ejgallego · 2022-08-31T17:00:00Z

Isn't dune setting OCAMLPATH to point to the _build directory?

Yes, as part of the workspace configuration.

silene · 2022-08-31T17:01:04Z

sysinit/coqargs.ml

+    try String.split_on_char ocamlpathsep (Sys.getenv "OCAMLPATH")
+    with Not_found -> []
+  in
+  opts.pre.ml_includes @ env_ocamlpath @ ml_path ,


Is it on purpose that the content of $OCAMLPATH is passed to Mltop.add_ml_dir? This seems like a very bad idea.

Yes, I think this part should be reverted until we remove the legacy loading method in 8.17

This point came up at the call, but nobody could find the problem. What is it?

What problem?

the content of $OCAMLPATH is passed to Mltop.add_ml_dir? This seems like a very bad idea.

what is the problem when doing that?

The problem is that, on some systems (e.g., Nix), $OCAMLPATH contains the whole world. Thus, when trying to load a legacy plugin, Coq will scan a bunch of directories that are completely unrelated to Coq. (Notice that this pull request scans env_ocamlpath before ml_path, where the legacy plugins lie.) In fact, if by sheer luck Coq were to actually find a plugin with the searched name in one of these directories, it is guaranteed to be a broken one.

OK, then I think @SkySkimmer should avoid this, and that requires changing the API IMO, since you need to separate the paths from OCAMPATH from the others.

I keep the occasion, in case Nix people are listening, to remind that OCAMLPATH is there to let one override the system config, not a place to store it. If they want to stay with env variables, they should add a nix specific one to findlib, eg NIX_OCAMLPATH, and have findlib honor both, giving OCAMLPATH precedence.

You only need to change the API if you want $OCAMLPATH to be searched after opts.pre.ml_includes but before ml_path. But why do you even want that in the first place? Why should the Coq directories in ml_path not take precedence over OCAMLPATH?

remind that OCAMLPATH is there to let one override

because of this? (we may even use this in the CI)

Responding to the off-topic comment:

I keep the occasion, in case Nix people are listening, to remind that OCAMLPATH is there to let one override the system config, not a place to store it. If they want to stay with env variables, they should add a nix specific one to findlib, eg NIX_OCAMLPATH, and have findlib honor both, giving OCAMLPATH precedence.

Nix is using this "trick" in many programming languages that have a PATH environment variable, and has done so successfully for years. If Nix users had had to request changes to most of their programming tools to be able to work, it would have been less successful. The fact that Nix is becoming more and more important and has more and more users does not justify (IMHO) to introduce Nix-specific quirks in generic tools.

Fix coq#16406

SkySkimmer · 2022-09-01T11:46:20Z

changed: findlib sees A:B:$default_dirs:$OCAMLPATH, legacy loading doesn't see OCAMLPATH

gares · 2022-09-01T11:54:31Z

Hum, this way OCAMLPATH cannot be used to override default_dirs, but just to extend them. Was there a problem with default_dirs being last?

Zimmi48 · 2022-09-01T12:11:08Z

Hum, this way OCAMLPATH cannot be used to override default_dirs, but just to extend them. Was there a problem with default_dirs being last?

#16428 (comment)

But I guess, this particular problem was actually resolved by #16428 (comment)

gares · 2022-09-01T12:17:00Z

Hum, so?

ejgallego · 2022-09-01T12:33:05Z

@SkySkimmer adding a test wouldn't hurt, we can simulate a "global" install using the findlib variables, then we can test precedence properly.

sysinit/coqargs.ml

SkySkimmer · 2022-09-01T12:43:36Z

If you want to write a test feel free, I don't have quite enough understanding to do it myself.

ejgallego · 2022-09-01T12:52:27Z

If you want to write a test feel free, I don't have quite enough understanding to do it myself.

I'll open an issue, I don't have time to write the test now, but happy to sheperd.

silene · 2022-09-01T15:47:20Z

doc/sphinx/practical-tools/coq-commands.rst

@@ -184,6 +184,9 @@ and ``coqtop``, unless stated otherwise:
  (``.cmo`` or ``.cmxs``).  Subdirectories are not included.
  See the command :cmd:`Declare ML Module`.

+  Directories added with ``-I`` are searched after the current directory,
+  in the order in which they were given on the command line


Since there is some missing punctuation, we might just as well be comprehensive.

Suggested change

in the order in which they were given on the command line

in the order in which they were given on the command line,

before OCaml's default directories.

I think neither comma is needed.

ejgallego · 2022-09-02T13:52:53Z

@coqbot: merge now

SkySkimmer requested a review from a team as a code owner August 29, 2022 11:14

silene requested changes Aug 29, 2022

View reviewed changes

SkySkimmer force-pushed the ocamlpath-order branch from 24ea74c to c5e01fc Compare August 31, 2022 14:37

SkySkimmer requested a review from silene August 31, 2022 14:38

SkySkimmer force-pushed the ocamlpath-order branch from c5e01fc to c87c455 Compare August 31, 2022 14:42

SkySkimmer requested a review from a team as a code owner August 31, 2022 14:42

ppedrot reviewed Aug 31, 2022

View reviewed changes

silene reviewed Aug 31, 2022

View reviewed changes

SkySkimmer force-pushed the ocamlpath-order branch from c87c455 to 85e0645 Compare August 31, 2022 20:42

Fix ocamlpath order in findlib init

ed8ce2b

Fix coq#16406

SkySkimmer force-pushed the ocamlpath-order branch from 85e0645 to ed8ce2b Compare September 1, 2022 11:45

ejgallego self-assigned this Sep 1, 2022

ejgallego approved these changes Sep 1, 2022

View reviewed changes

ejgallego added this to the 8.16.0 milestone Sep 1, 2022

ejgallego added the kind: fix This fixes a bug or incorrect documentation. label Sep 1, 2022

ejgallego added the part: build The build system. label Sep 1, 2022

ejgallego reviewed Sep 1, 2022

View reviewed changes

sysinit/coqargs.ml Show resolved Hide resolved

ejgallego mentioned this pull request Sep 1, 2022

[test-suite] Missing tests for findlib plugin aliasing #16447

Open

silene approved these changes Sep 1, 2022

View reviewed changes

coqbot-app bot merged commit 6d2a9f2 into coq:master Sep 2, 2022

ppedrot added a commit to ppedrot/coq that referenced this pull request Sep 2, 2022

Backport PR coq#16428: Fix ocamlpath order in findlib init

96b17d2

ppedrot added a commit to ppedrot/coq that referenced this pull request Sep 4, 2022

Backport PR coq#16428: Fix ocamlpath order in findlib init

34ca3c7

SkySkimmer deleted the ocamlpath-order branch September 5, 2022 08:53

ejgallego mentioned this pull request Sep 20, 2024

[coqdep] path relativization doesn't work for some Windows setups #19579

Open

	in the order in which they were given on the command line
	in the order in which they were given on the command line,
	before OCaml's default directories.

Fix ocamlpath order in findlib init #16428

Fix ocamlpath order in findlib init #16428

Conversation

SkySkimmer commented Aug 29, 2022

SkySkimmer commented Aug 29, 2022

gares commented Aug 29, 2022

silene commented Aug 29, 2022 • edited Loading

ejgallego commented Aug 29, 2022

Choose a reason for hiding this comment

SkySkimmer commented Aug 29, 2022

SkySkimmer commented Aug 31, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

silene commented Aug 31, 2022

ejgallego commented Aug 31, 2022

ejgallego commented Aug 31, 2022

gares commented Aug 31, 2022

ejgallego commented Aug 31, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gares Sep 1, 2022 • edited Loading

Choose a reason for hiding this comment

Zimmi48 Sep 1, 2022 • edited Loading

Choose a reason for hiding this comment

SkySkimmer commented Sep 1, 2022

gares commented Sep 1, 2022

Zimmi48 commented Sep 1, 2022 • edited Loading

gares commented Sep 1, 2022

ejgallego commented Sep 1, 2022

SkySkimmer commented Sep 1, 2022

ejgallego commented Sep 1, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ejgallego commented Sep 2, 2022

silene commented Aug 29, 2022 •

edited

Loading

gares Sep 1, 2022 •

edited

Loading

Zimmi48 Sep 1, 2022 •

edited

Loading

Zimmi48 commented Sep 1, 2022 •

edited

Loading