Stream: Coq devs & plugin devs

Topic: Detecting Stdlib installation

Karl Palmskog (Mar 29 2023 at 21:06):

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?

Karl Palmskog (Mar 29 2023 at 21:10):

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.

Enrico Tassi (Mar 29 2023 at 21:25):

IIRC coqc -where fails if the stdlib is not there

Karl Palmskog (Mar 29 2023 at 21:32):

so maybe something like this?

if ! coqc -where ; then
  # do installation assuming Coq is not there
else
  # continue assuming coqc and stdlib
fi

Enrico Tassi (Mar 29 2023 at 21:37):

Yes, to be tested.

Karl Palmskog (Mar 29 2023 at 21:39):

right, I was hoping some package maintainer would battle test this once 8.17.0 is actually out on opam

Ali Caglayan (Mar 29 2023 at 22:23):

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.

Ali Caglayan (Mar 29 2023 at 22:23):

Most of them boil down to: something in coq-core are useless without coq-stdlib being around

Karl Palmskog (Mar 30 2023 at 06:43):

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.

Théo Zimmermann (Mar 30 2023 at 07:56):

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.

Karl Palmskog (Mar 31 2023 at 07:06):

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).

Guillaume Claret (Mar 31 2023 at 08:08):

@Karl Palmskog OK, thanks for the notice!

Last updated: Oct 12 2024 at 13:01 UTC