Use `./configure` before `make dunestrap`
- Dec 24, 2023
-
-
Jason Gross authored
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
7301a086
-