Stream: Coq devs & plugin devs

Topic: Mac failing to build plugins?


view this post on Zulip Jason Gross (Jul 03 2023 at 13:31):

What might cause "ocamlfind: Package `coq-core.plugins.ltac' not found"?
https://github.com/mit-plv/fiat-crypto/issues/1616

view this post on Zulip Pierre-Marie Pédrot (Jul 03 2023 at 13:49):

A wrong OCAMLPATH maybe?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 03 2023 at 14:19):

or a wrong PATH that makes Coq's build system find the wrong ocamlfind

view this post on Zulip Jason Gross (Jul 03 2023 at 15:22):

The reporter says they installed with brew install coq ocaml-findlib coreutils jq, so I doubt there's another ocamlfind lying around.

view this post on Zulip Jason Gross (Jul 03 2023 at 15:22):

What does OCAMLPATH have to be set to in order for this to work?

view this post on Zulip Paolo Giarrusso (Jul 03 2023 at 18:47):

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

view this post on Zulip Paolo Giarrusso (Jul 03 2023 at 18:50):

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

view this post on Zulip Jason Gross (Jul 05 2023 at 05:33):

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

view this post on Zulip Paolo Giarrusso (Jul 05 2023 at 13:25):

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.

view this post on Zulip Jason Gross (Jul 28 2023 at 07:09):

@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)?

view this post on Zulip Jason Gross (Jul 28 2023 at 07:10):

(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"

)

view this post on Zulip Paolo Giarrusso (Jul 28 2023 at 07:14):

Ah https://github.com/Homebrew/homebrew-core/blob/faef1a2ce132e56d627c9b296059816dedaa7f64/Formula/ocaml.rb#L60

view this post on Zulip Paolo Giarrusso (Jul 28 2023 at 07:20):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 28 2023 at 15:24):

No idea how Homebrew works, but as today Coq both needs:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 28 2023 at 15:32):

in the first point, the value of coqcorelib which must contain $coqcorelib/plugins/ltac/ltac_plugin.cmxs etc... is determined as follows:

  1. if the COQCORELIB env var is set, use that value
  2. if not, guess coqlib, which follows the order COQLIB, Coq_config.coqlibsuffix/theories/Init/Prelude.vo, Coq_config.coqlib/theories/Init/Prelude.vo, fail.
  3. Then use as $coqcorelib:
    a. $coqlib if $coqlib/plugins exists (mainly used in local build)
    b. $coqlib/../coq-core in other cases

Note this last rule is a bit clunky, PRs welcome to improve it.

view this post on Zulip Jason Gross (Jul 28 2023 at 15:58):

So I guess we should configure with HOMEBREW_PREFIX but install with prefix? How does homebrew know what files to link?

view this post on Zulip Paolo Giarrusso (Jul 28 2023 at 16:16):

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

view this post on Zulip Michael Soegtrop (Jul 28 2023 at 16:27):

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.

view this post on Zulip Michael Soegtrop (Jul 28 2023 at 16:28):

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.

view this post on Zulip Michael Soegtrop (Jul 28 2023 at 16:30):

(actually I patch it on Linux as well - snap needs it).

view this post on Zulip Michael Soegtrop (Jul 28 2023 at 16:31):

Each executable searches directories upstream from its own binary folder until it finds the marker file and then addresses shared libraries from there.

view this post on Zulip Paolo Giarrusso (Jul 28 2023 at 18:17):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 28 2023 at 21:53):

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 ?

view this post on Zulip Paolo Giarrusso (Jul 28 2023 at 23:54):

AFAICT from my first post here, Coq plugins are neither in HOMEBREW_PREFIX nor available to findlib

view this post on Zulip Jason Gross (Jul 29 2023 at 00:32):

How do packages specify what needs to be linked in to HOMEBREW_PREFIX?

view this post on Zulip Paolo Giarrusso (Jul 29 2023 at 00:43):

Hmm. https://rubydoc.brew.sh/Formula.html#lib-instance_method suggests the whole lib contents should be symlinked... And that seems true?

view this post on Zulip Paolo Giarrusso (Jul 29 2023 at 00:46):

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

view this post on Zulip Paolo Giarrusso (Jul 29 2023 at 00:49):

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

view this post on Zulip Paolo Giarrusso (Jul 29 2023 at 01:01):

New theory with experiments

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

Details for OCaml expert to check

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

view this post on Zulip Paolo Giarrusso (Jul 29 2023 at 01:09):

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

view this post on Zulip Paolo Giarrusso (Jul 29 2023 at 02:07):

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

view this post on Zulip Jason Gross (Jul 29 2023 at 04:02):

@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: Jul 13 2024 at 03:01 UTC