What might cause "ocamlfind: Package `coq-core.plugins.ltac' not found"?
https://github.com/mit-plv/fiat-crypto/issues/1616
A wrong OCAMLPATH maybe?
or a wrong PATH
that makes Coq's build system find the wrong ocamlfind
The reporter says they installed with brew install coq ocaml-findlib coreutils jq
, so I doubt there's another ocamlfind lying around.
What does OCAMLPATH
have to be set to in order for this to work?
just installed homebrew coq, does this help?
$ OCAMLPATH=/opt/homebrew/Cellar/coq/8.17.1/lib /opt/homebrew/bin/ocamlfind query coq-core.plugins.ltac
/opt/homebrew/Cellar/coq/8.17.1/lib/coq-core/plugins/ltac
$ /opt/homebrew/bin/ocamlfind query coq-core.plugins.ltac
ocamlfind: Package `coq-core.plugins.ltac' not found
$ find /opt/homebrew/Cellar/coq/8.17.1 -name META
/opt/homebrew/Cellar/coq/8.17.1/lib/coq-stdlib/META
/opt/homebrew/Cellar/coq/8.17.1/lib/coqide-server/META
/opt/homebrew/Cellar/coq/8.17.1/lib/coq-core/META
/opt/homebrew/Cellar/coq/8.17.1/lib/coq/META
$ /opt/homebrew/bin/ocamlfind query findlib
/opt/homebrew/lib/ocaml/findlib
$ /opt/homebrew/bin/ocamlfind query zarith
/opt/homebrew/lib/ocaml/zarith
$ ls /opt/homebrew/lib/ocaml/*coq*
gls: cannot access '/opt/homebrew/lib/ocaml/*coq*': No such file or directory
Also, is it normal that you must find OCAMLPATH
for ocamlfind
to find stuff, or are they mispackaging things? Should they add symlinks into /opt/homebrew/lib/ocaml/
?
https://github.com/Homebrew/homebrew-core/blob/faef1a2ce132e56d627c9b296059816dedaa7f64/Formula/coq.rb#L34-L35 suggests extending OCAMLPATH is required on brew, but it seems not actually needed in those cases, and it's not needed with opam packages:
$ echo $OCAMLPATH
$ ocamlfind query findlib
/Users/pgiarrusso1/.opam/4.14.1+flambda/lib/findlib
$ ocamlfind query coq-core.plugins.ltac
/Users/pgiarrusso1/.opam/4.14.1+flambda/lib/coq-core/plugins/ltac
$ ocamlfind query findlib
/Users/pgiarrusso1/.opam/4.14.1+flambda/lib/findlib
(note: I'm a brew user and I'm happy to help here, but I'm not volunteering to contact the homebrew upstream, and I'm not an ocamlfind expert anyway)
Thank you, this does look to me like the Coq brew package is (probably?) misconfigured. I'll try to reproduce on CI and then file a bug with brew-core
That makes sense. FWIW I'd consider opening a discussion first https://github.com/orgs/Homebrew/discussions — they only have 20 issues in https://github.com/Homebrew/homebrew-core/issues, and IME issues are closed much more eagerly (and IMO, aggressively) than in many other projects.
@Paolo Giarrusso (or other Mac users), do you know if there's a difference between prefix
(used in the Coq and dune recipes) and HOMEBREW_PREFIX
(used in findlib and OCaml recipes)?
(actually, the OCaml recipe uses both of them:
args = %W[
--prefix=#{HOMEBREW_PREFIX}
--enable-debug-runtime
--mandir=#{man}
]
system "./configure", *args
system "make", "world.opt"
system "make", "prefix=#{prefix}", "install"
)
Yes, each homebrew package has its own prefix, then files that need to be in the HOMEBREW_PREFIX
get symlinked. Example:
$ ls $HOMEBREW_PREFIX/Cellar/ocaml/4.14.0
Changes INSTALL_RECEIPT.json LICENSE README.adoc bin lib share
$ brew unlink ocaml && brew link ocaml -v
Unlinking /opt/homebrew/Cellar/ocaml/4.14.0... 2417 symlinks removed.
Linking /opt/homebrew/Cellar/ocaml/4.14.0...
ln -s ../Cellar/ocaml/4.14.0/bin/ocaml ocaml
ln -s ../Cellar/ocaml/4.14.0/bin/ocamlc ocamlc
ln -s ../Cellar/ocaml/4.14.0/bin/ocamlc.byte ocamlc.byte
[...]
ln -s ../../Cellar/ocaml/4.14.0/lib/ocaml/weak.ml weak.ml
ln -s ../../Cellar/ocaml/4.14.0/lib/ocaml/weak.mli weak.mli
2417 symlinks created.
No idea how Homebrew works, but as today Coq both needs:
-prefix
to be set to a place where plugins
will be found, otherwise COQCORELIB
needs to be adjusted. This is used to locate plugins in "legacy" mode, i.e. stdlib and ltac. ocamlfind
needs to be working (that is ocamfind query coq-core.plugins.ltac
must work), for plugins in non-"legacy" modein the first point, the value of coqcorelib
which must contain $coqcorelib/plugins/ltac/ltac_plugin.cmxs
etc... is determined as follows:
COQCORELIB
env var is set, use that valuecoqlib
, which follows the order COQLIB
, Coq_config.coqlibsuffix/theories/Init/Prelude.vo
, Coq_config.coqlib/theories/Init/Prelude.vo
, fail.$coqcorelib
:$coqlib
if $coqlib/plugins
exists (mainly used in local build)$coqlib/../coq-core
in other casesNote this last rule is a bit clunky, PRs welcome to improve it.
So I guess we should configure with HOMEBREW_PREFIX but install with prefix? How does homebrew know what files to link?
@Jason Gross homebrew has assumptions like "stuff in prefix/bin must be symlinked", but here you'll have to also add the stuff in lib/ocaml IIUC? It seems findlib and zarith get this right already...
Note that in Coq Platform I patch Ocaml findlib on Mac and Windows. It has an extra mechanism to find shared libraries. See https://github.com/coq/platform/tree/main/opam/opam-repository/packages/ocamlfind/ocamlfind.1.9.5~relocatable.
Unfortunately they didn't want this change upstream. It proved to be fairly stable, though. Essentially it works by putting a marker file (findlib.root) into Coq's root folder and paths are given relative to the folder of this maker file.
(actually I patch it on Linux as well - snap needs it).
Each executable searches directories upstream from its own binary folder until it finds the marker file and then addresses shared libraries from there.
Paolo Giarrusso said:
Jason Gross homebrew has assumptions like "stuff in prefix/bin must be symlinked", but here you'll have to also add the stuff in lib/ocaml IIUC? It seems findlib and zarith get this right already...
okay I checked the formulas and I can't find anything explicit they do to get this right.
Jason Gross said:
So I guess we should configure with HOMEBREW_PREFIX but install with prefix? How does homebrew know what files to link?
I guess it'd be good to first understand why the lookup is failing, I'm unsure the solution you propose would help, aren't the plugins both in HOMEBREW_PREFIX
and prefix
?
AFAICT from my first post here, Coq plugins are neither in HOMEBREW_PREFIX nor available to findlib
How do packages specify what needs to be linked in to HOMEBREW_PREFIX?
Hmm. https://rubydoc.brew.sh/Formula.html#lib-instance_method suggests the whole lib contents should be symlinked... And that seems true?
so, I made a mistake earlier: all in $prefix/lib
is symlinked in all cases, but ocaml-findlib
and ocaml-zarith
puts libraries in lib/ocaml
, while coq
puts them in lib
$ ls /opt/homebrew/Cellar/ocaml-findlib/1.9.6/lib/
ocaml
$ ls /opt/homebrew/Cellar/coq/8.17.1/lib/
coq coq-core coq-stdlib coqide-server stublibs
$ ls /opt/homebrew/lib/coq*
/opt/homebrew/lib/coq:
META dune-package opam theories user-contrib
/opt/homebrew/lib/coq-core:
META boot clib config coqworkmgrapi dune-package engine gramlib interp kernel lib library opam parsing plugins pretyping printing proofs revision stm sysinit tactics tools top_printers toplevel vernac vm
/opt/homebrew/lib/coq-stdlib:
META dune-package opam
/opt/homebrew/lib/coqide-server:
META core dune-package opam protocol
https://docs.brew.sh/Formula-Cookbook#variables-for-directory-locations only notes that stuff in libexec
isn't symlinked — but bin
, share
etc are all documented to be symlinked like lib
It seems homebrew sets tells findlib to find libraries in ${HOMEBREW_PREFIX}/lib/ocaml
instead of ${HOMEBREW_PREFIX}/lib
, then tells working packages to put their libraries in ${HOMEBREW_PREFIX}/lib/ocaml
instead of ${HOMEBREW_PREFIX}/lib
— but the coq
formula isn't doing that.
I tested this theory by unlinking coq, "live-patching" the coq install in-place, and relinking it:
$ brew unlink coq
$ mkdir /opt/homebrew/Cellar/coq/8.17.1/lib/ocaml
$ mv /opt/homebrew/Cellar/coq/8.17.1/lib/* /opt/homebrew/Cellar/coq/8.17.1/lib/ocaml
$ brew link coq
$ /opt/homebrew/bin/ocamlfind query coq-core.plugins.ltac
/opt/homebrew/lib/ocaml/coq-core/plugins/ltac
https://github.com/Homebrew/homebrew-core/blob/0978c7d0eb0593e296dddc555c71e53cb933b258/Formula/ocaml-findlib.rb#L33C1-L33C1 sets "OCAML_SITELIB=#{lib}/ocaml",
aka ${HOMEBREW_PREFIX}/lib/ocaml
, and then the ocaml-zarith
formula passes lib/ocaml
in lots of places including OCAMLFIND_DESTDIR
https://github.com/Homebrew/homebrew-core/blob/faef1a2ce132e56d627c9b296059816dedaa7f64/Formula/ocaml-zarith.rb#L25
of course, since I didn't re-run configure
with the adjusted paths, coq
itself isn't too happy and demands -coqlib
, but that should be fixable
Okay, got a patch where both /opt/homebrew/bin/coqtop
and /opt/homebrew/bin/ocamlfind query coq-core.plugins.ltac
work: https://github.com/Blaisorblade/homebrew-core/pull/1/files. I basically told configure
and dune
to move everything from lib
to lib/ocaml
. Does that make sense?
Maybe somebody would object that having theories
under ocaml
isn't ideal:
$ ls /opt/homebrew/lib/ocaml/coq*
/opt/homebrew/lib/ocaml/coq:
META dune-package opam theories user-contrib
/opt/homebrew/lib/ocaml/coq-core:
META boot clib config coqworkmgrapi dune-package engine gramlib interp kernel lib library opam parsing plugins pretyping printing proofs revision stm sysinit tactics tools top_printers toplevel vernac vm
/opt/homebrew/lib/ocaml/coq-stdlib:
META dune-package opam
/opt/homebrew/lib/ocaml/coqide-server:
META core dune-package opam protocol
@Paolo Giarrusso That patch seems fine to me, but I'm not an expert and maybe @Emilio Jesús Gallego Arias will have an opinion on it
Last updated: Oct 13 2024 at 01:02 UTC