How does one install a new version of Coq when it cannot find the repositories in a new Mac M1 machine?

Asked 14/2, 2022 at 20:20 Answered 15/2, 2022 at 7:27

I got a new machine (mac book m1, not sure if it matters) and I noticed I didn't have Coq:

(base) brandomiranda~ ❯ coqc -v

zsh: command not found: coqc

So I went to the instructions to download coq (https://coq.inria.fr/opam-using.html). Some part of it seems to work:

(base) brandomiranda~ ❯ opam init
eval $(opam env)

<><> Required setup - please read <><><><><><><><><><><><><><><><><><><><><>  🐫

  In normal operation, opam only alters files within ~/.opam.

  However, to best integrate with your system, some environment variables
  should be set. If you allow it to, this initialisation step will update
  your zsh configuration by adding the following line to ~/.zshrc:

    [[ ! -r /Users/brandomiranda/.opam/opam-init/init.zsh ]] || source /Users/brandomiranda/.opam/opam-init/init.zsh  > /dev/null 2> /dev/null

  Otherwise, every time you want to access your opam installation, you will
  need to run:

    eval $(opam env)

  You can always re-run this setup with 'opam init' later.

Do you want opam to modify ~/.zshrc? [N/y/f]
(default is 'no', use 'f' to choose a different file) y
A hook can be added to opam's init scripts to ensure that the shell remains in sync with the opam environment when they are loaded. Set that up? [y/N] y

User configuration:
  Updating ~/.zshrc.

but then when I go get and pin coq opam can't find it:

(base) brandomiranda~ ❯ opam pin add coq 8.15.0
[ERROR] Package coq has no known version 8.15.0 in the repositories

anyone know what is going on? Seems puzzling.

cross: https://coq.discourse.group/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found/1562 https://github.com/coq/platform/issues/219

Getting this issue now:

(base) brandomiranda~ ❯ opam upgrade
[WARNING] Upgrade is not possible because of conflicts or packages that are no longer available:
    - Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

You may run "opam upgrade --fixup" to let opam fix the current state.
(base) brandomiranda~ ❯ opam upgrade --fixup
[ERROR] It appears that the switch invariant is no longer satisfiable. Either fix the package prerequisites or change the invariant with 'opam switch set-invariant'.
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

No solution found, exiting
(base) brandomiranda~ ❯ opam remove ocaml-base-compiler
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

No solution found, exiting

also:

(base) brandomiranda~ ❯ opam info coq

<><> coq: information on all versions <><><><><><><><><><><><><><><><><><><>  🐫
name         coq
all-versions 8.3  8.4pl1  8.4pl2  8.4pl4  8.4.5  8.4.6~camlp4  8.4.6  8.5.0~camlp4  8.5.0  8.5.1  8.5.2~camlp4  8.5.2  8.5.3  8.6  8.6.1  8.7.0  8.7.1  8.7.1+1  8.7.1+2  8.7.2
             8.8.0  8.8.1  8.8.2  8.9.0  8.9.1  8.10.0  8.10.1  8.10.2  8.11.0  8.11.1  8.11.2  8.12.0  8.12.1  8.12.2  8.13.0  8.13.1  8.13.2  8.14.0  8.14.1  8.15.0

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><>  🐫
version      8.15.0
repository   default
url.src      "https://github.com/coq/coq/archive/refs/tags/V8.15.0.tar.gz"
url.checksum "sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3"
homepage     "https://coq.inria.fr/"
bug-reports  "https://github.com/coq/coq/issues"
dev-repo     "git+https://github.com/coq/coq.git"
authors      "The Coq development team, INRIA, CNRS, and contributors."
maintainer   "[email protected]"
license      "LGPL-2.1-only"
depends      "ocaml" {>= "4.05.0"}
             "ocamlfind" {build}
             "dune" {>= "2.5.1"}
             "conf-findutils" {build}
             "zarith" {>= "1.10"}
depopts      "coq-native"
conflicts    "base-nnp" "ocaml-option-nnpchecker"
synopsis     Formal proof management system
description  The Coq proof assistant provides a formal language to write
             mathematical definitions, executable algorithms, and theorems, together
             with an environment for semi-interactive development of machine-checked
             proofs. Typical applications include the certification of properties of programming
             languages (e.g., the CompCert compiler certification project and the
             Bedrock verified low-level programming library), the formalization of
             mathematics (e.g., the full formalization of the Feit-Thompson theorem
             and homotopy type theory) and teaching.

(base) brandomiranda~ ❯ opam switch create NAME 4.07.0

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><>  🐫
Switch invariant: ["ocaml-base-compiler" {= "4.07.0"} | "ocaml-system" {= "4.07.0"}]
[ERROR] Could not determine which packages to install for this switch:
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0 | ocaml-system = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'
    unmet availability conditions: 'sys-ocaml-version = "4.07.0"'


Switch initialisation failed: clean up? ('n' will leave the switch partially installed) [Y/n] Y

seems there was an error:

∗ installed eprover.2.6
[ERROR] The compilation of cairo2.0.6.2 failed at "dune build -p cairo2 -j 16".
∗ installed ocamlgraph.2.0.0
∗ installed zarith.1.12
∗ installed coq-coqprime-generator.dev
∗ installed ocaml-migrate-parsetree.1.8.0
[ERROR] The compilation of z3.4.8.13 failed at "python3 scripts/mk_make.py --ml".
∗ installed menhir.dev
∗ installed ppxlib.0.15.0
∗ installed ppx_deriving.5.1
∗ installed elpi.1.14.1
⬇ retrieved coq-unimath.dev  (git+https://github.com/UniMath/UniMath.git#master)
Processing 188/279: [coq: make]

∗ installed coq.dev
∗ installed coq-dpdgraph.dev
∗ installed coq-hammer-tactics.dev
∗ installed coq-ext-lib.dev
∗ installed coq-aac-tactics.dev
∗ installed coq-libhyps.dev
∗ installed coq-hammer.dev
∗ installed coq-paramcoq.dev
∗ installed coq-menhirlib.dev
∗ installed coq-simple-io.dev
∗ installed coq-bignums.dev
∗ installed coq-unicoq.dev
∗ installed coq-mathcomp-ssreflect.dev
∗ installed coq-hott.dev
∗ installed coq-stdpp.dev
∗ installed coq-flocq.3.dev
∗ installed coq-math-classes.dev
∗ installed coq-coquelicot.dev
∗ installed coq-coqprime.dev
∗ installed coq-equations.dev
∗ installed coq-gappa.dev
∗ installed coq-mathcomp-bigenough.dev
[ERROR] The compilation of coq-interval.dev failed at "./remake -j16".
∗ installed coq-mathcomp-fingroup.dev
∗ installed coq-elpi.dev
∗ installed coq-mtac2.dev
∗ installed coq-mathcomp-finmap.dev
∗ installed coq-hierarchy-builder.dev
∗ installed coq-reglang.dev
∗ installed coq-quickchick.dev
∗ installed coq-compcert.dev
∗ installed coq-iris.dev
∗ installed coq-mathcomp-algebra.dev
∗ installed coq-mathcomp-zify.dev
∗ installed coq-mathcomp-multinomials.dev
∗ installed coq-iris-heap-lang.dev
∗ installed coq-mathcomp-solvable.dev
∗ installed coq-corn.dev
∗ installed coq-mathcomp-field.dev
∗ installed coq-mathcomp-real-closed.dev
∗ installed coq-coqeal.dev
∗ installed coq-mathcomp-character.dev
∗ installed coq-mathcomp-analysis.dev
∗ installed coq-unimath.dev
∗ installed coq-vst.dev

#=== ERROR while compiling z3.4.8.13 ==========================================#
# context              2.1.2 | macos/arm64 | ocaml-base-compiler.4.10.2 | file:///Users/brandomiranda/Downloads/platform-2022.01.0/opam/opam-repository
# path                 ~/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13
# command              ~/.opam/opam-init/hooks/sandbox.sh build python3 scripts/mk_make.py --ml
# exit-code            1
# env-file             ~/.opam/log/z3-96628-ab4f2a.env
# output-file          ~/.opam/log/z3-96628-ab4f2a.out
### output ###
# [...]
# Copied 'z3types.cpython-39.pyc'
# Copied 'z3core.cpython-39.pyc'
# Testing ocamlc...
# Testing ocamlopt...
# Traceback (most recent call last):
#   File "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13/scripts/mk_make.py", line 18, in <module>
#     mk_bindings(API_files)
#   File "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13/scripts/mk_util.py", line 3044, in mk_bindings
#     check_ml()
#   File "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13/scripts/mk_util.py", line 450, in check_ml
#     raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.')
# mk_exception.MKException: 'Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.'


#=== ERROR while compiling coq-interval.dev ===================================#
# context              2.1.2 | macos/arm64 | ocaml-base-compiler.4.10.2 | https://coq.inria.fr/opam/extra-dev#2022-02-15 19:00
# path                 ~/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/coq-interval.dev
# command              ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j16
# exit-code            1
# env-file             ~/.opam/log/coq-interval-96628-942e59.env
# output-file          ~/.opam/log/coq-interval-96628-942e59.out
### output ###
# [...]
# [deprecated-syntactic-definition,deprecated]
# File "./src/Interval/Transcend.v", line 2077, characters 14-24:
# Warning: Notation plus_assoc is deprecated since 8.16.
# The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
# [deprecated-syntactic-definition,deprecated]
# Finished src/Interval/Transcend.vo
# Finished src/Interval/Float_full.vo
# File "./src/Tactic.v", line 22, characters 0-42:
# Warning:
# New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function.
# [ambiguous-paths,typechecker]
# Finished src/Tactic.vo


#=== ERROR while compiling cairo2.0.6.2 =======================================#
# context              2.1.2 | macos/arm64 | ocaml-base-compiler.4.10.2 | https://opam.ocaml.org#28fab8d8
# path                 ~/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/cairo2.0.6.2
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p cairo2 -j 16
# exit-code            1
# env-file             ~/.opam/log/cairo2-96628-a005f1.env
# output-file          ~/.opam/log/cairo2-96628-a005f1.out
### output ###
#   ocamlmklib src/dllcairo_stubs.so,src/libcairo_stubs.a (exit 2)
# (cd _build/default && /Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/bin/ocamlmklib.opt -g -o src/cairo_stubs src/cairo_stubs.o -L/opt/homebrew/opt/freetype/lib -lfreetype -L/opt/homebrew/Cellar/fontconfig/2.13.1/lib -L/opt/homebrew/opt/freetype/lib -lfontconfig -lfreetype -L/opt/homebrew/Cellar/cairo/1.16.0_5/lib -lcairo)
# ld: in '/usr/local/lib/libpng16.16.dylib', building for macOS-arm64 but attempting to link with file built for macOS-x86_64
# clang: error: linker command failed with exit code 1 (use -v to see invocation)



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
┌─ The following actions failed
│ λ build cairo2       0.6.2
│ λ build coq-interval dev
│ λ build z3           4.8.13
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install camlp5                    7.14
│ ∗ install conf-adwaita-icon-theme   2
│ ∗ install conf-autoconf             0.1
│ ∗ install conf-automake             1
│ ∗ install conf-cairo                1
│ ∗ install conf-findutils            1
│ ∗ install conf-g++                  1.0
│ ∗ install conf-gcc                  1.0
│ ∗ install conf-gmp                  4
│ ∗ install conf-gtk3                 18
│ ∗ install conf-gtksourceview3       0+2
│ ∗ install conf-libtool              1
│ ∗ install conf-perl                 2
│ ∗ install conf-pkg-config           2
│ ∗ install conf-python-3             9.0.0
│ ∗ install conf-which                1
│ ∗ install coq                       dev
│ ∗ install coq-aac-tactics           dev
│ ∗ install coq-bignums               dev
│ ∗ install coq-compcert              dev
│ ∗ install coq-coqeal                dev
│ ∗ install coq-coqprime              dev
│ ∗ install coq-coqprime-generator    dev
│ ∗ install coq-coquelicot            dev
│ ∗ install coq-corn                  dev
│ ∗ install coq-dpdgraph              dev
│ ∗ install coq-elpi                  dev
│ ∗ install coq-equations             dev
│ ∗ install coq-ext-lib               dev
│ ∗ install coq-flocq                 3.dev
│ ∗ install coq-gappa                 dev
│ ∗ install coq-hammer                dev
│ ∗ install coq-hammer-tactics        dev
│ ∗ install coq-hierarchy-builder     dev
│ ∗ install coq-hott                  dev
│ ∗ install coq-iris                  dev
│ ∗ install coq-iris-heap-lang        dev
│ ∗ install coq-libhyps               dev
│ ∗ install coq-math-classes          dev
│ ∗ install coq-mathcomp-algebra      dev
│ ∗ install coq-mathcomp-analysis     dev
│ ∗ install coq-mathcomp-bigenough    dev
│ ∗ install coq-mathcomp-character    dev
│ ∗ install coq-mathcomp-field        dev
│ ∗ install coq-mathcomp-fingroup     dev
│ ∗ install coq-mathcomp-finmap       dev
│ ∗ install coq-mathcomp-multinomials dev
│ ∗ install coq-mathcomp-real-closed  dev
│ ∗ install coq-mathcomp-solvable     dev
│ ∗ install coq-mathcomp-ssreflect    dev
│ ∗ install coq-mathcomp-zify         dev
│ ∗ install coq-menhirlib             dev
│ ∗ install coq-mtac2                 dev
│ ∗ install coq-paramcoq              dev
│ ∗ install coq-quickchick            dev
│ ∗ install coq-reglang               dev
│ ∗ install coq-simple-io             dev
│ ∗ install coq-stdpp                 dev
│ ∗ install coq-unicoq                dev
│ ∗ install coq-unimath               dev
│ ∗ install coq-vst                   dev
│ ∗ install cppo                      1.6.8
│ ∗ install csexp                     1.5.1
│ ∗ install dune                      2.9.3
│ ∗ install dune-configurator         2.9.3
│ ∗ install elpi                      1.14.1
│ ∗ install eprover                   2.6
│ ∗ install gmp-ecm                   7.0.3
│ ∗ install menhir                    dev
│ ∗ install menhirLib                 dev
│ ∗ install menhirSdk                 dev
│ ∗ install num                       1.4
│ ∗ install ocaml-compiler-libs       v0.12.4
│ ∗ install ocaml-migrate-parsetree   1.8.0
│ ∗ install ocamlbuild                0.14.1
│ ∗ install ocamlfind                 1.9.3
│ ∗ install ocamlgraph                2.0.0
│ ∗ install ppx_derivers              1.2.1
│ ∗ install ppx_deriving              5.1
│ ∗ install ppxlib                    0.15.0
│ ∗ install re                        1.10.3
│ ∗ install result                    1.5
│ ∗ install seq                       base
│ ∗ install sexplib0                  v0.14.0
│ ∗ install stdlib-shims              0.3.0
│ ∗ install zarith                    1.12
└─

<><> cairo2.0.6.2 troubleshooting <><><><><><><><><><><><><><><><><><><><><>  🐫
=> Try to re-run the install command with PKG_CONFIG_PATH pointing a pkg-config path including libffi, e.g. if you use homebrew you can try
   PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig

The former state can be restored with:
    /opt/homebrew/bin/opam switch import "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/backup/state-20220216165905.export"

when running the coq plataform script:

(base) brandomiranda~/Downloads/platform-2022.01.0 ❯ bash coq_platform_make.sh

Summit answered 14/2, 2022 at 20:20 Comment(11)

Did you opam update? What does opam info coq tell you? – Gianna 14/2, 2022 at 20:28

Updated question with new errors. Seems I have the wrong version of ocaml. Tried uninstalling it but couldn't make it work. Also it does seem to show info about coq...? Unsure how to fix it. I already tried uninstalling ocaml... – Summit 14/2, 2022 at 20:48

I think you need to create a new switch in order to change OCaml versions. See the opam switch manpage. For example, opam switch create NAME 4.07.0. – Underbid 14/2, 2022 at 21:13

@ana-borges I'm confused, what do I do after that? – Summit 15/2, 2022 at 2:35

@ana-borges

opam switch create NAME 4.07.0  <><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><>  🐫 Switch invariant: ["ocaml-base-compiler" {= "4.07.0"} | "ocaml-system" {= "4.07.0"}] [ERROR] Could not determine which packages to install for this switch:   * Missing dependency:     - ocaml-base-compiler = 4.07.0 | ocaml-system = 4.07.0     unmet availability conditions: '!(os = "macos" & arch = "arm64")'     unmet availability conditions: 'sys-ocaml-version = "4.07.0"' Switch initialisation failed: clean up? ('n' will leave the switch partially installed)

– Summit 15/2, 2022 at 2:36

@CharlieParker Ok, that didn't solve the problem. It appears that opam can't install OCaml 4.07.0 on your machine due to unmet conditions, but I don't know why they aren't available. You can try more recent versions of OCaml, or probably what you should actually do is use the Coq Platform scripts as suggested by Zimm i48. – Underbid 15/2, 2022 at 9:10

Indeed @ana-borges, it turns out (from the related Discourse discussion) that only OCaml >= 4.10.2 is compatible with Apple M1. – Horsepowerhour 16/2, 2022 at 17:54

see this gitissue: github.com/coq/platform/issues/219 – Summit 17/2, 2022 at 18:48

what is wrong with doing opam repo add coq-released then https://coq.inria.fr/opam/released opam install coq? – Summit 8/6, 2022 at 17:6

related for a specific version of coq: #54395010 – Summit 8/6, 2022 at 18:25

related: #54122227 – Summit 8/6, 2022 at 18:30

If you are not an opam / OCaml expert, then you're best bet to install Coq with opam is to rely on the scripts provided by the Coq Platform. See: https://github.com/coq/platform/releases

These interactive scripts will take care of:

creating a new opam switch
installing an appropriate version of the OCaml compiler
installing any external dependencies you need (e.g., if you want CoqIDE)
they can also propose to install a collection of additional Coq packages that can be useful for Coq projects

Finally, relying on this script creates a sound basis that you can later extend if you need more Coq packages that were not included in the Platform.

Horsepowerhour answered 15/2, 2022 at 7:27 Comment(11)

I'm confused, is what your suggesting to use this dmg github.com/coq/platform/releases/download/2022.01.0/… then why does the coq page seem to suggest to use Opam? (though I would like to learn to use opam I admit) – Summit 15/2, 2022 at 18:52

I guess I got confused because of this page coq.inria.fr/opam-using.html so opam isn't the recommended way to install Coq (especially if I want to use it outside of the coqide e.g. emacs, vscode) – Summit 15/2, 2022 at 19:5

This page recommends binary installers for beginners or platform scripts for experienced users. What I mentioned in my answer are the Platform scripts, not the binary installers. They are a good place to start using opam because they will create a good opam configuration for you that you can then learn to extend. The page you link to also talk about the Platform scripts as the recommended solution. – Horsepowerhour 15/2, 2022 at 20:59

ok got it. Coq installation scripts. However, given that my machine is in a weird situation -- was restored from a intel time machine but the hardware is the M1. How do I unistall and removing everything and essentially start from scratch? Then I assume the script you suggest are ok to do. Right? – Summit 16/2, 2022 at 16:46

In principle, the Platform scripts are safe to run even if you have other switches around, including some that might be in a weird situation. But removing everything first (rm -rf ~/.opam) is always an option of course. – Horsepowerhour 16/2, 2022 at 17:55

weird I did run the coq plataform scripts...but got errors (see question detaios). The coqc -v doesn't think coqc exists...any idea what to do? – Summit 16/2, 2022 at 18:49

Something that I didn't notice initially but that was noted by Michael here is that you seem to have selected the "dev" variant. Try any other release (such as Coq 8.14, which should be the default) and you will get fewer failures. As for getting coqc -v to work, I would expect that you just need to re-run eval $(opam env) first. – Horsepowerhour 16/2, 2022 at 21:6

indepedently discovered that after running eval $(opam ev) coqc started working...mysterious! – Summit 17/2, 2022 at 16:25

When you installed opam, it asked if it should alter your environment or if you prefer to load it every time with eval $(opam env). It seems that you chose the latter. – Horsepowerhour 17/2, 2022 at 17:9

btw this gitissue: github.com/coq/platform/issues/219 looks useful – Summit 17/2, 2022 at 18:48

what is wrong with doing opam repo add coq-released then https://coq.inria.fr/opam/released opam install coq? – Summit 8/6, 2022 at 17:6

In case you are confsued what "install with the Coq Platform scripts" means here is a few more details:

Installing Coq

install brew: https://brew.sh/
Follow the Coq Platform scripts for installation: https://coq.inria.fr/opam-using.html or "Installation by compiling from Sources using opam" https://github.com/coq/platform/blob/main/doc/README_macOS.md.

Last time I installed this I downloaded their coq zip file with the instlal script (note check for most recent or version you want e.g. at https://github.com/coq/platform/blob/main/doc/README_macOS.md):

https://github.com/coq/platform/archive/refs/tags/2022.01.0.zip

and ran after cding to the unzipped files location of the above:

bash coq_platform_make.sh

select the version you want (likely something stable! Avoid, beta, dev. At the time of this writing option 7.

you might have to do eval $(opam env).
Check it installed correctly:

coqc -v

output something like:

The Coq Proof Assistant, version 8.16+alpha
compiled with OCaml 4.10.2

if its working

Note, for HPCs

it seems one can do this too:

# - install opam
# brew install opam
# https://mcmap.net/q/1925306/-how-does-one-install-opam-with-conda-for-mac-apple-os-x
conda install -c conda-forge opam
opam init
# if doing local env? https://mcmap.net/q/1772957/-what-does-eval-opam-env-do-does-it-activate-a-opam-environment-duplicate
#eval $(opam env)

# - install coq
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq

Summit answered 14/2, 2022 at 20:20 Comment(2)

see this gitissue: github.com/coq/platform/issues/219 – Summit 17/2, 2022 at 18:47

how do you install a specific version of Coq with opam? – Summit 8/6, 2022 at 18:23

Hot tags

Godot Unity Godot Help Programming Godot 4.X GUI GDScript 3D 2D Physics CSharp Godot 3.X VR XR Projects C++

Installing Coq

Note, for HPCs

Recommended topics

Hot tags