Stream: Coq devs & plugin devs

Topic: installing without sphinx?


view this post on Zulip Jason Gross (Aug 04 2023 at 23:16):

How do I tell coq to install even when the build is broken?

$ dune install --prefix "$HOME/.local64/coq/coq-master/" -p coq-core
Error: The following <package>.install are missing:
- _build/default/coq-doc.install
Hint: try running: dune build [-p <pkg>] @install

view this post on Zulip Jason Gross (Aug 04 2023 at 23:17):

I guess I can touch _build/default/coq-doc.install, but that seems kinda weird

view this post on Zulip Théo Zimmermann (Aug 05 2023 at 09:11):

Sphinx is not part of the coq-core / coq opam packages, so I don't see why you would need the Sphinx dependency / to build this part of the system. The coq-doc opam package is known not to work BTW.

view this post on Zulip Jason Gross (Aug 05 2023 at 22:14):

Is it possible I have some outdated files somewhere and need to git clean -xfd?

view this post on Zulip Gaëtan Gilbert (Aug 05 2023 at 22:21):

did you dune build -p coq-core or whatever the build command is before dune install?

view this post on Zulip Jason Gross (Aug 05 2023 at 23:06):

Yes, and it succeeded, IIRC

view this post on Zulip Théo Zimmermann (Aug 07 2023 at 09:25):

If you have Dune caching enabled, it rarely hurts to do a git clean -xfd.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 08 2023 at 16:34):

@Jason Gross I think your command line should be dune install --prefix "$HOME/.local64/coq/coq-master/" coq-core without the -p, dune install taking the -p is indeed confusing, and comes from a time where dune install would run dune build if needed (cc @Ali Caglayan )

view this post on Zulip Emilio Jesús Gallego Arias (Aug 08 2023 at 16:35):

dune install -p $PKGS will be interpreted as just dune install, that is, it will try to install all packages that dune knows for the workspace.


Last updated: Jun 18 2024 at 00:02 UTC