blob: c575bde0889c115461674a860364ecfa4812fd80 (
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
|
COMPCERTRECDIRS := lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \
MenhirLib cparser
COMPCERTCOQINCLUDES := $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
COQINCLUDES := -R src/Common CoqUp.Common -R src/Verilog CoqUp.Verilog -R src/Driver CoqUp.Driver -R src/Extraction CoqUp.Extraction $(COMPCERTCOQINCLUDES)
COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
COQMAKE := "$(COQBIN)coq_makefile"
COQUPDIRS := SMTrans Common Driver Verilog
VS := $(foreach d, $(COQUPDIRS), src/$(d)/*.v)
.PHONY: all install proof clean
all:
(cd lib/CompCert && ./configure x86_64-linux)
$(MAKE) -C lib/CompCert all
$(MAKE) proof
$(MAKE) compile
install:
$(MAKE) -f Makefile.coq install
proof: Makefile.coq
$(MAKE) -f Makefile.coq
extraction: src/Extraction/STAMP
compile: src/Extraction/STAMP
@echo "OCaml bin/coqup"
@mkdir -p bin
@dune build src/Driver/Driver.exe
@cp _build/default/src/Driver/Driver.exe bin/coqup
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 */*~ *~
|