Théo Zimmermann (Jul 04 2022 at 09:46): Théo Zimmermann (Jul 04 2022 at 09:46):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.
Théo Zimmermann (Jul 04 2022 at 09:47):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)
Théo Zimmermann (Jul 04 2022 at 09:49):Has someone tried to run the coqtop binary installed with the coq-core opam package without the coq-stdlib package?
Pierre-Marie Pédrot (Jul 04 2022 at 09:51):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.
Théo Zimmermann (Jul 04 2022 at 09:54):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.
Théo Zimmermann (Jul 04 2022 at 10:00):I will open a bug report about the coqtop issue.
Théo Zimmermann (Jul 04 2022 at 10:05):https://github.com/coq/coq/issues/16276
Ali Caglayan (Jul 05 2022 at 15:22):https://github.com/coq/coq/pull/16279
Notification Bot (Jul 05 2022 at 15:23):Ali Caglayan has marked this topic as resolved.
Last updated: Apr 20 2024 at 13:01 UTC