Stream: Coq users

Topic: Having trouble installing Coq with opam


view this post on Zulip YoungJu Song (Oct 03 2022 at 15:00):

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

view this post on Zulip Gaëtan Gilbert (Oct 03 2022 at 15:05):

can you run opam with -v (verbose)?

view this post on Zulip Michael Soegtrop (Oct 03 2022 at 19:22):

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.

view this post on Zulip Michael Soegtrop (Oct 03 2022 at 19:23):

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.

view this post on Zulip YoungJu Song (Oct 07 2022 at 09:26):

@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: Jan 28 2023 at 07:30 UTC