With Coq 8.17.0, the presence of
coqc is no longer enough to determine whether a Coq installation is complete, i.e., can be used as an optional dependency (
depopts in opam). What is the recommended way to query
coqc to figure out whether Stdlib is installed?
to give one example,
coq-of-ocaml.2.5.3+4.14 fails build/installation when only
coqc but not Stdlib is installed. It would be nice to recommend a general idiom based on only checking for and running
coqcto figure out whether the complete Coq collection is there.
IIRC coqc -where fails if the stdlib is not there
so maybe something like this?
if ! coqc -where ; then # do installation assuming Coq is not there else # continue assuming coqc and stdlib fi
Yes, to be tested.
right, I was hoping some package maintainer would battle test this once 8.17.0 is actually out on opam
Why did we do the packet split on opam? I wasn't aware it was really ready. I had found a few problems with the local opam files.
Most of them boil down to: something in coq-core are useless without coq-stdlib being around
opam packages in the OCaml repository are basically maintained by volunteers outside Coq core devs. I think it's completely unrealistic to use a different set of packages (such as a
coq package with different requirements/build) in the OCaml repository than what is tested/maintained in the Coq GitHub repo and in the Coq opam repo.
This was the expectation from the beginning that the package split would be done both in opam-coq-archive and in opam-repository as soon as the Dune migration would be complete.
hi @Guillaume Claret we marked the latest release of Coq-of-OCaml as incompatible with the
coq-core opam package, meaning it won't work with Coq 8.17.0. If you do a new release, the advice is to use something like
coqc -where to detect that both
coqc and Stdlib are installed (
coqc could be installed without Stdlib).
@Karl Palmskog OK, thanks for the notice!
Last updated: Nov 29 2023 at 22:01 UTC