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
I guess I can
touch _build/default/coq-doc.install, but that seems kinda weird
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.
Is it possible I have some outdated files somewhere and need to
git clean -xfd?
dune build -p coq-core or whatever the build command is before
Yes, and it succeeded, IIRC
If you have Dune caching enabled, it rarely hurts to do a
git clean -xfd.
@Jason Gross I think your command line should be
dune install --prefix "$HOME/.local64/coq/coq-master/" coq-core without the
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 )
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: Dec 05 2023 at 12:01 UTC