Jason Gross 88c10e1de2 testing/coq: ./configure in build for Coq plugins
Fixes #15609

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.

N.B. The value for `--libdir` is taken from `community/dune/APKBUILD`,
but as per
https://github.com/coq/coq/issues/15635#issuecomment-1032476125, it
might be the case that `ocamlfind printconf destdir` is more correct?

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.
2024-01-04 07:00:28 +00:00
..