Coq's Homebrew source build can no longer find zarith

[tchajed]

Description of the problem

brew install --build-from-source coq no longer works, complaining that zarith cannot be found. The Homebrew formula depends on a formula ocaml-zarith, which used to work but no longer does. I suspect this is not a bug in Coq per se (more likely something to do with one of the build tools), but hopefully a Coq developer could take a look.

I did a bit of debugging with brew install --build-from-source --debug coq and the same issue appears with both make world (as the formula does) and dune build.

This bug prevented me from bumping Coq to 8.15.1 in Homebrew.

Coq Version

Coq 8.15.0 (the version packaged by Homebrew) has this problem, as does 8.15.1.

[txyyss]

I tried to build from source without homebrew. It also failed with error message: zarith not found.
Here is the error message:

Shengyi:coq-8.15.1$ make
/Library/Developer/CommandLineTools/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build 
MKDIR     BUILD_OUT
DUNE      _build/default/tools/flock/coq_flock.exe
DUNE      _build/install/default/bin/coqdep
DUNE      sources
COQDEP    VFILES
DUNE      sources
DUNE      _build/install/default/bin/coqc
File "interp/dune", line 6, characters 12-18:
6 |  (libraries zarith pretyping))
                ^^^^^^
Error: Library "zarith" not found.
-> required by library "coq-core.interp" in _build/default/interp
-> required by executable coqc_bin in topbin/dune:24
-> required by _build/default/topbin/coqc_bin.exe
-> required by _build/install/default/bin/coqc
make[1]: *** [_build/install/default/bin/coqc] Error 1
make: *** [submake] Error 2

I also looked at the _build/log:

