# 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 dev Formal proof management system dune 3.0.3 Fast, portable, and opinionated build system ocaml 4.11.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.11.2 Official release 4.11.2 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: "christian.doczkal@inria.fr" homepage: "https://github.com/coq-community/graph-theory" dev-repo: "git+https://github.com/coq-community/graph-theory.git" bug-reports: "https://github.com/coq-community/graph-theory/issues" license: "CECILL-B" synopsis: "Graph theory results in Coq and MathComp" description: """ A library of formalized graph theory results, including various standard results from the literature (e.g., Menger’s Theorem, Hall’s Marriage Theorem, and the excluded minor characterization of treewidth-two graphs) as well as some more recent results arising from the study of relation algebra within the ERC CoVeCe project (e.g., soundness and completeness of an axiomatization of graph isomorphism).""" build: [ ["sh" "-exc" "cat _CoqProject.wagner >>_CoqProject"] {coq-fourcolor:installed} [make "-j%{jobs}%" ] ] install: [make "install"] depends: [ "coq" {(>= "8.12" & < "8.14~") | (= "dev")} "coq-mathcomp-algebra" {(>= "1.12" & < "1.13~") | (= "dev")} "coq-mathcomp-finmap" "coq-hierarchy-builder" { (>= "1.1.0") } ] depopts: ["coq-fourcolor"] tags: [ "category:Computer Science/Graph Theory" "keyword:graph theory" "keyword:minors" "keyword:treewidth" "keyword:algebra" "logpath:GraphTheory" "date:2020-12-08" ] authors: [ "Christian Doczkal" "Damien Pous" ] url { src: "https://github.com/coq-community/graph-theory/archive/v0.9.tar.gz" checksum: "sha512=db62ec2bdbbb1fa2cbe411c42acaa4d4ab0988486a8cff8b53acd4f0b9776df72e117ca9256141a7d59de35686bda8f07d705273b00f79e2715755aa78d93f0e" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-graph-theory.0.9 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-graph-theory.0.9 coq.dev
# 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 dev Formal proof management system dune 3.0.3 Fast, portable, and opinionated build system ocaml 4.11.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.11.2 Official release 4.11.2 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 The following actions will be performed: - install conf-perl 2 - install ppx_derivers 1.2.1 - install seq base - install sexplib0 v0.15.0 - install cppo 1.6.8 - install result 1.5 - install coq-mathcomp-ssreflect dev - install ocaml-compiler-libs v0.12.4 - install stdlib-shims 0.3.0 - install camlp5 7.14 - install re 1.10.3 - install coq-mathcomp-finmap dev - install coq-mathcomp-fingroup dev - install ppxlib 0.25.0 - install coq-mathcomp-algebra dev - install ppx_deriving 5.2.1 - install elpi 1.14.1 - install coq-elpi dev - install coq-hierarchy-builder dev ===== 19 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [camlp5.7.14] downloaded from cache at https://opam.ocaml.org/cache [coq-elpi.dev] synchronised from git+https://github.com/LPCIC/coq-elpi.git#coq-master [coq-hierarchy-builder.dev] synchronised from git+https://github.com/math-comp/hierarchy-builder.git#coq-master [coq-mathcomp-algebra.dev] synchronised from git+https://github.com/math-comp/math-comp.git [coq-mathcomp-ssreflect.dev] synchronised from git+https://github.com/math-comp/math-comp.git#master [cppo.1.6.8] downloaded from cache at https://opam.ocaml.org/cache [coq-mathcomp-fingroup.dev] synchronised from git+https://github.com/math-comp/math-comp.git [coq-mathcomp-finmap.dev] synchronised from git+https://github.com/math-comp/finmap.git#master [ocaml-compiler-libs.v0.12.4] downloaded from cache at https://opam.ocaml.org/cache [elpi.1.14.1] downloaded from cache at https://opam.ocaml.org/cache [ppx_derivers.1.2.1] downloaded from cache at https://opam.ocaml.org/cache [ppx_deriving.5.2.1] downloaded from cache at https://opam.ocaml.org/cache [ppxlib.0.25.0] downloaded from cache at https://opam.ocaml.org/cache [re.1.10.3] downloaded from cache at https://opam.ocaml.org/cache [result.1.5] downloaded from cache at https://opam.ocaml.org/cache [sexplib0.v0.15.0] downloaded from cache at https://opam.ocaml.org/cache [stdlib-shims.0.3.0] downloaded from cache at https://opam.ocaml.org/cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed conf-perl.2 -> installed cppo.1.6.8 -> installed ocaml-compiler-libs.v0.12.4 -> installed ppx_derivers.1.2.1 -> installed result.1.5 -> installed seq.base -> installed sexplib0.v0.15.0 -> installed stdlib-shims.0.3.0 -> installed re.1.10.3 -> installed ppxlib.0.25.0 -> installed coq-mathcomp-ssreflect.dev -> installed ppx_deriving.5.2.1 -> installed coq-mathcomp-finmap.dev -> installed camlp5.7.14 -> installed elpi.1.14.1 -> installed coq-mathcomp-fingroup.dev -> installed coq-mathcomp-algebra.dev -> installed coq-elpi.dev [ERROR] The compilation of coq-hierarchy-builder failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make build". #=== ERROR while compiling coq-hierarchy-builder.dev ==========================# # context 2.0.7 | linux/x86_64 | ocaml-base-compiler.4.11.2 | file:///home/bench/run/opam-coq-archive/extra-dev # path ~/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.dev # command ~/.opam/opam-init/hooks/sandbox.sh build make build # exit-code 2 # env-file ~/.opam/log/coq-hierarchy-builder-31396-21ab01.env # output-file ~/.opam/log/coq-hierarchy-builder-31396-21ab01.out ### output ### # [...] # make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.dev' # COQDEP VFILES # *** Warning: in file structures.v, library elpi is required from root elpi and has not been found in the loadpath! # COQC structures.v # File "./structures.v", line 15, characters 0-30: # Error: Cannot find a physical path bound to logical path # elpi with prefix elpi. # # make[2]: *** [Makefile.coq:791: structures.vo] Error 1 # make[1]: *** [Makefile.coq:408: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/build/coq-hierarchy-builder.dev' # make: *** [Makefile:97: this-build] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-hierarchy-builder dev +- +- The following changes have been performed | - install camlp5 7.14 | - install conf-perl 2 | - install coq-elpi dev | - install coq-mathcomp-algebra dev | - install coq-mathcomp-fingroup dev | - install coq-mathcomp-finmap dev | - install coq-mathcomp-ssreflect dev | - install cppo 1.6.8 | - install elpi 1.14.1 | - install ocaml-compiler-libs v0.12.4 | - install ppx_derivers 1.2.1 | - install ppx_deriving 5.2.1 | - install ppxlib 0.25.0 | - install re 1.10.3 | - install result 1.5 | - install seq base | - install sexplib0 v0.15.0 | - install stdlib-shims 0.3.0 +- # Run eval $(opam env) to update the current shell environment The former state can be restored with: opam switch import "/home/bench/.opam/ocaml-base-compiler.4.11.2/.opam-switch/backup/state-20220327025357.export"
true
No files were installed.
true