diff options
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | README.md | 6 |
2 files changed, 4 insertions, 5 deletions
@@ -1,4 +1,4 @@ -COQ_ARGS := -R fiat/src Fiat -R bedrock/Bedrock Bedrock +COQ_ARGS := -R bedrock/Bedrock Bedrock MOD_NAME := Crypto SRC_DIR := src MODULES := Curves Galois Rep Specific Tactics Util @@ -20,6 +20,5 @@ clean: Makefile.coq install: coq ln -sfL $(shell pwd)/src $(shell coqtop -where)/user-contrib/Crypto - ln -sfL $(shell pwd)/fiat/src $(shell coqtop -where)/user-contrib/Fiat ln -sfL $(shell pwd)/bedrock/Bedrock $(shell coqtop -where)/user-contrib/Bedrock @@ -1,11 +1,11 @@ -Synthesizing Correct-by-Construction Assembly for Cryptographic Primitives in Fiat +Synthesizing Correct-by-Construction Assembly for Cryptographic Primitives ----- ... which would make a good paper title. To build: - ln -s <FIAT_DIR> fiat - (cd fiat && make fiat-core) + git clone git@github.mit.edu:plv/bedrock.git + ( cd bedrock && $(MAKE) Bedrock/Word.vo ) make |