# dune build --display=quiet --release _build/install/default/bin/coqc
# OCAMLPARAM: unset
# Shared cache: disabled
# Workspace root: /Users/shengyiwang/Downloads/coq-8.15.1
# Auto-detected concurrency: 10
$ /opt/homebrew/bin/ocamlc.opt -config > /var/folders/t6/8jmn6tb96933rz0sxr3bc9b40000gn/T/dune_3d35da_output
# Dune context:
#  { name = "default"
#  ; kind = "default"
#  ; profile = Release
#  ; merlin = true
#  ; for_host = None
#  ; fdo_target_exe = None
#  ; build_dir = "default"
#  ; toplevel_path = None
#  ; ocaml_bin = External "/opt/homebrew/bin"
#  ; ocaml = Ok External "/opt/homebrew/bin/ocaml"
#  ; ocamlc = External "/opt/homebrew/bin/ocamlc.opt"
#  ; ocamlopt = Ok External "/opt/homebrew/bin/ocamlopt.opt"
#  ; ocamldep = Ok External "/opt/homebrew/bin/ocamldep.opt"
#  ; ocamlmklib = Ok External "/opt/homebrew/bin/ocamlmklib.opt"
#  ; env =
#      map
#        { "CAML_LD_LIBRARY_PATH" :
#            "/Users/shengyiwang/Downloads/coq-8.15.1/_build/install/default/lib/stublibs"
#        ; "DUNE_OCAML_HARDCODED" : "/opt/homebrew/lib"
#        ; "DUNE_OCAML_STDLIB" : "/opt/homebrew/lib/ocaml"
#        ; "DUNE_SOURCEROOT" : "/Users/shengyiwang/Downloads/coq-8.15.1"
#        ; "INSIDE_DUNE" :
#            "/Users/shengyiwang/Downloads/coq-8.15.1/_build/default"
#        ; "OCAMLFIND_IGNORE_DUPS_IN" :
#            "/Users/shengyiwang/Downloads/coq-8.15.1/_build/install/default/lib"
#        ; "OCAMLPATH" :
#            "/Users/shengyiwang/Downloads/coq-8.15.1/_build/install/default/lib"
#        ; "OCAMLTOP_INCLUDE_PATH" :
#            "/Users/shengyiwang/Downloads/coq-8.15.1/_build/install/default/lib/toplevel"
#        ; "OCAML_COLOR" : "always"
#        ; "OPAMCOLOR" : "always"
#        }
#  ; findlib_path = [ External "/opt/homebrew/lib" ]
#  ; arch_sixtyfour = true
#  ; natdynlink_supported = true
#  ; supports_shared_libraries = true
#  ; ocaml_config =
#      { version = "4.12.0"
#      ; standard_library_default = "/opt/homebrew/lib/ocaml"
#      ; standard_library = "/opt/homebrew/lib/ocaml"
#      ; standard_runtime = "the_standard_runtime_variable_was_deleted"
#      ; ccomp_type = "cc"
#      ; c_compiler = "clang"
#      ; ocamlc_cflags = [ "-O2"; "-fno-strict-aliasing"; "-fwrapv" ]
#      ; ocamlc_cppflags = [ "-D_FILE_OFFSET_BITS=64"; "-D_REENTRANT" ]
#      ; ocamlopt_cflags = [ "-O2"; "-fno-strict-aliasing"; "-fwrapv" ]
#      ; ocamlopt_cppflags = [ "-D_FILE_OFFSET_BITS=64"; "-D_REENTRANT" ]
#      ; bytecomp_c_compiler =
#          [ "clang"
#          ; "-O2"
#          ; "-fno-strict-aliasing"
#          ; "-fwrapv"
#          ; "-D_FILE_OFFSET_BITS=64"
#          ; "-D_REENTRANT"
#          ]
#      ; bytecomp_c_libraries = [ "-lm"; "-lpthread" ]
#      ; native_c_compiler =
#          [ "clang"
#          ; "-O2"
#          ; "-fno-strict-aliasing"
#          ; "-fwrapv"
#          ; "-D_FILE_OFFSET_BITS=64"
#          ; "-D_REENTRANT"
#          ]
#      ; native_c_libraries = [ "-lm" ]
#      ; native_pack_linker = [ "ld"; "-r"; "-o" ]
#      ; cc_profile = []
#      ; architecture = "arm64"
#      ; model = "default"
#      ; int_size = 63
#      ; word_size = 64
#      ; system = "macosx"
#      ; asm = [ "clang"; "-c"; "-Wno-trigraphs" ]
#      ; asm_cfi_supported = true
#      ; with_frame_pointers = false
#      ; ext_exe = ""
#      ; ext_obj = ".o"
#      ; ext_asm = ".s"
#      ; ext_lib = ".a"
#      ; ext_dll = ".so"
#      ; os_type = "Unix"
#      ; default_executable_name = "a.out"
#      ; systhread_supported = true
#      ; host = "aarch64-apple-darwin21.1.0"
#      ; target = "aarch64-apple-darwin21.1.0"
#      ; profiling = false
#      ; flambda = false
#      ; spacetime = false
#      ; safe_string = true
#      ; exec_magic_number = "Caml1999X029"
#      ; cmi_magic_number = "Caml1999I029"
#      ; cmo_magic_number = "Caml1999O029"
#      ; cma_magic_number = "Caml1999A029"
#      ; cmx_magic_number = "Caml1999Y029"
#      ; cmxa_magic_number = "Caml1999Z029"
#      ; ast_impl_magic_number = "Caml1999M029"
#      ; ast_intf_magic_number = "Caml1999N029"
#      ; cmxs_magic_number = "Caml1999D029"
#      ; cmt_magic_number = "Caml1999T029"
#      ; natdynlink_supported = true
#      ; supports_shared_libraries = true
#      ; windows_unicode = false
#      }
#  }

From the log, we can see it does know the standard_library = "/opt/homebrew/lib/ocaml", zarith is installed there:

Shengyi:_build$ ls /opt/homebrew/lib/ocaml/zarith 
META		big_int_Z.mli	q.cmx		z.cmx		zarith.cmxa
big_int_Z.cmi	libzarith.a	q.mli		z.mli		zarith.cmxs
big_int_Z.cmti	q.cmi		z.cmi		zarith.a	zarith.h
big_int_Z.cmx	q.cmti		z.cmti		zarith.cma	zarith_top.cma

[ejgallego]

That seems like a bug in homebrew, in particular it seems ocamlfind list | grep zarith is not working.

[txyyss]

I don't understand this: ocamlfind list | grep zarith is not working. In my machine, it can find zarith:

Shengyi:~$ ocamlfind list | grep zarith
zarith              (version: 1.12)
zarith.top          (version: 1.12)

Does it find too many?

[Blaisorblade]

ocamlfind needs to find zarith inside the homebrew sandbox. That should filter out installations from opam, and maybe more. @txyyss you'd have to try that inside the "homebrew environment" for interactive builds from source; if I get to a laptop and find time, I can turn this into a concrete brew command. And maybe try myself (unlikely, I don't believe in brew install coq).

[ejgallego]

Seems like a homebrew problem, AFAICT everything is fine in the Coq side.