* (2021-04-08 21:07:48 UTC)*

# 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 3 Virtual package relying on a GMP lib system installation coq 8.13.0 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.1 Official release 4.10.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 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: [make "-j%{jobs}%" ] install: [make "install"] depends: [ "coq" {>= "8.11" & < "8.14~"} "coq-mathcomp-ssreflect" {>= "1.10" & < "1.13~"} "coq-mathcomp-finmap" "coq-hierarchy-builder" { >= "0.10" } ] 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.8.tar.gz" checksum: "sha512=695618a7a62092fdaf296824ca5d2b01606a0e41cc8ab34233db3de2475d88e4c24da16f2bbf4d40914138581b44883345982ea616874d7beba16ad161f74bba" }

- Command
`true`

- Return code
- 0

Dry install with the current Coq version:

- Command
`opam install -y --show-action coq-graph-theory.0.8 coq.8.13.0`

- Return code
- 0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

- Command
`true`

- Return code
- 0

- Command
`opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-graph-theory.0.8 coq.8.13.0`

- Return code
- 0
- Duration
- 13 m 40 s

- Command
`opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-graph-theory.0.8 coq.8.13.0`

- Return code
- 7936
- Duration
- 42 s
- Output
# Packages matching: installed # Name # Installed # Synopsis base v0.14.1 Full standard library replacement for OCaml base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-gmp 3 Virtual package relying on a GMP lib system installation conf-perl 1 Virtual package relying on perl coq 8.13.0 Formal proof management system coq-elpi 1.9.5 Elpi extension language for Coq coq-hierarchy-builder 1.1.0 High level commands to declare and evolve a hierarchy based on packed classes coq-mathcomp-bigenough 1.0.0 A small library to do epsilon - N reasonning coq-mathcomp-finmap 1.5.1 Finite sets, finite maps, finitely supported functions coq-mathcomp-ssreflect 1.12.0 Small Scale Reflection cppo 1.6.7 Code preprocessor like cpp for OCaml csexp 1.5.1 Parsing and printing of S-expressions in Canonical form dune 2.8.5 Fast, portable, and opinionated build system dune-configurator 2.8.5 Helper library for gathering system configuration elpi 1.13.0 ELPI - Embeddable λProlog Interpreter num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.10.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.10.1 Official release 4.10.1 ocaml-compiler-libs v0.12.3 OCaml compiler libraries repackaged ocaml-config 1 OCaml Switch Configuration ocaml-migrate-parsetree 1.8.0 Convert OCaml parsetrees between different versions ocamlfind 1.9.1 A library manager for OCaml ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_deriving 5.1 Type-driven code generation for OCaml ppxlib 0.14.0 Base library and tools for ppx rewriters re 1.9.0 RE is a regular expression library for OCaml result 1.5 Compatibility Result module seq base Compatibility package for OCaml's standard iterator type starting from 4.07. sexplib0 v0.14.0 Library containing the definition of S-expressions and some base converters stdio v0.14.0 Standard IO library for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is 8.13.0). The following actions will be performed: - install coq-graph-theory 0.8 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-graph-theory.0.8: http] [coq-graph-theory.0.8] downloaded from https://github.com/coq-community/graph-theory/archive/v0.8.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-graph-theory: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-graph-theory.0.8) - coq_makefile -f _CoqProject -o Makefile.coq - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-graph-theory.0.8' - COQDEP VFILES - COQC theories/edone.v - COQC theories/bounded.v - COQC theories/setoid_bigop.v - COQC theories/preliminaries.v - File "./theories/preliminaries.v", line 27, characters 0-58: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./theories/setoid_bigop.v", line 17, characters 0-83: - Warning: elpi: Using coq.env.add-const for declaring axioms or section - variables is deprecated. Use coq.env.add-axiom or - coq.env.add-section-variable instead - [elpi.add-const-for-axiom-or-sectionvar,deprecated] - File "./theories/setoid_bigop.v", line 37, characters 0-43: - Warning: - The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead - [lib,elpi] - File "./theories/setoid_bigop.v", line 39, characters 0-42: - Warning: - The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead - [lib,elpi] - File "./theories/setoid_bigop.v", line 45, characters 0-36: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./theories/preliminaries.v", line 711, characters 0-45: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - Warning: mem_imset is deprecated; use imset_f instead - Warning: mem_imset is deprecated; use imset_f instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - Warning: sorted_le_nth is deprecated; use sorted_leq_nth instead - COQC theories/bij.v - COQC theories/set_tac.v - File "./theories/bij.v", line 28, characters 0-49: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./theories/bij.v", line 36, characters 0-49: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./theories/set_tac.v", line 185, characters 0-72: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - COQC theories/finmap_plus.v - COQC theories/finite_quotient.v - COQC theories/digraph.v - COQC theories/structures.v - File "./theories/structures.v", line 69, characters 0-144: - Warning: elpi: Using coq.env.add-const for declaring axioms or section - variables is deprecated. Use coq.env.add-axiom or - coq.env.add-section-variable instead - [elpi.add-const-for-axiom-or-sectionvar,deprecated] - File "./theories/structures.v", line 69, characters 0-144: - Warning: elpi: Using coq.env.add-const for declaring axioms or section - variables is deprecated. Use coq.env.add-axiom or - coq.env.add-section-variable instead - [elpi.add-const-for-axiom-or-sectionvar,deprecated] - COQC theories/equiv.v - File "./theories/structures.v", line 88, characters 0-259: - Warning: elpi: Using coq.env.add-const for declaring axioms or section - variables is deprecated. Use coq.env.add-axiom or - coq.env.add-section-variable instead - [elpi.add-const-for-axiom-or-sectionvar,deprecated] - File "./theories/structures.v", line 88, characters 0-259: - Warning: elpi: Using coq.env.add-const for declaring axioms or section - variables is deprecated. Use coq.env.add-axiom or - coq.env.add-section-variable instead - [elpi.add-const-for-axiom-or-sectionvar,deprecated] - File "./theories/structures.v", line 134, characters 0-27: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - COQC theories/pttdom.v - File "./theories/equiv.v", line 64, characters 0-44: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./theories/equiv.v", line 67, characters 0-30: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./theories/pttdom.v", line 17, characters 0-208: - Warning: elpi: Using coq.env.add-const for declaring axioms or section - variables is deprecated. Use coq.env.add-axiom or - coq.env.add-section-variable instead - [elpi.add-const-for-axiom-or-sectionvar,deprecated] - File "./theories/pttdom.v", line 17, characters 0-208: - Warning: elpi: Using coq.env.add-const for declaring axioms or section - variables is deprecated. Use coq.env.add-axiom or - coq.env.add-section-variable instead - [elpi.add-const-for-axiom-or-sectionvar,deprecated] - File "./theories/digraph.v", line 741, characters 0-26: - Warning: The default value for hint locality is currently "local" in a - section and "global" otherwise, but is scheduled to change in a future - release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore deprecated. It is recommended to - use "export" whenever possible. [deprecated-hint-without-locality,deprecated] - File "./theories/pttdom.v", line 45, characters 0-858: - Error: - elpi: parameter illtyped: In environment - A : Type - The term "id_phant" has type "phantom Type A -> phantom Type A" - while it is expected to have type - "unify Type Type A ?t (Some (is_not_canonically_a, setoid))". - - make[2]: *** [Makefile.coq:719: theories/pttdom.vo] Error 1 - make[2]: *** Waiting for unfinished jobs.... - File "./theories/digraph.v", line 1126, characters 0-124: - Warning: The format modifier is irrelevant for only parsing rules. - [irrelevant-format-only-parsing,parsing] - File "./theories/digraph.v", line 1128, characters 0-126: - Warning: The format modifier is irrelevant for only parsing rules. - [irrelevant-format-only-parsing,parsing] - File "./theories/digraph.v", line 1131, characters 0-131: - Warning: The format modifier is irrelevant for only parsing rules. - [irrelevant-format-only-parsing,parsing] - File "./theories/digraph.v", line 1135, characters 0-133: - Warning: The format modifier is irrelevant for only parsing rules. - [irrelevant-format-only-parsing,parsing] - make[1]: *** [Makefile.coq:343: all] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-graph-theory.0.8' - make: *** [Makefile:2: all] Error 2 [ERROR] The compilation of coq-graph-theory failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-graph-theory.0.8 ===============================# # context 2.0.6 | linux/x86_64 | ocaml-base-compiler.4.10.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-graph-theory.0.8 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-graph-theory-21022-335865.env # output-file ~/.opam/log/coq-graph-theory-21022-335865.out ### output ### # [...] # File "./theories/digraph.v", line 1128, characters 0-126: # Warning: The format modifier is irrelevant for only parsing rules. # [irrelevant-format-only-parsing,parsing] # File "./theories/digraph.v", line 1131, characters 0-131: # Warning: The format modifier is irrelevant for only parsing rules. # [irrelevant-format-only-parsing,parsing] # File "./theories/digraph.v", line 1135, characters 0-133: # Warning: The format modifier is irrelevant for only parsing rules. # [irrelevant-format-only-parsing,parsing] # make[1]: *** [Makefile.coq:343: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.1/.opam-switch/build/coq-graph-theory.0.8' # make: *** [Makefile:2: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-graph-theory 0.8 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-graph-theory.0.8 coq.8.13.0' failed.

No files were installed.

- Command
`true`

- Return code
- 0
- Missing removes
- none
- Wrong removes
- none