aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-03-31 15:31:41 +0100
committerYann Herklotz <git@yannherklotz.com>2020-03-31 15:31:41 +0100
commit2d11fe952455efbb66a4cf9a59d9e39425bd522c (patch)
treef27bedc03b229985ebefe77b28b49ba0be795c20 /Makefile
parentfa18be8c99b1dcd8c55f0f6928aeaf74731f1ad7 (diff)
downloadvericert-2d11fe952455efbb66a4cf9a59d9e39425bd522c.tar.gz
vericert-2d11fe952455efbb66a4cf9a59d9e39425bd522c.zip
Fix the Makefile build
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile15
1 files changed, 9 insertions, 6 deletions
diff --git a/Makefile b/Makefile
index 17cf636..1b4e39b 100644
--- a/Makefile
+++ b/Makefile
@@ -14,27 +14,30 @@ COQUPDIRS := translation common verilog
VSSUBDIR := $(foreach d, $(COQUPDIRS), src/$(d)/*.v)
VS := src/Compiler.v $(VSSUBDIR)
-.PHONY: all install proof clean
+PREFIX ?= .
+
+.PHONY: all install proof clean extraction
all:
- (cd lib/CompCert && ./configure x86_64-linux)
- $(MAKE) -C lib/CompCert all
$(MAKE) proof
$(MAKE) compile
install:
- $(MAKE) -f Makefile.coq 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
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
+ @dune build driver/CoqupDriver.exe
+ @cp lib/CompCert/compcert.ini _build/default/driver/.
src/extraction/STAMP:
@echo "COQEXEC ./src/extraction/Extraction.v"