# 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.16.1 Formal proof management system dune 3.12.1 Fast, portable, and opinionated build system ocaml 4.13.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.13.1 Official release 4.13.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 """ build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "ocaml" {>= "4.09"} "coq" {>= "8.16" & < "8.17~"} ] 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" "date:2023-03-15" ] 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.16.tar.gz" checksum: "sha512=3767bec13090517d72dbffe9089199e9a302b8de0cb26e7560932508d4f5b6f30fccb85e9e34b38311de449d5c1beda85207979cde2efa1e4482a865dbffa0b1" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-bignums.9.0.0+coq8.16 coq.8.16.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.16 coq.8.16.1
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-bignums.9.0.0+coq8.16 coq.8.16.1
Total: 8 M
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/BigN.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/NMake.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/NMake.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigQ/QMake.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigQ/QMake.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigNumPrelude.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigNumPrelude.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.vo
../ocaml-base-compiler.4.13.1/lib/coq-bignums/bignums_syntax_plugin.cmxs
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/plugin/bignums_syntax_plugin.cmxs
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDiv.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/NMake.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.vo
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSqrt.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigQ/QMake.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/NMake_gen.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleCyclic.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleMul.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigZ/ZMake.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleDivn1.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleLift.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/Nbasic.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/BigN.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleBase.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleSub.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.glob
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSigZAxioms.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSigNAxioms.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/CyclicDouble/DoubleAdd.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigNumPrelude.v
../ocaml-base-compiler.4.13.1/lib/coq-bignums/bignums_syntax_plugin.cmi
../ocaml-base-compiler.4.13.1/lib/coq-bignums/bignums_syntax_plugin.cmx
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaQ/QSig.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigZ/BigZ.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigN/BigN.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/BigQ/BigQ.v
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/ZSig.v
../ocaml-base-compiler.4.13.1/lib/coq-bignums/bignums_syntax_plugin.cmxa
../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Bignums/SpecViaZ/NSig.v
../ocaml-base-compiler.4.13.1/lib/coq-bignums/META
opam remove -y coq-bignums.9.0.0+coq8.16