# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.13.1 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.12.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.1 Official release 4.12.1 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlfind 1.9.6 A library manager for OCaml zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "Laurent.Thery@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" license: "LGPL-2.1-only" synopsis: "Bignums, the Coq library of arbitrary large numbers" description: """ Provides BigN, BigZ, BigQ that used to be part of Coq standard library < 8.6 """ build: [make "-j%{jobs}%" {ocaml:version >= "4.06"}] install: [make "install"] depends: [ "ocaml" "coq" {>= "8.13" & < "8.14~"} ] tags: [ "category:Miscellaneous/Coq Extensions" "category:Mathematics/Arithmetic and Number Theory/Number theory" "category:Mathematics/Arithmetic and Number Theory/Rational numbers" "keyword:integer numbers" "keyword:rational numbers" "keyword:arithmetic" "keyword:arbitrary-precision" "logpath:Bignums" ] authors: [ "Laurent Théry" "Benjamin Grégoire" "Arnaud Spiwack" "Evgeny Makarov" "Pierre Letouzey" ] url { src: "https://github.com/coq/bignums/archive/v9.0.0+coq8.13.tar.gz" checksum: "sha512=b2bf7991eede3d01a3e9410a993b4b192cee6b359d43d208ea92af529b5d342df40fbef1eeaa941a11d1e2117e3d5eb20618f469d63625740c270c0aab6a9876" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-bignums.9.0.0+coq8.13 coq.8.13.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-bignums.9.0.0+coq8.13 coq.8.13.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-bignums.9.0.0+coq8.13 coq.8.13.1
Total: 8 M
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/BigN.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/NMake.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/NMake.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigQ/QMake.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigQ/QMake.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigNumPrelude.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigNumPrelude.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmxs
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/NMake.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.vo
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigQ/QMake.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/BigN.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.glob
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigNumPrelude.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmi
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmx
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigN/BigN.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.v
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmxa
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.v
opam remove -y coq-bignums.9.0.0+coq8.13