# 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.14.0 Formal proof management system dune 3.0.3 Fast, portable, and opinionated build system ocaml 4.08.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.08.1 Official release 4.08.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.3 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "arthur.chargueraud@inria.fr" homepage: "https://gitlab.inria.fr/charguer/cfml2" dev-repo: "git+https://gitlab.inria.fr/charguer/cfml2.git" bug-reports: "https://gitlab.inria.fr/charguer/cfml2/-/issues" license: "CC-BY-4.0" synopsis: "The CFML Basis library" description: """ This library provides theoretical foundations for the CFML tool. """ build: [ [make "-C" "lib/coq" "-j%{jobs}%"] ] install: [ [make "-C" "lib/coq" "install"] ] depends: [ "coq" { >= "8.13" } "coq-tlc" { >= "20211215"} ] tags: [ "date:" "logpath:CFML" "category:Computer Science/Programming Languages/Formal Definitions and Theory" "keyword:program verification" "keyword:separation logic" "keyword:weakest precondition" ] authors: [ "Arthur Charguéraud" ] url { src: "https://gitlab.inria.fr/charguer/cfml2/-/archive/20220112/archive.tar.gz" checksum: [ "md5=4bd2f2c9e59a5ba2894aed81c766ef09" "sha512=08778c62243ffe8646377d8e00a7bae3e5a4ee52e6e37410a1e86f39a869f9e07c486df18ae50ba334898e6946355dbb9064aebbfaa89f536ce2672cbe93ae25" ] }
true
Dry install with the current Coq version:
opam install -y --show-action coq-cfml-basis.20220112 coq.8.14.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-cfml-basis.20220112 coq.8.14.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-cfml-basis.20220112 coq.8.14.0
Total: 5 M
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepFunctor.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepSimpl.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepSimpl.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/SepBase.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepFunctor.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/Semantics.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPTactics.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLifted.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPRecord.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLifted.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/SepLifted.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/SepBase.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepFmap.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/Semantics.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/SepLifted.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPBase.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepGroup.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepVar.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPRecord.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepFmap.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepBind.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPTactics.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPBase.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPTactics.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepSimpl.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepFunctor.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLifted.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/Semantics.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPArrayNonlifted.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLibCommon.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/SepBase.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepGroup.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPHeader.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPRecord.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPArray.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/SepLifted.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPBuiltin.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepFmap.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepBind.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPBase.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLib.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepTLCbuffer.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLibCredits.vo
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepVar.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLibCommon.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPArrayNonlifted.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepVar.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepBind.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPBuiltin.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepGroup.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPArrayNonlifted.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPHeader.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPBuiltin.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPArray.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLibCommon.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPArray.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPHeader.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepTLCbuffer.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/LibSepTLCbuffer.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLib.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLib.v
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLibCredits.glob
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/CFML/WPLibCredits.v
opam remove -y coq-cfml-basis.20220112