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
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 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
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
-noinit are required.
I will open a bug report about the
Ali Caglayan has marked this topic as resolved.
Last updated: Jun 05 2023 at 10:01 UTC