From d4305d4abd7254e9fc7c5e0636d9dd5fa770455f Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Wed, 6 Nov 2024 09:51:55 +0100 Subject: [PATCH] introduce makefiles in subdirectories, modify opam packages to use them --- .github/workflows/docker-action.yml | 28 ++++++- Makefile | 27 +----- Makefile.common | 99 ++++++++++++++++++++++ coq-fourcolor-reals.opam | 30 +++++++ coq-fourcolor.opam | 10 +-- theories/proof/Make | 123 ++++++++++++++++++++++++++++ theories/proof/Makefile | 7 ++ theories/reals/Make | 12 +++ theories/reals/Makefile | 7 ++ 9 files changed, 310 insertions(+), 33 deletions(-) create mode 100644 Makefile.common create mode 100644 coq-fourcolor-reals.opam create mode 100644 theories/proof/Make create mode 100644 theories/proof/Makefile create mode 100644 theories/reals/Make create mode 100644 theories/reals/Makefile diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 3a20fb9..d99f23b 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/Makefile b/Makefile index 257ce2a..d5aa0bf 100644 --- a/Makefile +++ b/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 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/coq-fourcolor-reals.opam b/coq-fourcolor-reals.opam new file mode 100644 index 0000000..15b62a1 --- /dev/null +++ b/coq-fourcolor-reals.opam @@ -0,0 +1,30 @@ +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: "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" +] diff --git a/coq-fourcolor.opam b/coq-fourcolor.opam index 94846bf..cfe2477 100644 --- a/coq-fourcolor.opam +++ b/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: "palmskog@gmail.com" version: "dev" @@ -17,13 +14,14 @@ 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: [ @@ -31,7 +29,7 @@ tags: [ "keyword:Four color theorem" "keyword:small scale reflection" "keyword:Mathematical Components" - "logpath:fourcolor" + "logpath:fourcolor.proof" ] authors: [ "Georges Gonthier" diff --git a/theories/proof/Make b/theories/proof/Make new file mode 100644 index 0000000..e4eef2c --- /dev/null +++ b/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 diff --git a/theories/proof/Makefile b/theories/proof/Makefile new file mode 100644 index 0000000..3d67475 --- /dev/null +++ b/theories/proof/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../../Makefile.common diff --git a/theories/reals/Make b/theories/reals/Make new file mode 100644 index 0000000..58a8452 --- /dev/null +++ b/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 diff --git a/theories/reals/Makefile b/theories/reals/Makefile new file mode 100644 index 0000000..3d67475 --- /dev/null +++ b/theories/reals/Makefile @@ -0,0 +1,7 @@ +# -*- Makefile -*- + +# setting variables +COQPROJECT?=Make + +# Main Makefile +include ../../Makefile.common