blob: f477613aeb4628069325f1b25eb455aefbbcbcdd (
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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
UNAME_S := $(shell uname -s)
ifeq ($(UNAME_S),Linux)
ARCH := verilog-linux
endif
ifeq ($(UNAME_S),Darwin)
ARCH := verilog-macosx
endif
ifeq ($(UNAME_S),FreeBSD)
ARCH := verilog-bsd
endif
COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser
COQINCLUDES := -R src vericert \
$(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) \
-R lib/CompCert/flocq Flocq \
-R lib/CompCert/MenhirLib MenhirLib
COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
COQMAKE := $(COQBIN)coq_makefile
COQDOCFLAGS := --no-lib-name -l
ALECTRYON_OPTS := --no-header --html-minification --long-line-threshold 80 \
--coq-driver sertop_noexec $(COQINCLUDES)
VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, $(wildcard src/$(d)/*.v))
PREFIX ?= .
.PHONY: all install proof clean extraction test force
all: lib/COMPCERTSTAMP
$(MAKE) proof
$(MAKE) compile
lib/CompCert/Makefile.config: lib/CompCert/configure
(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
touch $@
install: # doc/vericert.1
sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
install -d $(PREFIX)/bin
install -C -m 644 _build/default/driver/compcert.ini $(PREFIX)/bin
install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert
install -d $(PREFIX)/share/man/man1
install -C -m 644 $< $(PREFIX)/share/man/man1
proof: Makefile.coq
$(MAKE) -f Makefile.coq
@rm -f src/extraction/STAMP
doc-html: $(patsubst src/%.v,html/%.html,$(VS))
html/%.html: src/%.v
@mkdir -p $(dir $@)
@echo "ALECTRYON" $@; alectryon $(ALECTRYON_OPTS) $< -o $@
coqdoc: Makefile.coq
$(MAKE) COQDOCFLAGS="$(COQDOCFLAGS)" -f Makefile.coq html
cp ./docs/res/coqdoc.css html/.
doc-pdf: Makefile.coq
$(MAKE) COQDOCFLAGS="$(COQDOCFLAGS)" -f Makefile.coq all.tex
extraction: src/extraction/STAMP
test:
$(MAKE) -C test
compile: src/extraction/STAMP
@echo "OCaml bin/vericert"
@mkdir -p bin
@dune build driver/VericertDriver.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 _CoqProject: force
@echo "COQMAKE Makefile.coq"
$(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq
echo "$(COQINCLUDES)" >_CoqProject
force:
docs/vericert.1:
$(MAKE) -C docs vericert.1
detangle-all:
emacs --batch --eval "(progn(require 'org)(require 'ob-tangle)\
(setq org-src-preserve-indentation t)\
$(foreach vs,$(VS),(org-babel-detangle \"$(vs)\"))\
(org-save-all-org-buffers))"
clean:: Makefile.coq
$(MAKE) -f Makefile.coq clean
$(MAKE) -C test clean
rm -f Makefile.coq
clean::
rm -f */*.v.d */*.glob */*.vo */*~ *~
rm -f src/extraction/*.ml src/extraction/*.mli
|
