See#1039

I have not reviewed the proposed change in detail yet, but this could be an invasive change, so we should not rush it.

It's rebased onto trunk, so hopefully will pass the CI this time.

I agree - given the comments about initialisation timing in toploop.ml (and the fact that I haven't tested the native toplevel), this change does need reviewing by someone more familiar with the code...

I don't remember how all this toplevel code works, but note the comment in toploop.ml:

(* Toplevel initialization. Performed here instead of at the   beginning of loop() so that user code linked in with ocamlmktop   can call directives from Topdirs. *)

So, I think it's safer to keepCompmisc.init_path false; in the initialization code of Toploop. But it should be OK to re-doCompmisc.init_path false; in Topmain.main so that the command-line flags are taken into account.

To elaborate on my previous comment, the "user code linked in with ocamlmktop" I have in mind is Coq, and more precisely itsDrop. command, which runs a Caml toplevel loop inside Coq for debugging purposes. See section 3.4 ofhttps://coq.inria.fr/cocorico/CoqCustomizationHowTo2006 . The procedure outlined there (compile Coq locally, run coqtop.byte,Drop.,#use "include";;) looks like a good regression test for us.

(Adding@maximedenes to this discussion for his information. No action expected yet.)

@xavierleroy - thanks for the test case! With the original PR, I got an error fromDrop. for being unable to find the standard library, so the PR definitely broke that. With the new commit I just pushed, I get to an OCaml toplevel - I get an error with the#use "include" (with either of theinclude files on offer), but I think that the ability to get to the toploop was the key thing here?

Rebased and squashed.@xavierleroy - are you happy to merge this?