-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
54 lines (39 loc) · 1.52 KB
/
Makefile
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
COQMAKEFILE=CoqMakefile
LIBNAME=cbpv
SYNTAX=$(shell ls */syntax.sig */*/syntax.sig)
SYNTAXV=$(patsubst %.sig,%.v,$(SYNTAX))
.PHONY: coq syntax clean fullclean
# compile all .v files in _CoqProject
coq: CoqSrc.mk $(VFILES)
make -f CoqSrc.mk
CoqSrc.mk: _CoqProject
coq_makefile -arg '-w -variable-collision,-meta-collision,-require-in-module,-notation-overridden' -f _CoqProject -o CoqSrc.mk
# Remove compiled files
clean:
make -f CoqSrc.mk clean
syntax: $(SYNTAXV)
# Generate the syntax.v files with Autosubst 2 and add imports
# This will run Autosubst 2 and add_imports_to_syntax.pl.
%/syntax.v: %/syntax.sig Makefile
as2-exe -i $< -p Coq > $@
perl add_imports_to_syntax.pl $@
# Generate syntax files and compile all .v files
# This will run Autosubst 2 and add_imports_to_syntax.pl.
fullmake: _CoqProject coq
# Generate syntax.v files and add all .v files to _CoqProject
# This will run Autosubst 2 and add_imports_to_syntax.pl.
_CoqProject : syntax
{ echo "-R . $(LIBNAME) " ; ls autosubst2/*.v common/*.v general/*.v */CBPV/*.v */CBV/*.v */CBN/*.v effects/EffCBV/*.v ; } > _CoqProject
# Remove compiled files and also remove
# the Autosubst-2-generated syntax.v files and auxiliary make files
# Regenerating syntax.v files will run Autosubst 2 and add_imports_to_syntax.pl.
fullclean: clean
rm -f $(SYNTAXV)
rm -f .CoqSrc.mk.d CoqSrc CoqSrc.conf CoqSrc.mk CoqSrc.mk.conf
rm -f _CoqProject
%.vo: %.v CoqSrc.mk
make -f CoqSrc.mk $*.vo
vos: CoqSrc.mk
@make -f CoqSrc.mk vos
%.vos: %.v CoqSrc.mk
@make -f CoqSrc.mk $*.vos