coq-fourcolor.opam

opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/coq-community/fourcolor"
dev-repo: "git+https://github.com/coq-community/fourcolor.git"
bug-reports: "https://github.com/coq-community/fourcolor/issues"
license: "CECILL-B"

synopsis: "Mechanization of the Four Color Theorem in Coq"
description: """
This library contains a formal proof of the Four Color Theorem in Coq,
along with the theories needed to support stating and then proving the Theorem.
This includes an axiomatization of the setoid of classical real numbers,
basic plane topology definitions, and a theory of combinatorial hypermaps."""

build: [make "-C" "theories/proof" "-j%{jobs}%"]
install: [make "-C" "theories/proof" "install"]
depends: [
  "coq" {>= "8.16"}
  "coq-mathcomp-ssreflect" {>= "2.1.0"}
  "coq-mathcomp-algebra" 
  "coq-hierarchy-builder" {>= "1.5.0"}
  "coq-fourcolor-reals" {= version}
]

tags: [
  "category:Mathematics/Combinatorics and Graph Theory"
  "keyword:Four color theorem"
  "keyword:small scale reflection"
  "keyword:Mathematical Components"
  "logpath:fourcolor.proof"
]
authors: [
  "Georges Gonthier"
]