Skip to content

Use `./configure` before `make dunestrap`

Jason Gross requested to merge jasongross/coq:jasongross-main-patch-22455 into main

As per https://github.com/coq/coq/issues/15635#issuecomment-1032476125, and https://github.com/coq/coq/issues/15452 and https://github.com/coq/coq/issues/18439, if we specify --prefix, we must also pass --libdir to dune install to avoid errors such as ocamlfind: Package `coq-core.plugins.ltac' not found when building Coq plugins.

The value for --libdir is taken from https://github.com/coq/coq/issues/15635#issuecomment-1032476125, but maybe we want to hardcode the same path that was given to dune?

As per https://github.com/coq/coq/issues/15635#issuecomment-1868550860, skipping ./configure is improper, and will cause issues in most layouts with Coq not being able to find its own standard library (apparently the previous configuration was the singular(?) exception).

This should probably go away in a future version of Coq, along with make dunestrap, as per https://github.com/coq/coq/issues/18433#issuecomment-1866922967.

Note that -mandir and -docdir are optional in this instance, since they default to /usr/share/man and /usr/share/doc respectively when -prefix /usr is passed. I included them to immitate the call to dune install below.

See also https://github.com/coq/coq/issues/15635#issuecomment-1868450824 and https://gitlab.alpinelinux.org/alpine/aports/-/merge_requests/57766

The alternative to this would be adding symlinks like

ln -s ../../coq "$pkgdir"/usr/lib/ocaml/coq
ln -s ../../coq-core "$pkgdir"/usr/lib/ocaml/coq-core
ln -s ../../coqide-server "$pkgdir"/usr/lib/ocaml/coqide-server

Let me know if this is preferred.

Edited by Jason Gross

Merge request reports