Update Mac OS install instructions

[peterlefanulumsdaine]

Addresses #1360 : bring the Mac OS install instructions up-to-date. Several changes:

• remove instructions to install packages that are no longer needed, in particular camlp5 and the CoqIDE packages
• add note about how to switch OCaml versions if needed
• include mention of VSCode as an alternative to Emacs

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

[peterlefanulumsdaine]

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!

[DanGrayson]

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

[DanGrayson]

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

[DanGrayson]

We had the same problem a year ago: https://github.com/UniMath/UniMath/issues/1315#issuecomment-613159280

[DanGrayson]

Switching to 4.09.0 instead of to 4.11.0 fixes both problems. Maybe we should just incorporate that into the instructions, and make switching unconditional.

[benediktahrens]

@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 https://github.com/UniMath/UniMath/pull/1437:

1. Install Coq via homebrew
2. Set the installation of Coq to "no" in the configuration file.

This has worked well for Julian (who previously wrote to the mailing list at https://groups.google.com/g/univalent-mathematics/c/hb6u_yxJqzY).

[peterlefanulumsdaine]

Closing this old PR — it’s obsolete, superseded by #1437, which substantially changed and simplified the build process and updated the instructions to match.