Skip to content

Commit 56179ba

Browse files
palmskogpalmskog
committed
enable using coq_makefile for opam packages
1 parent ca570af commit 56179ba

File tree

16 files changed

+247
-27
lines changed

16 files changed

+247
-27
lines changed

‎.github/workflows/docker-action.yml‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
# This file was generated from `meta.yml`, please do not edit manually.
2-
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
31
name: Docker CI
42

53
on:
@@ -18,8 +16,10 @@ jobs:
1816
matrix:
1917
image:
2018
- 'mathcomp/mathcomp-dev:coq-dev'
19+
- 'mathcomp/mathcomp-dev:coq-8.20'
2120
- 'mathcomp/mathcomp-dev:coq-8.19'
2221
- 'mathcomp/mathcomp-dev:coq-8.18'
22+
- 'mathcomp/mathcomp:2.3.0-coq-8.20'
2323
- 'mathcomp/mathcomp:2.2.0-coq-8.19'
2424
- 'mathcomp/mathcomp:2.1.0-coq-8.18'
2525
- 'mathcomp/mathcomp:2.1.0-coq-8.17'
@@ -38,46 +38,46 @@ jobs:
3838
startGroup "Build gaia-theory-of-sets dependencies"
3939
opam pin add -n -y -k path coq-gaia-theory-of-sets .
4040
opam update -y
41-
opam install -y -j 2 coq-gaia-theory-of-sets --deps-only
41+
opam install -y -j $(nproc) coq-gaia-theory-of-sets --deps-only
4242
endGroup
4343
startGroup "Build gaia-theory-of-sets"
44-
opam install -y -v -j 2 coq-gaia-theory-of-sets
44+
opam install -y -v -j $(nproc) coq-gaia-theory-of-sets
4545
opam list
4646
endGroup
4747
startGroup "Build gaia-schutte dependencies"
4848
opam pin add -n -y -k path coq-gaia-schutte .
4949
opam update -y
50-
opam install -y -j 2 coq-gaia-schutte --deps-only
50+
opam install -y -j $(nproc) coq-gaia-schutte --deps-only
5151
endGroup
5252
startGroup "Build gaia-schutte"
53-
opam install -y -v -j 2 coq-gaia-schutte
53+
opam install -y -v -j $(nproc) coq-gaia-schutte
5454
opam list
5555
endGroup
5656
startGroup "Build gaia-ordinals dependencies"
5757
opam pin add -n -y -k path coq-gaia-ordinals .
5858
opam update -y
59-
opam install -y -j 2 coq-gaia-ordinals --deps-only
59+
opam install -y -j $(nproc) coq-gaia-ordinals --deps-only
6060
endGroup
6161
startGroup "Build gaia-ordinals"
62-
opam install -y -v -j 2 coq-gaia-ordinals
62+
opam install -y -v -j $(nproc) coq-gaia-ordinals
6363
opam list
6464
endGroup
6565
startGroup "Build gaia-numbers dependencies"
6666
opam pin add -n -y -k path coq-gaia-numbers .
6767
opam update -y
68-
opam install -y -j 2 coq-gaia-numbers --deps-only
68+
opam install -y -j $(nproc) coq-gaia-numbers --deps-only
6969
endGroup
7070
startGroup "Build gaia-numbers"
71-
opam install -y -v -j 2 coq-gaia-numbers
71+
opam install -y -v -j $(nproc) coq-gaia-numbers
7272
opam list
7373
endGroup
7474
startGroup "Build gaia-stern dependencies"
7575
opam pin add -n -y -k path coq-gaia-stern .
7676
opam update -y
77-
opam install -y -j 2 coq-gaia-stern --deps-only
77+
opam install -y -j $(nproc) coq-gaia-stern --deps-only
7878
endGroup
7979
startGroup "Build gaia-stern"
80-
opam install -y -v -j 2 coq-gaia-stern
80+
opam install -y -v -j $(nproc) coq-gaia-stern
8181
opam list
8282
endGroup
8383
startGroup "Uninstallation test"

