I'm doing tests with building coq-core separately in nixpkgs. An issue that I'm going to encounter is that I need to tell coq-core where the coq-stdlib package is going to be located, but I cannot predict this because providing the value in the coq-core derivation would change the location of coq-stdlib. I guess if I really wanted to do this, I would need to wrap all the Coq commands to pass the right `-coqlib`

or `COQLIB`

value.

Anyway, even before encountering this issue, I found another one which may not be specific to Nix: when running coqtop, I get the following message:

```
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.
```

and that's the case *even* if I run coqtop with `-boot`

and `-noinit`

! (why `-boot`

is needed BTW? I don't think it used to be)

Has someone tried to run the coqtop binary installed with the `coq-core`

opam package without the `coq-stdlib`

package?

Not since the switch to full dune build, but it happens to me from time to time to run coqc without library around. Until then it was not necessary to pass the -boot option AFAIR, but maybe this was changed with the dune consolidation PR.

Actually, I guess that if the `coq-stdlib`

package is installed, only `-noinit`

is needed, because Coq can still bind `Coq.`

to the stdlib, whereas if it cannot be found, it makes sense that both `-boot`

and `-noinit`

are required.

I will open a bug report about the `coqtop`

issue.

https://github.com/coq/coq/issues/16276

https://github.com/coq/coq/pull/16279

Ali Caglayan has marked this topic as resolved.

Last updated: Oct 12 2024 at 12:01 UTC