blob: 1303b135c5c799affa2181a3131e6c03f481ebe9 (
plain)
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
UNAME_S := $(shell uname -s)
ifeq ($(UNAME_S),Linux)
ARCH := x86_32-linux
endif
ifeq ($(UNAME_S),Darwin)
ARCH := x86_32-macosx
endif
COMPCERTRECDIRS := lib common x86_32 x86 backend cfrontend driver flocq exportclight \
MenhirLib cparser
COQINCLUDES := -R src/common coqup.common -R src/verilog coqup.verilog \
-R src/extraction coqup.extraction -R src/translation coqup.translation \
-R src coqup \
$(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
COQMAKE := $(COQBIN)coq_makefile
VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v)
PREFIX ?= .
.PHONY: all install proof clean extraction test
all: lib/COMPCERTSTAMP
$(MAKE) proof
$(MAKE) compile
lib/COMPCERTSTAMP:
(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
$(MAKE) -C lib/CompCert
touch $@
install:
install -d $(PREFIX)/bin
install -C _build/default/driver/compcert.ini $(PREFIX)/bin/.
install -C _build/default/driver/CoqupDriver.exe $(PREFIX)/bin/coqup
proof: Makefile.coq
$(MAKE) -f Makefile.coq
@rm -f src/extraction/STAMP
extraction: src/extraction/STAMP
test:
./test/test_all.sh ./test
compile: src/extraction/STAMP
@echo "OCaml bin/coqup"
@mkdir -p bin
@dune build driver/CoqupDriver.exe
@cp lib/CompCert/compcert.ini _build/default/driver/.
src/extraction/STAMP:
@echo "COQEXEC ./src/extraction/Extraction.v"
@$(COQEXEC) ./src/extraction/Extraction.v
@touch $@
Makefile.coq:
@echo "COQMAKE Makefile.coq"
$(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq
clean:: Makefile.coq
$(MAKE) -f Makefile.coq clean
rm -f Makefile.coq
clean::
rm -f */*.v.d */*.glob */*.vo */*~ *~
rm -f src/extraction/*.ml src/extraction/*.mli
|