aboutsummaryrefslogtreecommitdiff
path: root/.make
diff options
context:
space:
mode:
Diffstat (limited to '.make')
-rw-r--r--.make/cc.mk20
-rw-r--r--.make/coq.mk28
2 files changed, 0 insertions, 48 deletions
diff --git a/.make/cc.mk b/.make/cc.mk
deleted file mode 100644
index 58724089a..000000000
--- a/.make/cc.mk
+++ /dev/null
@@ -1,20 +0,0 @@
-# © 2012–2015 the Massachusetts Institute of Technology
-# @author bbaren
-
-CC = clang
-CXX = clang++
-
-CPPFLAGS = \
- -Wall \
- -D_FORTIFY_SOURCE=2
-
-CXXFLAGS = \
- -std=c++11 \
- -ftrapv \
- -fstack-protector-strong --param=ssp-buffer-size=4 \
- -fPIC \
- -O2 -g \
- -ffunction-sections -fdata-sections \
- -Weverything -Wno-c++98-compat
-
-LDFLAGS = -fPIE -pie
diff --git a/.make/coq.mk b/.make/coq.mk
deleted file mode 100644
index bab225be7..000000000
--- a/.make/coq.mk
+++ /dev/null
@@ -1,28 +0,0 @@
-# © 2012–2015 the Massachusetts Institute of Technology
-# @author bbaren + rsloan
-
-COQC = coqc
-COQDEP = coqdep
-
-COMPILE.v = $(COQC) -q $(COQLIBS)
-
-.PHONY: check_fiat check_bedrock
-
-check_fiat:
- @perl -e \
- 'if(! -d "./fiat") { print("you need to link fiat to ./fiat\n"); exit(1) }'
-
-check_bedrock:
- @perl -e \
- 'if(! -d "./bedrock") { print("you need to link bedrock to ./bedrock\n"); exit(1) }'
-
-%.vo %.glob: %.v.d
- $(COMPILE.v) $*
-
-%.v.d: %.v
- @$(COQDEP) -I . $(COQLIBS) "$<" >"$@" \
- || (RV=$$?; rm -f "$@"; exit $${RV})
-
-define coq-generated
-$1.vo $1.v.d $1.glob
-endef