# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq dev The Coq Proof Assistant coq-core dev The Coq Proof Assistant -- Core Binaries and Tools coq-stdlib dev The Coq Proof Assistant -- Standard Library coqide-server dev The Coq Proof Assistant, XML protocol server dune 3.12.2 Fast, portable, and opinionated build system ocaml 5.0.0 The OCaml compiler (virtual package) ocaml-base-compiler 5.0.0 Official release 5.0.0 ocaml-config 3 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: "FCSL <fcsl@software.imdea.org>" homepage: "http://software.imdea.org/fcsl/" bug-reports: "https://github.com/imdea-software/fcsl-pcm/issues" dev-repo: "git+https://github.com/imdea-software/fcsl-pcm.git" license: "Apache-2.0" build: [ make "-j%{jobs}%" ] install: [ make "install" ] depends: [ "coq" {>= "8.11"} "coq-mathcomp-ssreflect" {>= "1.11.0"} "coq-mathcomp-algebra" ] tags: [ "keyword:separation logic" "keyword:partial commutative monoid" "category:Computer Science/Data Types and Data Structures" "logpath:fcsl" ] authors: [ "Aleksandar Nanevski" ] synopsis: "Partial Commutative Monoids" description: """ The PCM library provides a formalisation of Partial Commutative Monoids (PCMs), a common algebraic structure used in separation logic for verification of pointer-manipulating sequential and concurrent programs. The library provides lemmas for mechanised and automated reasoning about PCMs in the abstract, but also supports concrete common PCM instances, such as heaps, histories and mutexes. This library relies on extensionality axioms: propositional and functional extentionality.""" url { src: "git+https://github.com/imdea-software/fcsl-pcm.git#master" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-fcsl-pcm.dev coq.dev
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-fcsl-pcm.dev coq.dev
# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq dev The Coq Proof Assistant coq-core dev The Coq Proof Assistant -- Core Binaries and Tools coq-stdlib dev The Coq Proof Assistant -- Standard Library coqide-server dev The Coq Proof Assistant, XML protocol server dune 3.12.2 Fast, portable, and opinionated build system ocaml 5.0.0 The OCaml compiler (virtual package) ocaml-base-compiler 5.0.0 Official release 5.0.0 ocaml-config 3 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 The following actions will be performed: - install cppo 1.6.9 - install ppx_derivers 1.2.1 - install menhirLib dev - install menhirSdk dev - install cmdliner 1.2.0 - install easy-format 1.3.4 - install result 1.5 - install seq base - install ocaml-compiler-libs v0.12.4 - install camlp-streams 5.0.1 - install sexplib0 v0.16.0 - install stdlib-shims 0.3.0 - install menhir dev - install yojson 2.1.2 - install re 1.11.0 - install biniou 1.2.2 - install ppxlib 0.31.0 - install atd 2.15.0 - install atdgen-runtime 2.15.0 - install ppx_deriving 5.2.1 - install atdts 2.15.0 - install atdgen 2.15.0 - install elpi 1.18.1 - install coq-elpi dev - install coq-hierarchy-builder dev - install coq-mathcomp-ssreflect dev - install coq-mathcomp-fingroup dev - install coq-mathcomp-algebra dev ===== 28 to install ===== <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> retrieved atd.2.15.0 (https://github.com/ahrefs/atd/releases/download/2.15.0/atd-2.15.0.tbz) -> retrieved atdts.2.15.0 (cached) -> retrieved biniou.1.2.2 (https://github.com/mjambon/biniou/releases/download/1.2.2/biniou-1.2.2.tbz) -> retrieved atdgen.2.15.0 (https://github.com/ahrefs/atd/releases/download/2.15.0/atd-2.15.0.tbz) -> retrieved cmdliner.1.2.0 (https://erratique.ch/software/cmdliner/releases/cmdliner-1.2.0.tbz) -> retrieved camlp-streams.5.0.1 (https://github.com/ocaml/camlp-streams/archive/v5.0.1.tar.gz) -> retrieved atdgen-runtime.2.15.0 (https://github.com/ahrefs/atd/releases/download/2.15.0/atd-2.15.0.tbz) -> installed camlp-streams.5.0.1 -> installed cmdliner.1.2.0 -> retrieved coq-hierarchy-builder.dev (git+https://github.com/math-comp/hierarchy-builder.git#master) -> retrieved coq-elpi.dev (git+https://github.com/LPCIC/coq-elpi.git#coq-master) -> retrieved coq-mathcomp-algebra.dev (git+https://github.com/math-comp/math-comp.git) -> retrieved coq-mathcomp-ssreflect.dev (git+https://github.com/math-comp/math-comp.git#master) -> retrieved coq-mathcomp-fingroup.dev (git+https://github.com/math-comp/math-comp.git) -> retrieved cppo.1.6.9 (https://github.com/ocaml-community/cppo/archive/v1.6.9.tar.gz) -> retrieved easy-format.1.3.4 (https://github.com/ocaml-community/easy-format/releases/download/1.3.4/easy-format-1.3.4.tbz) -> installed cppo.1.6.9 -> installed easy-format.1.3.4 -> retrieved elpi.1.18.1 (https://github.com/LPCIC/elpi/releases/download/v1.18.1/elpi-1.18.1.tbz) -> installed biniou.1.2.2 -> retrieved menhir.dev (git+https://gitlab.inria.fr/fpottier/menhir.git#master) -> retrieved ocaml-compiler-libs.v0.12.4 (https://github.com/janestreet/ocaml-compiler-libs/releases/download/v0.12.4/ocaml-compiler-libs-v0.12.4.tbz) -> installed ocaml-compiler-libs.v0.12.4 -> retrieved menhirSdk.dev (git+https://gitlab.inria.fr/fpottier/menhir.git#master) -> retrieved menhirLib.dev (git+https://gitlab.inria.fr/fpottier/menhir.git#master) -> retrieved ppx_derivers.1.2.1 (https://github.com/ocaml-ppx/ppx_derivers/archive/1.2.1.tar.gz) -> installed ppx_derivers.1.2.1 -> installed menhirSdk.dev -> installed menhirLib.dev -> retrieved ppx_deriving.5.2.1 (https://github.com/ocaml-ppx/ppx_deriving/releases/download/v5.2.1/ppx_deriving-v5.2.1.tbz) -> retrieved ppxlib.0.31.0 (https://github.com/ocaml-ppx/ppxlib/releases/download/0.31.0/ppxlib-0.31.0.tbz) -> installed seq.base -> retrieved re.1.11.0 (https://github.com/ocaml/ocaml-re/releases/download/1.11.0/re-1.11.0.tbz) -> installed re.1.11.0 -> retrieved result.1.5 (https://github.com/janestreet/result/releases/download/1.5/result-1.5.tbz) -> installed result.1.5 -> installed menhir.dev -> retrieved sexplib0.v0.16.0 (https://ocaml.janestreet.com/ocaml-core/v0.16/files/sexplib0-v0.16.0.tar.gz) -> retrieved stdlib-shims.0.3.0 (https://github.com/ocaml/stdlib-shims/releases/download/0.3.0/stdlib-shims-0.3.0.tbz) -> installed sexplib0.v0.16.0 -> installed stdlib-shims.0.3.0 -> retrieved yojson.2.1.2 (https://github.com/ocaml-community/yojson/releases/download/2.1.2/yojson-2.1.2.tbz) -> installed yojson.2.1.2 -> installed atdgen-runtime.2.15.0 -> installed atd.2.15.0 -> installed atdts.2.15.0 -> installed atdgen.2.15.0 -> installed ppxlib.0.31.0 -> installed ppx_deriving.5.2.1 -> installed elpi.1.18.1 [ERROR] The compilation of coq-elpi.dev failed at "make build COQBIN=/home/bench/.opam/ocaml-base-compiler.5.0.0/bin/ ELPIDIR=/home/bench/.opam/ocaml-base-compiler.5.0.0/lib/elpi OCAMLWARN=". #=== ERROR while compiling coq-elpi.dev =======================================# # context 2.1.5 | linux/x86_64 | ocaml-base-compiler.5.0.0 | file:///home/bench/run/opam-coq-archive/extra-dev # path ~/.opam/ocaml-base-compiler.5.0.0/.opam-switch/build/coq-elpi.dev # command ~/.opam/opam-init/hooks/sandbox.sh build make build COQBIN=/home/bench/.opam/ocaml-base-compiler.5.0.0/bin/ ELPIDIR=/home/bench/.opam/ocaml-base-compiler.5.0.0/lib/elpi OCAMLWARN= # exit-code 2 # env-file ~/.opam/log/coq-elpi-21095-f70a51.env # output-file ~/.opam/log/coq-elpi-21095-f70a51.out ### output ### # [...] # CAMLOPT -c -for-pack Elpi_plugin src/coq_elpi_vernacular.ml # CAMLOPT -c -for-pack Elpi_plugin src/coq_elpi_vernacular_syntax.ml # CAMLOPT -pack -o src/elpi_plugin.cmx # CAMLOPT -a -o src/elpi_plugin.cmxa # CAMLOPT -shared -o src/elpi_plugin.cmxs # COQC theories/elpi.v # Fatal error: Not enough heap memory to reserve minor heaps # Aborted (core dumped) # make[3]: *** [Makefile.coq:847: theories/elpi.vo] Error 134 # make[2]: *** [Makefile.coq:417: all] Error 2 # make[1]: *** [Makefile.coq:937: opt] Error 2 # make: *** [Makefile:51: build-core] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-elpi dev +- +- The following changes have been performed (the rest was aborted) | - install atd 2.15.0 | - install atdgen 2.15.0 | - install atdgen-runtime 2.15.0 | - install atdts 2.15.0 | - install biniou 1.2.2 | - install camlp-streams 5.0.1 | - install cmdliner 1.2.0 | - install cppo 1.6.9 | - install easy-format 1.3.4 | - install elpi 1.18.1 | - install menhir dev | - install menhirLib dev | - install menhirSdk dev | - install ocaml-compiler-libs v0.12.4 | - install ppx_derivers 1.2.1 | - install ppx_deriving 5.2.1 | - install ppxlib 0.31.0 | - install re 1.11.0 | - install result 1.5 | - install seq base | - install sexplib0 v0.16.0 | - install stdlib-shims 0.3.0 | - install yojson 2.1.2 +- # Run eval $(opam env) to update the current shell environment The former state can be restored with: /usr/local/bin/opam switch import "/home/bench/.opam/ocaml-base-compiler.5.0.0/.opam-switch/backup/state-20240114182003.export"
true
No files were installed.
true