introduce makefiles in subdirectories, modify opam packages to use them

.github/workflows/docker-action.yml

@@ -28,12 +28,34 @@ jobs:
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-fourcolor.opam'
           custom_image: ${{ matrix.image }}
-
+          custom_script: |
+            {{before_install}}
+            startGroup "Build fourcolor-reals dependencies"
+              opam pin add -n -y -k path coq-fourcolor-reals .
+              opam update -y
+              opam install -y -j $(nproc) coq-fourcolor-reals --deps-only
+            endGroup
+            startGroup "Build fourcolor-reals"
+              opam install -y -v -j $(nproc) coq-fourcolor-reals
+              opam list
+            endGroup
+            startGroup "Build fourcolor dependencies"
+              opam pin add -n -y -k path coq-fourcolor .
+              opam update -y
+              opam install -y -j $(nproc) coq-fourcolor --deps-only
+            endGroup
+            startGroup "Build fourcolor"
+              opam install -y -v -j $(nproc) coq-fourcolor
+              opam list
+            endGroup
+            startGroup "Uninstallation test"
+              opam remove -y coq-fourcolor
+              opam remove -y coq-fourcolor-reals
+            endGroup
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

Makefile

@@ -1,25 +1,4 @@
-# KNOWNTARGETS will not be passed along to CoqMakefile
-KNOWNTARGETS := Makefile.coq
-# KNOWNFILES will not get implicit targets from the final rule, and so
-# depending on them won't invoke the submake
-# Warning: These files get declared as PHONY, so any targets depending
-# on them always get rebuilt
-KNOWNFILES   := Makefile _CoqProject
+# -*- Makefile -*-
 
-.DEFAULT_GOAL := invoke-coqmakefile
-
-Makefile.coq: Makefile _CoqProject
-	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
-
-invoke-coqmakefile: Makefile.coq
-	$(MAKE) --no-print-directory -f Makefile.coq $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
-
-.PHONY: invoke-coqmakefile $(KNOWNFILES)
-
-####################################################################
-##                      Your targets here                         ##
-####################################################################
-
-# This should be the last rule, to handle any targets not declared above
-%: invoke-coqmakefile
-	@true
+# --------------------------------------------------------------------
+include Makefile.common

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) $@

coq-fourcolor-reals.opam

@@ -0,0 +1,30 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+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: "Interface for real numbers used in the Four Color Theorem"
+description: """
+An axiomatization of the setoid of classical real numbers, along
+with proofs of properties such as categoricity."""
+
+build: [make "-C" "theories/reals" "-j%{jobs}%"]
+install: [make "-C" "theories/reals" "install"]
+depends: [
+  "coq" {>= "8.16"}
+  "coq-mathcomp-ssreflect" {>= "2.1.0"}
+  "coq-mathcomp-algebra" 
+]
+
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword:real numbers"
+  "logpath:fourcolor.reals"
+]
+authors: [
+  "Georges Gonthier"
+]

coq-fourcolor.opam

@@ -1,6 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
 maintainer: "[email protected]"
 version: "dev"
@@ -17,21 +14,22 @@ 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 "-j%{jobs}%"]
-install: [make "install"]
+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"
+  "logpath:fourcolor.proof"
 ]
 authors: [
   "Georges Gonthier"

theories/proof/Make

@@ -0,0 +1,123 @@
+-Q . fourcolor.proof
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-instance-without-locality
+
+dedekind.v
+realplane.v
+hypermap.v
+walkup.v
+jordan.v
+geometry.v
+cube.v
+color.v
+coloring.v
+patch.v
+sew.v
+snip.v
+revsnip.v
+chromogram.v
+kempe.v
+ctree.v
+gtree.v
+dyck.v
+initctree.v
+initgtree.v
+gtreerestrict.v
+ctreerestrict.v
+kempetree.v
+cfmap.v
+configurations.v
+cfcolor.v
+cfcontract.v
+cfreducible.v
+birkhoff.v
+contract.v
+embed.v
+quiz.v
+quiztree.v
+cfquiz.v
+part.v
+redpart.v
+discharge.v
+hubcap.v
+grid.v
+gridmap.v
+matte.v
+finitize.v
+approx.v
+discretize.v
+present.v
+present5.v
+present6.v
+present7.v
+present8.v
+present9.v
+present10.v
+present11.v
+job001to106.v
+job107to164.v
+job165to189.v
+job190to206.v
+job207to214.v
+task001to214.v
+job215to218.v
+job219to222.v
+job223to226.v
+job227to230.v
+job231to234.v
+task215to234.v
+job235to238.v
+job239to253.v
+job254to270.v
+job271to278.v
+job279to282.v
+task235to282.v
+job283to286.v
+job287to290.v
+job291to294.v
+job295to298.v
+job299to302.v
+task283to302.v
+job303to306.v
+job307to310.v
+job311to314.v
+job315to318.v
+job319to322.v
+task303to322.v
+job323to383.v
+job384to398.v
+job399to438.v
+job439to465.v
+job466to485.v
+task323to485.v
+job486to489.v
+job490to494.v
+job495to498.v
+job499to502.v
+job503to506.v
+task486to506.v
+job507to510.v
+job511to516.v
+job517to530.v
+job531to534.v
+job535to541.v
+task507to541.v
+job542to545.v
+job546to549.v
+job550to553.v
+job554to562.v
+job563to588.v
+task542to588.v
+job589to610.v
+job611to617.v
+job618to622.v
+job623to633.v
+task589to633.v
+unavoidability.v
+reducibility.v
+combinatorial4ct.v
+fourcolor.v

theories/proof/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../../Makefile.common

theories/reals/Make

@@ -0,0 +1,12 @@
+-Q . fourcolor.reals
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-instance-without-locality
+
+real.v
+realsyntax.v
+realprop.v
+realcategorical.v

theories/reals/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../../Makefile.common