enable using coq_makefile for opam packages

.github/workflows/docker-action.yml

@@ -1,5 +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.
 name: Docker CI
 
 on:
@@ -18,8 +16,10 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.20'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.1.0-coq-8.18'
           - 'mathcomp/mathcomp:2.1.0-coq-8.17'
@@ -38,46 +38,46 @@ jobs:
             startGroup "Build gaia-theory-of-sets dependencies"
               opam pin add -n -y -k path coq-gaia-theory-of-sets .
               opam update -y
-              opam install -y -j 2 coq-gaia-theory-of-sets --deps-only
+              opam install -y -j $(nproc) coq-gaia-theory-of-sets --deps-only
             endGroup
             startGroup "Build gaia-theory-of-sets"
-              opam install -y -v -j 2 coq-gaia-theory-of-sets
+              opam install -y -v -j $(nproc) coq-gaia-theory-of-sets
               opam list
             endGroup
             startGroup "Build gaia-schutte dependencies"
               opam pin add -n -y -k path coq-gaia-schutte .
               opam update -y
-              opam install -y -j 2 coq-gaia-schutte --deps-only
+              opam install -y -j $(nproc) coq-gaia-schutte --deps-only
             endGroup
             startGroup "Build gaia-schutte"
-              opam install -y -v -j 2 coq-gaia-schutte
+              opam install -y -v -j $(nproc) coq-gaia-schutte
               opam list
             endGroup
             startGroup "Build gaia-ordinals dependencies"
               opam pin add -n -y -k path coq-gaia-ordinals .
               opam update -y
-              opam install -y -j 2 coq-gaia-ordinals --deps-only
+              opam install -y -j $(nproc) coq-gaia-ordinals --deps-only
             endGroup
             startGroup "Build gaia-ordinals"
-              opam install -y -v -j 2 coq-gaia-ordinals
+              opam install -y -v -j $(nproc) coq-gaia-ordinals
               opam list
             endGroup
             startGroup "Build gaia-numbers dependencies"
               opam pin add -n -y -k path coq-gaia-numbers .
               opam update -y
-              opam install -y -j 2 coq-gaia-numbers --deps-only
+              opam install -y -j $(nproc) coq-gaia-numbers --deps-only
             endGroup
             startGroup "Build gaia-numbers"
-              opam install -y -v -j 2 coq-gaia-numbers
+              opam install -y -v -j $(nproc) coq-gaia-numbers
               opam list
             endGroup
             startGroup "Build gaia-stern dependencies"
               opam pin add -n -y -k path coq-gaia-stern .
               opam update -y
-              opam install -y -j 2 coq-gaia-stern --deps-only
+              opam install -y -j $(nproc) coq-gaia-stern --deps-only
             endGroup
             startGroup "Build gaia-stern"
-              opam install -y -v -j 2 coq-gaia-stern
+              opam install -y -v -j $(nproc) coq-gaia-stern
               opam list
             endGroup
             startGroup "Uninstallation test"

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

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

README.md

@@ -39,6 +39,7 @@ and number theory.
 - Compatible Coq versions: 8.16 or later
 - Additional dependencies:
   - [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+  - [Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder)
   - [MathComp algebra](https://math-comp.github.io)
 - Coq namespace: `gaia`
 - Related publication(s):

coq-gaia-schutte.opam

@@ -17,6 +17,7 @@ depends: [
   "dune" {>= "3.5"}
   "coq" {>= "8.16"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-hierarchy-builder" {>= "1.6.0"}
 ]
 
 tags: [

meta.yml

@@ -70,6 +70,11 @@ dependencies:
     version: '{>= "2.0"}'
   description: |-
     [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.6.0"}'
+  description: |-
+    [Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
@@ -78,10 +83,14 @@ dependencies:
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.20'
+  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.19'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
+- version: '2.3.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.18'

theories/numbers/Make

@@ -0,0 +1,18 @@
+-Q . gaia.numbers
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -notation-incompatible-format
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-ident-entry
+-arg -w -arg -deprecated-hint-rewrite-without-locality
+
+ssetc.v
+ssetr.v
+ssetz.v
+ssetq1.v
+ssetq2.v
+ssete6.v
+ssete7.v
+ssete8.v
+ssete11.v

theories/numbers/Makefile

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

theories/ordinals/Make

@@ -0,0 +1,25 @@
+-Q . gaia.ordinals
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -notation-incompatible-format
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-ident-entry
+-arg -w -arg -deprecated-hint-rewrite-without-locality
+
+sset11.v
+sset12.v
+sset13a.v
+sset13b.v
+sset13c.v
+sset14.v
+sset15.v
+sset16a.v
+sset16b.v
+sset16c.v
+sset17.v
+ssete10.v
+ssete2.v
+ssete3.v
+ssete4.v
+ssete5.v

theories/ordinals/Makefile

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

theories/schutte/Make

@@ -0,0 +1,10 @@
+-Q . gaia.schutte
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -notation-incompatible-format
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-ident-entry
+-arg -w -arg -deprecated-hint-rewrite-without-locality
+
+ssete9.v

theories/schutte/Makefile

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

theories/sets/Make

@@ -0,0 +1,23 @@
+-Q . gaia.sets
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -notation-incompatible-format
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-ident-entry
+-arg -w -arg -deprecated-hint-rewrite-without-locality
+
+sset10.v
+sset18.v
+sset19.v
+sset1.v 
+sset2_aux.v
+sset2.v
+sset3.v
+sset4.v
+sset5.v
+sset6.v
+sset7.v
+sset8.v
+sset9.v
+ssete1.v

theories/sets/Makefile

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

theories/stern/Make

@@ -0,0 +1,11 @@
+-Q . gaia.stern
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -notation-incompatible-format
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-ident-entry
+-arg -w -arg -deprecated-hint-rewrite-without-locality
+
+fibm.v
+stern.v

theories/stern/Makefile

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