Skip to content

Commit 8ff85ab

Browse files
palmskogpalmskog
authored
boilerplate for enabling packaging using coq_makefile (#34)
1 parent ab2d6c5 commit 8ff85ab

File tree

6 files changed

+159
-14
lines changed

6 files changed

+159
-14
lines changed

‎Makefile‎

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,4 @@
1-
all: default doc
2-
default: Makefile.coq
3-
make -f Makefile.coq
1+
# -*- Makefile -*-
42

5-
clean: Makefile.coq
6-
make -f Makefile.coq clean
7-
rm -f Makefile.coq
8-
9-
install: Makefile.coq
10-
make -f Makefile.coq install
11-
12-
Makefile.coq: _CoqProject
13-
coq_makefile -f _CoqProject -o Makefile.coq
14-
15-
.PHONY: coq clean install doc
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) $@

‎examples/Make‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
-Q . htt
2+
3+
-arg -w -arg -notation-overridden
4+
-arg -w -arg -redundant-canonical-projection
5+
6+
# release-specific arguments
7+
-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0
8+
-arg -w -arg -deprecated-from-Coq # specific to coq8.21
9+
-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21
10+
11+
exploit.v
12+
gcd.v
13+
counter.v
14+
llist.v
15+
dlist.v
16+
array.v
17+
queue.v
18+
cyclic.v
19+
stack.v
20+
bintree.v
21+
bst.v
22+
kvmaps.v
23+
hashtab.v
24+
bubblesort.v
25+
quicksort.v
26+
congmath.v
27+
congprog.v
28+
tree.v
29+
union_find.v

‎examples/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

‎htt/Make‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-Q . htt
2+
3+
-arg -w -arg -notation-overridden
4+
-arg -w -arg -redundant-canonical-projection
5+
6+
# release-specific arguments
7+
-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0
8+
-arg -w -arg -deprecated-from-Coq # specific to coq8.21
9+
-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21
10+
11+
options.v
12+
domain.v
13+
model.v
14+
heapauto.v

‎htt/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)