# 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.06.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.06.1 Official 4.06.1 release ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 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: [ ["sh" "-exc" "cat _CoqProject.wagner >>_CoqProject"] {coq-fourcolor:installed} [make "-j%{jobs}%" ] ] install: [make "install"] depends: [ "coq" {(>= "8.12" & < "8.14~") | (= "dev")} "coq-mathcomp-algebra" {(>= "1.12" & < "1.13~") | (= "dev")} "coq-mathcomp-finmap" "coq-hierarchy-builder" { (>= "1.1.0") } ] depopts: ["coq-fourcolor"] 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.9.tar.gz" checksum: "sha512=db62ec2bdbbb1fa2cbe411c42acaa4d4ab0988486a8cff8b53acd4f0b9776df72e117ca9256141a7d59de35686bda8f07d705273b00f79e2715755aa78d93f0e" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-graph-theory.0.9 coq.8.12.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-graph-theory.0.9 coq.8.12.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-graph-theory.0.9 coq.8.12.0
Total: 18 M
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/transfer.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/reduction.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/sgraph.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/connectivity.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/open_confluence.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/sgraph.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/open_confluence.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/skeleton.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/smerge.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/preliminaries.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/preliminaries.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/checkpoint.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/connectivity.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/wpgt.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/digraph.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/transfer.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/treewidth.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/pttdom.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph2.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/ptt.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_def.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/excluded.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/minor.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/digraph.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/checkpoint.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/skeleton.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/wpgt.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_iso.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/finmap_plus.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/smerge.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/structures.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/setoid_bigop.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_def.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/coloring.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/arc.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/cp_minor.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph2.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/treewidth.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph2_tw2.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_iso.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/arc.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/finite_quotient.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/dom.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/coloring.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/excluded.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/dom.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/finmap_plus.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_top.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/equiv.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/finite_quotient.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/minor.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/completeness.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/reduction.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/bij.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/helly.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/partition.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/setoid_bigop.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph2_tw2.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/set_tac.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/pttdom.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/cp_minor.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/equiv.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/sgraph.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/open_confluence.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_top.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/rewriting.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/connectivity.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/partition.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/transfer.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/preliminaries.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/completeness.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/digraph.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/bij.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/bounded.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/checkpoint.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/helly.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/skeleton.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/set_tac.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/wpgt.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/smerge.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph2.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/treewidth.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/ptt.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_def.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/structures.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/dom.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/excluded.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/minor.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/arc.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/coloring.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_iso.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/finite_quotient.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/reduction.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/pttdom.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/finmap_plus.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/cp_minor.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/equiv.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/bounded.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/rewriting.glob
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/mgraph2_tw2.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/setoid_bigop.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/set_tac.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/bij.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/extraction_top.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/partition.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/completeness.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/structures.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/helly.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/ptt.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/edone.vo
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/rewriting.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/bounded.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/edone.v
../ocaml-base-compiler.4.06.1/lib/coq/user-contrib/GraphTheory/edone.glob
opam remove -y coq-graph-theory.0.9