‎Makefile‎

Lines changed: 3 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,4 @@
1-
all: Makefile.coq
2-
@+$(MAKE) -f Makefile.coq all
1+
# -*- Makefile -*-
32

4-
clean: Makefile.coq
5-
@+$(MAKE) -f Makefile.coq cleanall
6-
@rm -f Makefile.coq Makefile.coq.conf
7-
8-
Makefile.coq: _CoqProject
9-
$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
10-
11-
force _CoqProject Makefile: ;
12-
13-
%: Makefile.coq force
14-
@+$(MAKE) -f Makefile.coq $@
15-
16-
.PHONY: all clean force
3+
# --------------------------------------------------------------------
4+
include Makefile.common

‎Makefile.common‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
# -*- Makefile -*-
2+
3+
######################################################################
4+
# USAGE: #
5+
# The rules this-config::, this-build::, this-distclean::, #
6+
# pre-makefile::, this-clean:: and __always__:: may be extended #
7+
# Additionally, the following variables may be customized: #
8+
SUBDIRS?=
9+
COQBIN?=$(dir $(shell which coqtop))
10+
COQMAKEFILE?=$(COQBIN)coq_makefile
11+
COQDEP?=$(COQBIN)coqdep
12+
COQPROJECT?=_CoqProject
13+
COQMAKEOPTIONS?=
14+
COQMAKEFILEOPTIONS?=
15+
V?=
16+
VERBOSE?=V
17+
######################################################################
18+
19+
# local context: -----------------------------------------------------
20+
.PHONY: all config build clean distclean __always__
21+
.SUFFIXES:
22+
23+
H:= $(if $(VERBOSE),,@) # not used yet
24+
TOP = $(dir $(lastword $(MAKEFILE_LIST)))
25+
COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
26+
BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
27+
| wc -l | sed 's/ *//g')
28+
29+
# coq version:
30+
ifneq "$(BRANCH_coq)" "0"
31+
COQVVV:= dev
32+
else
33+
COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1)
34+
endif
35+
36+
COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
37+
COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)
38+
39+
# all: ---------------------------------------------------------------
40+
all: config build
41+
42+
# Makefile.coq: ------------------------------------------------------
43+
.PHONY: pre-makefile
44+
45+
Makefile.coq: pre-makefile $(COQPROJECT) Makefile
46+
$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
47+
48+
# Global config, build, clean and distclean --------------------------
49+
config: sub-config this-config
50+
51+
build: sub-build this-build
52+
53+
clean: sub-clean this-clean
54+
55+
distclean: sub-distclean this-distclean
56+
57+
# Local config, build, clean and distclean ---------------------------
58+
.PHONY: this-config this-build this-distclean this-clean
59+
60+
this-config:: __always__
61+
62+
this-build:: this-config Makefile.coq
63+
+$(COQMAKE)
64+
65+
this-distclean:: this-clean
66+
rm -f Makefile.coq Makefile.coq.conf Makefile.coq
67+
68+
this-clean:: __always__
69+
@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
70+
71+
# Install target -----------------------------------------------------
72+
.PHONY: install
73+
74+
install: __always__ Makefile.coq
75+
$(COQMAKE) install
76+
# counting lines of Coq code -----------------------------------------
77+
.PHONY: count
78+
79+
COQFILES = $(shell grep '.v$$' $(COQPROJECT))
80+
81+
count:
82+
@coqwc $(COQFILES) | tail -1 | \
83+
awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
84+
# Additionally cleaning backup (*~) files ----------------------------
85+
this-distclean::
86+
rm -f $(shell find . -name '*~')
87+
88+
# Make in SUBDIRS ----------------------------------------------------
89+
ifdef SUBDIRS
90+
sub-%: __always__
91+
@set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
92+
else
93+
sub-%: __always__
94+
@true
95+
endif
96+
97+
# Make of individual .vo ---------------------------------------------
98+
%.vo: __always__ Makefile.coq
99+
+$(COQMAKE) $@

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ and number theory.
3939
- Compatible Coq versions: 8.16 or later
4040
- Additional dependencies:
4141
- [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
42+
- [Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder)
4243
- [MathComp algebra](https://math-comp.github.io)
4344
- Coq namespace: `gaia`
4445
- Related publication(s):

‎coq-gaia-schutte.opam‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ depends: [
1717
"dune" {>= "3.5"}
1818
"coq" {>= "8.16"}
1919
"coq-mathcomp-ssreflect" {>= "2.0"}
20+
"coq-hierarchy-builder" {>= "1.6.0"}
2021
]
2122

2223
tags: [

‎meta.yml‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,11 @@ dependencies:
7070
version: '{>= "2.0"}'
7171
description: |-
7272
[MathComp ssreflect 2.0 or later](https://math-comp.github.io)
73+
- opam:
74+
name: coq-hierarchy-builder
75+
version: '{>= "1.6.0"}'
76+
description: |-
77+
[Hierarchy Builder 1.6.0 or later](https://github.com/math-comp/hierarchy-builder)
7378
- opam:
7479
name: coq-mathcomp-algebra
7580
description: |-
@@ -78,10 +83,14 @@ dependencies:
7883
tested_coq_opam_versions:
7984
- version: 'coq-dev'
8085
repo: 'mathcomp/mathcomp-dev'
86+
- version: 'coq-8.20'
87+
repo: 'mathcomp/mathcomp-dev'
8188
- version: 'coq-8.19'
8289
repo: 'mathcomp/mathcomp-dev'
8390
- version: 'coq-8.18'
8491
repo: 'mathcomp/mathcomp-dev'
92+
- version: '2.3.0-coq-8.20'
93+
repo: 'mathcomp/mathcomp'
8594
- version: '2.2.0-coq-8.19'
8695
repo: 'mathcomp/mathcomp'
8796
- version: '2.1.0-coq-8.18'

‎theories/numbers/Make‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
-Q . gaia.numbers
2+
3+
-arg -w -arg -notation-overridden
4+
-arg -w -arg -notation-incompatible-format
5+
-arg -w -arg -ambiguous-paths
6+
-arg -w -arg -deprecated-hint-without-locality
7+
-arg -w -arg -deprecated-ident-entry
8+
-arg -w -arg -deprecated-hint-rewrite-without-locality
9+
10+
ssetc.v
11+
ssetr.v
12+
ssetz.v
13+
ssetq1.v
14+
ssetq2.v
15+
ssete6.v
16+
ssete7.v
17+
ssete8.v
18+
ssete11.v

‎theories/numbers/Makefile‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
# -*- Makefile -*-
2+
3+
# setting variables
4+
COQPROJECT?=Make
5+
6+
# Main Makefile
7+
include ../../Makefile.common

‎theories/ordinals/Make‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
-Q . gaia.ordinals
2+
3+
-arg -w -arg -notation-overridden
4+
-arg -w -arg -notation-incompatible-format
5+
-arg -w -arg -ambiguous-paths
6+
-arg -w -arg -deprecated-hint-without-locality
7+
-arg -w -arg -deprecated-ident-entry
8+
-arg -w -arg -deprecated-hint-rewrite-without-locality
9+
10+
sset11.v
11+
sset12.v
12+
sset13a.v
13+
sset13b.v
14+
sset13c.v
15+
sset14.v
16+
sset15.v
17+
sset16a.v
18+
sset16b.v
19+
sset16c.v
20+
sset17.v
21+
ssete10.v
22+
ssete2.v
23+
ssete3.v
24+
ssete4.v
25+
ssete5.v

‎theories/ordinals/Makefile‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
# -*- Makefile -*-
2+
3+
# setting variables
4+
COQPROJECT?=Make
5+
6+
# Main Makefile
7+
include ../../Makefile.common

0 commit comments

Comments
 (0)