I am using Mac OS Catalina (10.15.5) and have been using opam to install coq without any problem for years.
Recently, opam started to give me the following error. I tried it on fresh (local) opam switch with different OCaml version and for other Coq versions, but I am seeing the same error message. Any advice?
(I am using opam 2.1.3)
~$ opam install coq
The following actions will be performed:
- install coq 8.15.2*
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved coq.8.15.2 (cached)
[ERROR] The compilation of coq.8.15.2 failed at "make COQ_USE_DUNE= -j5".
#=== ERROR while compiling coq.8.15.2 =========================================#
# context 2.1.3 | macos/x86_64 | ocaml-base-compiler.4.13.1 | pinned(https://github.com/coq/coq/archive/refs/tags/V8.15.2.tar.gz)
# path ~/.opam/4.13.1/.opam-switch/build/coq.8.15.2
# command ~/.opam/opam-init/hooks/sandbox.sh build make COQ_USE_DUNE= -j5
# exit-code 2
# env-file ~/.opam/log/coq-10851-bdc7bb.env
# output-file ~/.opam/log/coq-10851-bdc7bb.out
### output ###
# [...]
# [cannot-open-dir,filesystem]
# File "./_build_vo/default//lib/coq/theories/Init/Prelude.v", line 11, characters 0-25:
# Error: Cannot find a physical path bound to logical path Notations.
#
# make[1]: *** [_build_vo/default//lib/coq/theories/Init/Prelude.vo] Error 1
# make[1]: *** [_build_vo/default//lib/coq/theories/Init/Prelude.vo] Deleting file `_build_vo/default//lib/coq/theories/Init/Prelude.glob'
# make[1]: *** Waiting for unfinished jobs....
# (cd _build/default && /Users/youngju.song/.opam/4.13.1/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -o tools/coqworkmgr.exe config/config.cmxa boot/boot.cmxa /Users/youngju.song/.opam/4.13.1/lib/ocaml/str.cmxa -I /Users/youngju.song/.opam/4.13.1/lib/ocaml /Users/youngju.song/.opam/4.13.1/lib/ocaml/unix.cmxa -I /Users/youngju.song/.opam/4.13.1/lib/ocaml /Users/youngju.song/.opam/4.[...]
# ld: warning: directory not found for option '-L/opt/local/lib'
# (cd _build/default && /Users/youngju.song/.opam/4.13.1/bin/ocamlopt.opt -w -40 -rectypes -g -O3 -unbox-closures -o ide/coqide/idetop.exe config/config.cmxa boot/boot.cmxa /Users/youngju.song/.opam/4.13.1/lib/ocaml/str.cmxa -I /Users/youngju.song/.opam/4.13.1/lib/ocaml /Users/youngju.song/.opam/4.13.1/lib/ocaml/unix.cmxa -I /Users/youngju.song/.opam/4.13.1/lib/ocaml /Users/youngju.song/.opam/4[...]
# ld: warning: directory not found for option '-L/opt/local/lib'
# make: *** [submake] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq 8.15.2
+-
- No changes have been performed
can you run opam with -v (verbose)?
The message ld: warning: directory not found for option '-L/opt/local/lib'
likely means that you created your switch with MacPorts installed and then deleted MacPorts.
A common issue on Mac also is auto migrating your data from an x86 Mac to an ARM Mac - this will lead to all sorts of funny effects. If you did something like this, delete MacPorts / Homebrew and reinstall them from scratch.
@Gaëtan Gilbert I tried and I got below (the lower parts are omitted). It seems it is indeed a problem with Mac. When I google the error message, I see many people complaining about the same issue with Mac -- outside opam -- and I will try their proposed fix.) Thanks for the suggestion!
@Michael Soegtrop I haven't migrated from x86 to ARM, but it indeed looks like a problem with Mac. Thanks for the input!
~$ opam pin add coq 8.15.2 -v
[NOTE] Pinning unchanged
coq is now pinned to version 8.15.2
The following actions will be performed:
- install coq 8.15.2*
Do you want to continue? [Y/n] Y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved coq.8.15.2 (cached)
+ /Users/youngju.song/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "-configdir" "/Users/youngju.song/.opam/default/lib/coq/config" "-prefix" "/Users/youngju.song/.opam/default" "-mandir" "/Users/youngju.song/.opam/default/man" "-docdir" "/Users/youngju.song/.opam/default/doc/coq" "-libdir" "/Users/youngju.song/.opam/default/lib/coq" "-datadir" "/Users/youngju.song/.opam/default/share/coq" "-coqide" "no" "-native-compiler" "no" (CWD=/Users/youngju.song/.opam/default/.opam-switch/build/coq.8.15.2)
- You have OCaml 4.14.0. Good!
- You have OCamlfind 1.9.5. Good!
- You have native-code compilation. Good!
- You have the Zarith library 1.12 installed. Good!
- CoqIde manually disabled:
- => no CoqIDE will be built.
-
- Architecture : Darwin
- Sys.os_type : Unix
- OCaml version : 4.14.0
- OCaml binaries in : /Users/youngju.song/.opam/default/bin/
- OCaml library in : /Users/youngju.song/.opam/default/lib/ocaml
- Native dynamic link support : true
- CoqIDE : no
- Documentation : None
- Web browser : open %s
- Coq web site : http://coq.inria.fr/
- Bytecode VM enabled : true
- Native Compiler enabled : no
-
- Paths for true installation:
- - Coq will be copied in /Users/youngju.song/.opam/default
- - the Coq library will be copied in /Users/youngju.song/.opam/default/lib/coq
- - the Coqide configuration files will be copied in /Users/youngju.song/.opam/default/lib/coq/config
- - the Coqide data files will be copied in /Users/youngju.song/.opam/default/share/coq
- - the Coq man pages will be copied in /Users/youngju.song/.opam/default/man
- - documentation prefix path for all Coq packages will be copied in /Users/youngju.song/.opam/default/doc/coq
-
- If anything is wrong above, please restart './configure'.
-
- *Warning* To compile the system for a new architecture
- don't forget to do a 'make clean' before './configure'.
+ /Users/youngju.song/.opam/opam-init/hooks/sandbox.sh "build" "make" "COQ_USE_DUNE=" "-j5" (CWD=/Users/youngju.song/.opam/default/.opam-switch/build/coq.8.15.2)
- /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
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveSum.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveLimits.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveLUB.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveMinMax.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveAbs.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveRealsMorphisms.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructivePower.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
- cp: _build_vo/default//lib/coq/theories/Reals/Abstract/ConstructiveReals.v: No such file or directory
- make[1]: Makefile.build:307: pipe: Too many open files
Last updated: Oct 13 2024 at 01:02 UTC