# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.9.1 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.3 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "palmskog@gmail.com" homepage: "https://github.com/coq-community/pocklington" dev-repo: "git+https://github.com/coq-community/pocklington.git" bug-reports: "https://github.com/coq-community/pocklington/issues" license: "LGPL-2.1-or-later" synopsis: "Pocklington's criterion in Coq" description: """ Coq formalization of Pocklington's criterion for checking primality for large natural numbers. Includes a formal proof of Fermat's little theorem.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "coq" {>= "8.7" & < "8.15~"} ] tags: [ "category:Mathematics/Arithmetic and Number Theory/Number theory" "keyword:Pocklington" "keyword:number theory" "keyword:prime numbers" "keyword:primality" "keyword:Fermat's little theorem" "logpath:Pocklington" "date:2021-01-01" ] authors: [ "Olga Caprotti" "Martijn Oostdijk" ] url { src: "https://github.com/coq-community/pocklington/archive/v8.12.0.tar.gz" checksum: "sha512=e17402d9719321c48bebc41030a5d36f8e1c0e31c3ed399bdce1d2c9a858d02c7890c70dddcc866b8d1937bf44b95516b149a9683908a4920de7cd04e6bd182e" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-pocklington.8.12.0 coq.8.9.1
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-pocklington.8.12.0 coq.8.9.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-pocklington.8.12.0 coq.8.9.1
Total: 1 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/modulo.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/fermat.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/fermat.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/list.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/modulo.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/divides.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/divides.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/lemmas.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/list.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/gcd.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/prime.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/dec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/pock.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/modprime.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/natZ.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/lemmas.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/exp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/order.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/gcd.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/pock.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/Pocklington.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/modprime.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/natZ.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/prime.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/fermat.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/dec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/list.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/modulo.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/exp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/divides.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/order.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/lemmas.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/dec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/gcd.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/pock.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/prime.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/natZ.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/modprime.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/exp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/order.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/Pocklington.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/Pocklington/Pocklington.glob
opam remove -y coq-pocklington.8.12.0