« Up

graph-theory 0.8 Error

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

Context

# 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"
}

Lint

Command
true
Return code
0

Dry install

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

Install dependencies

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

Install

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.

Installation size

No files were installed.

Uninstall

Command
true
Return code
0
Missing removes
none
Wrong removes
none