# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils coq 8.11.0 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "thery@sophia.inria.fr" homepage: "https://github.com/thery/coqprime" bug-reports: "https://github.com/thery/coqprime/issues" dev-repo: "git+https://github.com/thery/coqprime.git" license: "LGPL" authors: ["Laurent Thรฉry"] build: [ ["./configure.sh"] [make "-j%{jobs}%"] ] install: [ [make "install"] ] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Coqprime"] depends: [ "ocaml" "coq" {>= "8.8~" & < "8.12"} "coq-bignums" ] synopsis: "Certifying prime numbers in Coq" flags: light-uninstall url { src: "https://github.com/thery/coqprime/archive/v8.8.zip" checksum: "md5=3430856778d10abe378fbdd385ac834d" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-coqprime.1.0.3 coq.8.11.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-coqprime.1.0.3 coq.8.11.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-coqprime.1.0.3 coq.8.11.0
Total: 25 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/examples/BasePrimes.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/examples/BasePrimes.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/examples/BasePrimes.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/montgomery.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/SMain.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Mod_op.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Pock.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/ZEll.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/montgomery.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Mod_op.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/SMain.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/NEll.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/ZEll.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/PocklingtonCertificat.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Pmod.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/NEll.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Pocklington.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Pock.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/EGroup.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/EGroup.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/LucasLehmer.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/PocklingtonCertificat.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/Permutation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Lucas.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/GZnZ.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/LucasLehmer.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZSum.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/PGroup.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZCAux.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Pmod.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Cyclic.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Lucas.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Zp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/W.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Root.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZSum.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZCmisc.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/UList.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Pocklington.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/SMain.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/PGroup.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/ListAux.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/IGroup.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Proth.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Cyclic.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Root.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Zp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/Permutation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Pepin.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Bits.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/montgomery.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/ZEll.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZCAux.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/FGroup.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/Iterator.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Mod_op.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Euler.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/ZProgression.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/MEll.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/IGroup.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Lagrange.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/examples/PocklingtonRefl.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/MEll.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Ppow.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Pock.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Zmod.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/UList.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/GZnZ.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/NEll.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Lagrange.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/ListAux.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/N/NatAux.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/Iterator.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/EGroup.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/PocklingtonCertificat.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/LucasLehmer.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Pmod.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/FGroup.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/W.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Pepin.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Proth.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/Permutation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZCmisc.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Lucas.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Bits.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/ZProgression.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Zp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZSum.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Euler.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/PGroup.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZCAux.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Pocklington.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Zmod.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Cyclic.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/UList.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Root.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Tactic/Tactic.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/IGroup.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/ListAux.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/elliptic/GZnZ.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Ppow.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Lagrange.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/W.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/Iterator.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/N/NatAux.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/ZCmisc.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Pepin.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/FGroup.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Proth.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/List/ZProgression.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/MEll.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/PrimalityTest/Euler.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Tactic/Tactic.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/num/Bits.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/N/NatAux.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Zmod.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Tactic/Tactic.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/Z/Ppow.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/examples/PocklingtonRefl.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Coqprime/examples/PocklingtonRefl.glob
opam remove -y coq-coqprime.1.0.3