diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 1a26e6f..80c77f6 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,13 +18,13 @@ jobs: matrix: image: - 'mathcomp/mathcomp-dev:coq-dev' + - 'mathcomp/mathcomp:2.2.0-coq-8.20' - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.2.0-coq-8.18' - 'mathcomp/mathcomp:2.1.0-coq-8.18' - - 'mathcomp/mathcomp:2.0.0-coq-8.18' fail-fast: false steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - uses: coq-community/docker-coq-action@v1 with: custom_image: ${{ matrix.image }} diff --git a/Makefile b/Makefile index ad909e5..d5aa0bf 100644 --- a/Makefile +++ b/Makefile @@ -1,16 +1,4 @@ -all: Makefile.coq - @+$(MAKE) -f Makefile.coq all +# -*- Makefile -*- -clean: Makefile.coq - @+$(MAKE) -f Makefile.coq cleanall - @rm -f Makefile.coq Makefile.coq.conf - -Makefile.coq: _CoqProject - $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq - -force _CoqProject Makefile: ; - -%: Makefile.coq force - @+$(MAKE) -f Makefile.coq $@ - -.PHONY: all clean force +# -------------------------------------------------------------------- +include Makefile.common diff --git a/Makefile.common b/Makefile.common new file mode 100644 index 0000000..c523410 --- /dev/null +++ b/Makefile.common @@ -0,0 +1,99 @@ +# -*- Makefile -*- + +###################################################################### +# USAGE: # +# The rules this-config::, this-build::, this-distclean::, # +# pre-makefile::, this-clean:: and __always__:: may be extended # +# Additionally, the following variables may be customized: # +SUBDIRS?= +COQBIN?=$(dir $(shell which coqtop)) +COQMAKEFILE?=$(COQBIN)coq_makefile +COQDEP?=$(COQBIN)coqdep +COQPROJECT?=_CoqProject +COQMAKEOPTIONS?= +COQMAKEFILEOPTIONS?= +V?= +VERBOSE?=V +###################################################################### + +# local context: ----------------------------------------------------- +.PHONY: all config build clean distclean __always__ +.SUFFIXES: + +H:= $(if $(VERBOSE),,@) # not used yet +TOP = $(dir $(lastword $(MAKEFILE_LIST))) +COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS) +BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \ + | wc -l | sed 's/ *//g') + +# coq version: +ifneq "$(BRANCH_coq)" "0" +COQVVV:= dev +else +COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1) +endif + +COQV:= $(shell echo $(COQVVV) | cut -d"." -f1) +COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2) + +# all: --------------------------------------------------------------- +all: config build + +# Makefile.coq: ------------------------------------------------------ +.PHONY: pre-makefile + +Makefile.coq: pre-makefile $(COQPROJECT) Makefile + $(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq + +# Global config, build, clean and distclean -------------------------- +config: sub-config this-config + +build: sub-build this-build + +clean: sub-clean this-clean + +distclean: sub-distclean this-distclean + +# Local config, build, clean and distclean --------------------------- +.PHONY: this-config this-build this-distclean this-clean + +this-config:: __always__ + +this-build:: this-config Makefile.coq + +$(COQMAKE) + +this-distclean:: this-clean + rm -f Makefile.coq Makefile.coq.conf Makefile.coq + +this-clean:: __always__ + @if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi + +# Install target ----------------------------------------------------- +.PHONY: install + +install: __always__ Makefile.coq + $(COQMAKE) install +# counting lines of Coq code ----------------------------------------- +.PHONY: count + +COQFILES = $(shell grep '.v$$' $(COQPROJECT)) + +count: + @coqwc $(COQFILES) | tail -1 | \ + awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}' +# Additionally cleaning backup (*~) files ---------------------------- +this-distclean:: + rm -f $(shell find . -name '*~') + +# Make in SUBDIRS ---------------------------------------------------- +ifdef SUBDIRS +sub-%: __always__ + @set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done +else +sub-%: __always__ + @true +endif + +# Make of individual .vo --------------------------------------------- +%.vo: __always__ Makefile.coq + +$(COQMAKE) $@ diff --git a/README.md b/README.md index b2dffb1..c5afa9b 100644 --- a/README.md +++ b/README.md @@ -49,7 +49,7 @@ axiomatization of graph isomorphism). - License: [CeCILL-B](LICENSE) - Compatible Coq versions: 8.18 or later - Additional dependencies: - - MathComp's [SSReflect library](https://math-comp.github.io), version 2.0 or later + - MathComp's [SSReflect library](https://math-comp.github.io), version 2.1.0 or later - MathComp's [Algebra library](https://math-comp.github.io) - MathComp's [finmap library](https://github.com/math-comp/finmap) - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder), version 1.5.0 or later diff --git a/coq-graph-theory-planar.opam b/coq-graph-theory-planar.opam index 88c8b81..0d91edc 100644 --- a/coq-graph-theory-planar.opam +++ b/coq-graph-theory-planar.opam @@ -17,7 +17,7 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "3.5"} "coq" {>= "8.18"} - "coq-mathcomp-ssreflect" {>= "2.0"} + "coq-mathcomp-ssreflect" {>= "2.1.0"} "coq-graph-theory" {= version} "coq-fourcolor" ] diff --git a/coq-graph-theory.opam b/coq-graph-theory.opam index 374348d..c1663a7 100644 --- a/coq-graph-theory.opam +++ b/coq-graph-theory.opam @@ -17,7 +17,7 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "3.5"} "coq" {>= "8.18"} - "coq-mathcomp-ssreflect" {>= "2.0"} + "coq-mathcomp-ssreflect" {>= "2.1.0"} "coq-mathcomp-algebra" "coq-mathcomp-finmap" "coq-hierarchy-builder" {>= "1.5.0"} diff --git a/meta.yml b/meta.yml index 86a77c4..894264d 100644 --- a/meta.yml +++ b/meta.yml @@ -70,22 +70,22 @@ supported_coq_versions: tested_coq_opam_versions: - version: 'coq-dev' repo: 'mathcomp/mathcomp-dev' +- version: '2.2.0-coq-8.20' + repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.18' repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '2.0.0-coq-8.18' - repo: 'mathcomp/mathcomp' ci_cron_schedule: '25 5 * * 5' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{>= "2.0"}' - description: MathComp's [SSReflect library](https://math-comp.github.io), version 2.0 or later + version: '{>= "2.1.0"}' + description: MathComp's [SSReflect library](https://math-comp.github.io), version 2.1.0 or later - opam: name: coq-mathcomp-algebra description: MathComp's [Algebra library](https://math-comp.github.io) diff --git a/theories/core/Make b/theories/core/Make new file mode 100644 index 0000000..d011439 --- /dev/null +++ b/theories/core/Make @@ -0,0 +1,48 @@ +-arg -w -arg -notation-overridden +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -projection-no-head-constant +-arg -w -arg -duplicate-clear +-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar +-arg -w -arg -ambiguous-paths + +-Q . GraphTheory.core + +edone.v +bounded.v +preliminaries.v +setoid_bigop.v +finmap_plus.v +set_tac.v +bij.v +finite_quotient.v +equiv.v +arc.v +digraph.v +sgraph.v +helly.v +connectivity.v +treewidth.v +minor.v +excluded.v +checkpoint.v +cp_minor.v +smerge.v #(ITP 21) +structures.v +mgraph.v +pttdom.v +mgraph2.v +rewriting.v +reduction.v +open_confluence.v +transfer.v +completeness.v +ptt.v +skeleton.v +mgraph2_tw2.v +extraction_def.v +extraction_iso.v +extraction_top.v +dom.v +partition.v +coloring.v +wpgt.v diff --git a/theories/core/Makefile b/theories/core/Makefile new file mode 100644 index 0000000..3d67475 --- /dev/null +++ b/theories/core/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../../Makefile.common diff --git a/theories/planar/Make b/theories/planar/Make new file mode 100644 index 0000000..1e1dc14 --- /dev/null +++ b/theories/planar/Make @@ -0,0 +1,14 @@ +-arg -w -arg -notation-overridden +-arg -w -arg -redundant-canonical-projection +-arg -w -arg -projection-no-head-constant +-arg -w -arg -duplicate-clear +-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar +-arg -w -arg -ambiguous-paths + +-Q . GraphTheory.planar + +hmap_ops.v +hcycle.v +embedding.v +K4plane.v +wagner.v diff --git a/theories/planar/Makefile b/theories/planar/Makefile new file mode 100644 index 0000000..3d67475 --- /dev/null +++ b/theories/planar/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../../Makefile.common