Update Mac OS install instructions #1362
Conversation
|
For reference — these instructions are what worked for me on a clean install of Mac OS Big Sur 11.4. I should be able to test it on Mac OS Catalina 10.15 within a couple of days. If other Mac OS users (@DanGrayson , @maggesi ) have the chance to test them independently, that’d be great! |
INSTALL.md
Outdated
| 3. Install Emacs from https://emacsformacosx.com/. | ||
|
|
||
| Now proceed with [Installation of ProofGeneral](#installation-of-proofgeneral-all-operating-systems) and [Installing UniMath](#installing-unimath) below. | ||
| 2. If the build script later asks you to switch to a specific OCaml version, and/or install extra packages, you can do this with: |
There was a problem hiding this comment.
What "build script" are you referring to here?
There was a problem hiding this comment.
Oh, here's the message:
--- making .coq_makefile_input
--- making sub/coq/config/coq_config.ml because of sub/coq/configure.ml
cd sub/coq && ./configure -coqide "no" -with-doc no -local -no-custom
Your version of OCaml is 4.12.0.
You need a version of OCaml between 4.05 and 4.11.
Configuration script failed!
Makefile:76: .coq_makefile_output.conf: No such file or directoryIn the message, it's referred to as a "configuration script".
There was a problem hiding this comment.
I’ve reworded this in a new commit; hope you think it’s better now. I don’t want to say “the configuration script” because we just tell the user to invoke make, not the config script specifically.
INSTALL.md
Outdated
| Now proceed with [Installation of ProofGeneral](#installation-of-proofgeneral-all-operating-systems) and [Installing UniMath](#installing-unimath) below. | ||
| 2. If the build script later asks you to switch to a specific OCaml version, and/or install extra packages, you can do this with: | ||
| ```bash | ||
| $ opam switch 4.11.0 |
There was a problem hiding this comment.
This won't work until after opam init is run. And after that I get this error:
$ opam switch 4.11.0
[ERROR] No switch 4.11.0 is currently installed. Did you mean 'opam switch create 4.11.0'?
Installed switches are:
- default
There was a problem hiding this comment.
After running that command, it proceeds up to this error:
...
OCAMLOPT -a -o vernac/vernac.cmxa
OCAMLOPT -a -o stm/stm.cmxa
OCAMLOPT -a -o toplevel/toplevel.cmxa
OCAMLC kernel/byterun/coq_fix_code.c
OCAMLC kernel/byterun/coq_memory.c
OCAMLC kernel/byterun/coq_values.c
OCAMLC kernel/byterun/coq_interp.c
cd kernel/byterun/ && \
"/usr/local/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o
COQMKTOP -o bin/coqtop.opt
File "topbin/coqtop_bin.ml", line 11, characters 20-32:
11 | let drop_setup () = Mltop.remove ()
^^^^^^^^^^^^
Error: Unbound module Mltop
make[2]: *** [Makefile.build:422: bin/coqtop.opt] Error 2
make[2]: Leaving directory '/Users/dan/src/ProofChecking/UniMath/UniMath.git/sub/coq'
make[1]: *** [Makefile.make:178: submake] Error 2
make[1]: Leaving directory '/Users/dan/src/ProofChecking/UniMath/UniMath.git/sub/coq'
Makefile:76: .coq_makefile_output.conf: No such file or directory
make: *** [Makefile:244: sub/coq/bin/coq_makefile] Error 2There was a problem hiding this comment.
Re opam switch create — thanks, I’d been sloppy transcribing my notes. Fixed, hopefully.
Regarding your Error: Unbound module Mltop: Did you manage to troubleshoot this? My guess would have been files left around from previous compilations, so I’d try running git clean -Xfd and git submodule foreach git clean -Xfd and then re-running make (but of course you know that as well as I do). If that fixes it, then I don’t think we need to mention it here — it’s unlikely to occur for first-time users, not OS-specific, and we already mention git clean as a troubleshooting tip below. If it seems more OS-specific though then yes, we should try to pre-emptively avert it or give a fix!
There was a problem hiding this comment.
No, at that point I just stopped. It looks vaguely familiar. I'll try to troubleshoot it.
(I did git cleans, as usual.)
| ```bash | ||
| $ opam init | ||
| $ eval $(opam env) | ||
| $ opam switch create 4.11.0 |
There was a problem hiding this comment.
This gives an error if the switch has been created previously.
| ```bash | ||
| $ opam init | ||
| $ eval $(opam env) | ||
| $ opam switch create 4.11.0 |
There was a problem hiding this comment.
If this command works, then one has to run eval $(opam env) again.
|
Hmm, here is a prior problem: $ opam install num ocamlfind
The following actions will be performed:
∗ install ocamlfind 1.9.1
∗ install num 1.4
===== ∗ 2 =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[num.1.4] found in cache
[ocamlfind.1.9.1] found in cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[ERROR] The compilation of ocamlfind failed at "/Users/dan/.opamroot/opam-init/hooks/sandbox.sh build make all".
#=== ERROR while compiling ocamlfind.1.9.1 ====================================#
# context 2.0.8 | macos/x86_64 | ocaml-system.4.12.0 | https://opam.ocaml.org#a86de59f
# path ~/.opamroot/default/.opam-switch/build/ocamlfind.1.9.1
# command ~/.opamroot/opam-init/hooks/sandbox.sh build make all
# exit-code 2
# env-file ~/.opamroot/log/ocamlfind-39360-d0f245.env
# output-file ~/.opamroot/log/ocamlfind-39360-d0f245.out
### output ###
# [...]
# fi
# ocamldep *.ml *.mli >depend
# ocamlc -I +compiler-libs -opaque -g -c findlib_config.ml
# ocamlc -I +compiler-libs -opaque -g -c fl_split.ml
# ocamlc -I +compiler-libs -opaque -g -c fl_metatoken.ml
# ocamlc -I +compiler-libs -opaque -g -c fl_meta.ml
# File "fl_meta.ml", line 1:
# Error: Invalid import of Fl_metatoken, compiled with -unsafe-string.
# This compiler has been configured in strict safe-string mode (-force-safe-string)
# make[1]: *** [Makefile:165: fl_meta.cmo] Error 2
# make[1]: Leaving directory '/Users/dan/.opamroot/default/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
# make: *** [Makefile:14: all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
┌─ The following actions failed
│ λ build ocamlfind 1.9.1
└─
╶─ No changes have been performed |
|
Paradoxically, if I explicitly compile fl_metatokens with safe strings, the next step works: gallium$ cd /Users/dan/.opamroot/4.11.0/.opam-switch/sources/ocamlfind.1.9.1/src/findlib/
gallium$ ocamlc -I +compiler-libs -opaque -safe-string -g -c fl_metatoken.ml
gallium$ ocamlc -I +compiler-libs -opaque -g -c fl_meta.ml |
|
We had the same problem a year ago: #1315 (comment) |
|
Switching to |
|
@peterlefanulumsdaine @DanGrayson Thanks for your work on this PR so far. I would like to suggest using the easier installation route that @DanGrayson uses in #1437:
This has worked well for Julian (who previously wrote to the mailing list at https://groups.google.com/g/univalent-mathematics/c/hb6u_yxJqzY). |
|
Closing this old PR — it’s obsolete, superseded by #1437, which substantially changed and simplified the build process and updated the instructions to match. |
Addresses #1360 : bring the Mac OS install instructions up-to-date. Several changes:
camlp5and the CoqIDE packagesAnother minor change, while I was working on
INSTALL.md: fixed spelling of Proof General throughout (it’s two words not one: https://proofgeneral.github.io)