« Up

graph-theory 0.8 Error 🔥

📅 (2021-10-23 16:42:14 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.1      Formal proof management system
num                 1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.09.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1      Official release 4.09.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" { (>= "1.0.0") & (!= "1.1.0") }
]
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.1
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 4h opam install -y --deps-only coq-graph-theory.0.8 coq.8.13.1
Return code
0
Duration
11 m 13 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-graph-theory.0.8 coq.8.13.1
Return code
7936
Duration
56 s
Output
# Packages matching: installed
# Name                 # Installed # Synopsis
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.1      Formal proof management system
coq-elpi               1.11.1      Elpi extension language for Coq
coq-hierarchy-builder  1.2.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.8       Code preprocessor like cpp for OCaml
dune                   2.9.1       Fast, portable, and opinionated build system
elpi                   1.13.7      ELPI - Embeddable λProlog Interpreter
num                    1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                  4.09.1      The OCaml compiler (virtual package)
ocaml-base-compiler    4.09.1      Official release 4.09.1
ocaml-compiler-libs    v0.12.4     OCaml compiler libraries repackaged
ocaml-config           1           OCaml Switch Configuration
ocamlfind              1.9.1       A library manager for OCaml
ppx_derivers           1.2.1       Shared [@@deriving] plugin registry
ppx_deriving           5.2.1       Type-driven code generation for OCaml
ppxlib                 0.23.0      Standard library for ppx rewriters
re                     1.10.3      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
stdlib-shims           0.3.0       Backport some of the new stdlib features to older compiler
zarith                 1.12        Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is 8.13.1).
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.09.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.09.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 37, characters 0-43:
- Warning:
- The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead
- [HB.deprecated,HB]
- File "./theories/setoid_bigop.v", line 39, characters 0-42:
- Warning:
- The syntax "HB.instance Key FactoryInstance" is deprecated, use "HB.instance Definition" instead
- [HB.deprecated,HB]
- 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/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]
- 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]
- COQC theories/finmap_plus.v
- COQC theories/finite_quotient.v
- COQC theories/digraph.v
- COQC theories/structures.v
- 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/equiv.v
- 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/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 208, characters 1-105:
- Warning:
- non forgetful inheritance detected.
-  You have two solutions: 
- 1. (Best practice) Reorganize your hierarchy to make 
- structures_Elabel_of_Setoid depend on pttdom_Pttdom. 
- See the paper "Competing inheritance paths in 
- dependent type theory" (https://hal.inria.fr/hal-02463336) for more 
- explanations 
- 2. Use the attribute #[non_forgetful_inheritance] to disable this check. 
- We strongly advise you encapsulate this instance inside a module, 
- in order to isolate it from the rest of the code, and to be able 
- to import it on demand. See the above paper and the file 
- https://github.com/math-comp/hierarchy-builder/blob/master/tests/non-forgetful-inheritance.v 
- to witness devastating effects.
- [HB.non-forgetful-inheritance,HB]
- 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]
- File "./theories/pttdom.v", line 251, characters 11-30:
- Error: The reference Elabel.Exports.eqv' was not found in the current
- environment.
- 
- make[2]: *** [Makefile.coq:719: theories/pttdom.vo] Error 1
- make[2]: *** Waiting for unfinished jobs....
- make[1]: *** [Makefile.coq:343: all] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.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.09.1 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.09.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-14416-335865.env
# output-file          ~/.opam/log/coq-graph-theory-14416-335865.out
### output ###
# [...]
# File "./theories/digraph.v", line 1135, characters 0-133:
# Warning: The format modifier is irrelevant for only parsing rules.
# [irrelevant-format-only-parsing,parsing]
# File "./theories/pttdom.v", line 251, characters 11-30:
# Error: The reference Elabel.Exports.eqv' was not found in the current
# environment.
# 
# make[2]: *** [Makefile.coq:719: theories/pttdom.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# make[1]: *** [Makefile.coq:343: all] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.09.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.1' failed.

Installation size

No files were installed.

Uninstall 🧹

Command
true
Return code
0
Missing removes
none
Wrong removes
none