(2021-04-10 01:03:28 UTC)
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
coq 8.12.0 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.11.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.11.1 Official release 4.11.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.1 A library manager for OCaml
# 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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-graph-theory.0.8 coq.8.12.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 2h opam install -y --deps-only coq-graph-theory.0.8 coq.8.12.0opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-graph-theory.0.8 coq.8.12.0# 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-perl 1 Virtual package relying on perl coq 8.12.0 Formal proof management system coq-elpi 1.8.2~8.12 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.12.0 ELPI - Embeddable λProlog Interpreter num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.11.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.11.1 Official release 4.11.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 [NOTE] Package coq is already installed (current version is 8.12.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.11.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.11.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/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] - 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 - COQC theories/finmap_plus.v - COQC theories/finite_quotient.v - COQC theories/digraph.v - COQC theories/structures.v - COQC theories/equiv.v - COQC theories/pttdom.v - 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 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))". - - COQC theories/sgraph.v - make[2]: *** [Makefile.coq:715: theories/pttdom.vo] Error 1 - make[2]: *** Waiting for unfinished jobs.... - COQC theories/mgraph.v - 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 - Warning: mem_imset is deprecated; use imset_f instead - Warning: mem_imset is deprecated; use imset_f instead - make[1]: *** [Makefile.coq:339: all] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.11.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.7 | linux/x86_64 | ocaml-base-compiler.4.11.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.11.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-5896-335865.env # output-file ~/.opam/log/coq-graph-theory-5896-335865.out ### output ### # [...] # make[2]: *** [Makefile.coq:715: theories/pttdom.vo] Error 1 # make[2]: *** Waiting for unfinished jobs.... # COQC theories/mgraph.v # 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 # Warning: mem_imset is deprecated; use imset_f instead # Warning: mem_imset is deprecated; use imset_f instead # make[1]: *** [Makefile.coq:339: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.11.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.12.0' failed.
No files were installed.
true