ConCert/examples/Makefile at master · AU-COBRA/ConCert · GitHub

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
all: examples process-extraction-examples
.PHONY: all

RocqMakefile: _RocqProject
	rocq makefile -f _RocqProject -o RocqMakefile

examples: RocqMakefile
	+@make -f RocqMakefile
.PHONY: examples

clean: RocqMakefile
	+@make -f RocqMakefile clean
	rm -f RocqMakefile
.PHONY: clean

install: RocqMakefile
	+@make -f RocqMakefile install
.PHONY: install

uninstall: RocqMakefile
	+@make -f RocqMakefile uninstall
.PHONY: uninstall

vos: RocqMakefile
	+@make -f RocqMakefile vos

quick: RocqMakefile
	+@make -f RocqMakefile COQEXTRAFLAGS="-unset \"Universe Checking\"" vos

# Forward most things to Rocq makefile. Use 'force' to make this phony.
%: RocqMakefile force
	+@make -f RocqMakefile $@
force: ;

# Do not forward these files
Makefile _RocqProject: ;

process-extraction-examples: examples
	cd ../extraction && ./process-extraction-examples.sh
.PHONY: process-extraction-examples