aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2023-06-19 13:41:06 +0100
committerYann Herklotz <git@yannherklotz.com>2023-06-19 13:41:26 +0100
commit323f262727ac3a4b129bdaeaa21083d8daa5184c (patch)
tree451bac2293088b41511223521f4447e1ad5f3448
parent0a7392ef3694d681b52e302cdc8b68cf04ea4234 (diff)
downloadvericert-323f262727ac3a4b129bdaeaa21083d8daa5184c.tar.gz
vericert-323f262727ac3a4b129bdaeaa21083d8daa5184c.zip
Update makefile to build cohpred
-rw-r--r--Makefile8
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index c7e7752..3d8dfff 100644
--- a/Makefile
+++ b/Makefile
@@ -16,7 +16,7 @@ COQINCLUDES := -R src vericert \
-R lib/CompCert/flocq Flocq \
-R lib/CompCert/MenhirLib MenhirLib \
-R src TVSMT \
- -R lib/cohpred/lib/smtcoq/src SMTCoq \
+ -R lib/cohpred/smtcoq/src SMTCoq \
-I lib/smtcoq/src \
-I lib/smtcoq/src/bva \
-I lib/smtcoq/src/classes \
@@ -46,7 +46,7 @@ PREFIX ?= .
.PHONY: all install proof clean extraction test force
-all: lib/COMPCERTSTAMP
+all: lib/COMPCERTSTAMP lib/COHPREDSTAMP
$(MAKE) proof
$(MAKE) compile
@@ -57,6 +57,10 @@ lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
touch $@
+lib/COHPREDSTAMP:
+ $(MAKE) -C lib/cohpred
+ touch lib/COHPREDSTAMP
+
install: # doc/vericert.1
sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
install -d $(PREFIX)/bin