(2021-03-31 05:27:10 UTC)
# 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.2 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.1 Official release 4.10.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "Vincent.Laporte@inria.fr" homepage: "https://github.com/coq/bignums" dev-repo: "git+https://github.com/coq/bignums.git" bug-reports: "https://github.com/coq/bignums/issues" authors: [ "Laurent Théry" "Benjamin Grégoire" "Arnaud Spiwack" "Evgeny Makarov" "Pierre Letouzey" ] license: "LGPL-2.1-only" build: [ [make "-j%{jobs}%" {ocaml:version >= "4.06"}] ] install: [ [make "install"] ] depends: [ "ocaml" "coq" {>= "8.11" & < "8.12~"} ] tags: [ "keyword:integer numbers" "keyword:rational numbers" "keyword:arithmetic" "keyword:arbitrary-precision" "category:Miscellaneous/Coq Extensions" "category:Mathematics/Arithmetic and Number Theory/Number theory" "category:Mathematics/Arithmetic and Number Theory/Rational numbers" "logpath:Bignums" ] synopsis: "Bignums, the Coq library of arbitrary large numbers" description: "Provides BigN, BigZ, BigQ that used to be part of Coq standard library < 8.7." url { src: "https://github.com/coq/bignums/archive/V8.11.0.tar.gz" checksum: "sha512=d39cc13f4c399ad9203ae1526cf3deced2f006f137d892d4f9e1be091d9d75ed15c403dd7c2971874f9b71599e9f2ac2a9d960411f6de48875fdf0e0648a14a0" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-bignums.8.11.0 coq.8.11.2
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 2h opam install -y --deps-only coq-bignums.8.11.0 coq.8.11.2
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-bignums.8.11.0 coq.8.11.2
Total: 9 M
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/BigN.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/QMake.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/QMake.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigNumPrelude.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmxs
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigNumPrelude.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.vo
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/QMake.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/BigN.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.glob
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigNumPrelude.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmi
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmx
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigN/BigN.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.v
../ocaml-base-compiler.4.10.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmxa
opam remove -y coq-bignums.8.11.0