(2021-10-15 23:38:58 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.12.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.0 Official release 4.12.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-graph-theory.0.8 coq.8.13.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-graph-theory.0.8 coq.8.13.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-graph-theory.0.8 coq.8.13.0# 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.0 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.12.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.0 Official release 4.12.0 ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled 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.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.12.0/.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.12.0/.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/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 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 - COQC theories/equiv.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] - COQC theories/sgraph.v - COQC theories/mgraph.v - 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:720: theories/pttdom.vo] Error 1 - make[2]: *** Waiting for unfinished jobs.... - File "./theories/sgraph.v", line 318, characters 0-40: - 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: mem_imset is deprecated; use imset_f instead - Warning: mem_imset is deprecated; use imset_f instead - File "./theories/sgraph.v", line 737, characters 0-61: - 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 - make[1]: *** [Makefile.coq:343: all] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.12.0/.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.8 | linux/x86_64 | ocaml-base-compiler.4.12.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.12.0/.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-22512-335865.env # output-file ~/.opam/log/coq-graph-theory-22512-335865.out ### output ### # [...] # Warning: mem_imset is deprecated; use imset_f instead # File "./theories/sgraph.v", line 737, characters 0-61: # 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 # make[1]: *** [Makefile.coq:343: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.12.0/.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.
true