Path cannot be guessed when only coq-core is installed

[LasseBlaauwbroek]

If I only have coq-core installed, given MyCoqFile.v

Declare ML Module "ltac_plugin".

Running

coqc -noinit MyCoqFile.v

errors out with

cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.

Adding -boot results in Error: Can't find file ltac_plugin.cmxs on loadpath..
So I have to manually add -coqlib, which is rather tricky because this is system dependent. It seems to me that Coq should be able to detect the location of -coqlib even if coq-stdlib is not installed. Or alternatively, should support be added to coq_makefile and Dune to automatically add the correct argument for -coqlib when the -noinit flag is given?

[ejgallego]

Does that work if you use 8.16 (and the findlib loading syntax)?

[LasseBlaauwbroek]

8.16 doesn't have the package split, so I'm not sure how I can test that?

[LasseBlaauwbroek]

But I tried using findlib loading syntax on master and I get the same error:

Declare ML Module "ltac_plugin:coq-core.plugins.ltac".

[ejgallego]

Oh indeed, sorry @LasseBlaauwbroek , I meant in master, you are correct.

The syntax should be Declare ML Module "coq-core.plugins.ltac" , does that work?

The syntax you used precisely disabled the new lookup method (for some compat cases)

[LasseBlaauwbroek]

Great, yes, that works if I use both -noinit and -boot. I think that resolves my issue. But are all these three different ways to load ML code documented somewhere?

[LasseBlaauwbroek]

Okay the next problem is with Dune and coqdep:

File "theories/dune", line 1, characters 0-191:
 1 | (coq.theory
 2 |  (name Tactician)
 3 |  (package coq-tactician)
 4 |  (flags -boot -noinit)
 5 |  (libraries
 6 |    coq-tactician.record-plugin
 7 |    coq-tactician.tactics-plugin
 8 |    coq-tactician.ssreflect-plugin
 9 |  )
10 | )
Command [1] exited with code 1:
(cd _build/default/theories && /home/lasse/Documents/Projects/Tactician/coqdev/_opam/bin/coqdep <lots-of-I-flags> -I ../src -R . Tactician -dyndep opt Ltac1.v) > _build/default/theories/Ltac1.v.d
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.

It appears that Dune does not actually pass the correct flags to coqdep?

[LasseBlaauwbroek]

But are all these three different ways to load ML code documented somewhere?

To answer my own question:
https://coq.github.io/doc/master/refman/proof-engine/vernacular-commands.html?highlight=declare%20ml%20module#coq:cmd.Declare-ML-Module

[Alizter]

The coq-core split hasn't really been finished yet. There are still tools (such as coqdep) that rely on the stdlib having been installed.

For coqdep -noinit is a noop and -boot will go searching for standard library files if they are needed.

[LasseBlaauwbroek]

Well, -boot does work for this particular case. It's just that dune does not pass -boot.

Are there any existing tracking issues for the final pieces of the coq-core split?

[LasseBlaauwbroek]

@ejgallego Can I ask you for an opinion on this? Is this a bug in Coqdep or Dune? Or no bug at all? Should I open an issue in Dune?

[Alizter]

@LasseBlaauwbroek This is still a coq bug. There are various code paths that require the presence of coqlib (unintentionally). coqdep is reusing these paying no mind to noinit or boot which causes issues when no coqlib is setup.

[LasseBlaauwbroek]

I'm not convinced that this is true. My output of coqdep with -boot shows no generated dependencies on anything in coq-stdlib.

I see two potential issues with dune

• When I put (boot) in my stanza (which I think is an internal thing for Coq, but whatever), Dune is still magically determining that it needs to compile theories/Init/Prelude.v. Even though coqdep does not indicate that. So it seems that this is somehow hardcoded into Dune.
• When I don't use (boot) but just use (flags -boot -noinit), the -boot flag does not get passed to coqdep, causing it to malfunction. That also seems like a bug in Dune?

[Alizter]

@LasseBlaauwbroek What version of Dune are you using?

[LasseBlaauwbroek]

I'm on 3.4.1

[Alizter]

Would you be able to try an older version like 3.2? There was some broken refactoring with the flags (Dune is passing) recently that we still haven't managed to fix.

I am thinking this PR is the likely culprit: ocaml/dune#5866

But it is also quite possible that this never worked before that. We never really wrote down what -boot and -noinit are supposed to do since they are really for internal use. We should really clear this situation up as more and more users wish to use -noinit but the support from Coq itself and Dune is suboptimal.

[LasseBlaauwbroek]

I tried Dune 3.2.0 and the effect is the same as with 3.4.1.

[ejgallego]

@ejgallego Can I ask you for an opinion on this? Is this a bug in Coqdep or Dune? Or no bug at all? Should I open an issue in Dune?

As you have noticed @LasseBlaauwbroek , Dune does not really support libraries that run before the standard library, except for the (boot) flag, which is specific to Coq's stdlib.

The medium term plan is stop having the Stdlib as a implicit library, but that will require some breaking changes.

I'd suggest opening an issue in the Dune repository with your concrete use case, so we can have the (boot) flag work for you. How does tactician work before the stdlib? Does the stdlib still needs to be compiled after it?

Regarding your questions:

When I put (boot) in my stanza (which I think is an internal thing for Coq, but whatever), Dune is still magically determining that it needs to compile theories/Init/Prelude.v. Even though coqdep does not indicate that. So it seems that this is somehow hardcoded into Dune.

Yes, this is because coqc automatically imports Init.Prelude, so we need to inject this dep in Dune. This could be avoided by requiring people to do From Coq Require Import Prelude. which hopefully happens some day.

When I don't use (boot) but just use (flags -boot -noinit), the -boot flag does not get passed to coqdep, causing it to malfunction. That also seems like a bug in Dune?

coqdep flag set is not compatible with coqc one, so we can't pass flags like that. We could tho make an exception for -boot, but it could be a bit subtle. Likely a (stdlib no) flag could be more useful for Tactician and HoTT, I think. Let's discuss in Dune's tracker.

[LasseBlaauwbroek]

Closing in favour of ocaml/dune#6163