Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/InstallingCoq.md

Created August 24, 2018 15:44
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Blaisorblade/a213082531307bdeb2f8efc4fb36eff7 to your computer and use it in GitHub Desktop.
Save Blaisorblade/a213082531307bdeb2f8efc4fb36eff7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
InstallingCoq.md

What I did to install Coq 8.8.1 with equations 1.1 as a separate profile:

opam switch coq-8.8.1 --alias-of 4.06.1
eval `opam config env`
opam pin add coq 8.8.1
opam pin add coq-equations 1.1+8.8
opam install ott coq-ott
(opam pin -y add coq-equations 1.1+8.8 && opam install -y ott coq-ott)

I lack notes, but you can repeat opam switch profileName --alias-of 4.06.1 more times with different profileName and install different package versions.

Sadly this rebuilds Coq each time, even if you build two profiles with the same Coq version but different plugins. IIRC, I tried to do opam switch coq-8.8.1-A.A --alias-of coq-8.8.1, but that seemed unsupported.

References: Manage your Coq projects like a pro - opam: https://blog.zhenzhang.me/2016/09/19/coq-dev.html (stopped working :-(, maybe in some archive?) http://ssr.msr-inria.inria.fr/~gares/www/dest/node/31.html

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment