diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-06-17 23:50:09 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-06-17 23:50:09 -0400 |
| commit | 10787528349ef926b09acb219d1fd6acd1e041e7 (patch) | |
| tree | ff8fb23d6f899def7a24dfb9fc06f9ed9c6997db | |
| parent | d81a299db761650b6c9405cd19335cb54ea0b2ad (diff) | |
| parent | 7dc373e4c82f3e7a37832321abc9057cb55348f2 (diff) | |
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
| -rw-r--r-- | .mailmap | 18 | ||||
| -rw-r--r-- | Makefile | 16 | ||||
| -rw-r--r-- | README.md | 6 |
3 files changed, 37 insertions, 3 deletions
diff --git a/.mailmap b/.mailmap new file mode 100644 index 000000000..7c61488f3 --- /dev/null +++ b/.mailmap @@ -0,0 +1,18 @@ +## This file allows joining different accounts of a single person. +## Cf for instance: git shortlog -nse. More details via: man git shortlog + +# having the same name <email> name <email> on a line will fix capitalization +Adam Chlipala <adamc@csail.mit.edu> Adam Chlipala <adamc@csail.mit.edu> +Adam Chlipala <adam@chlipala.net> Adam Chlipala <adamc@csail.mit.edu> +Andres Erbsen <andreser@mit.edu> Andres Erbsen <andreser@mit.edu> +Jade Philipoom <jadep@mit.edu> Jade Philipoom <jadep@mit.edu> +jadep <jade.philipoom@gmail.com> Jade Philipoom <jadep@mit.edu> +jadep <jadep@mit.edu> Jade Philipoom <jadep@mit.edu> +Jason Gross <jgross@mit.edu> Jason Gross <jgross@mit.edu> +Robert Sloan <varomodt@gmail.com> Robert Sloan <varomodt@gmail.com> +Robert Sloan <varomodt@Roberts-MacBook.local> Robert Sloan <varomodt@gmail.com> +Robert Sloan <rsloan@sumologic.com> Robert Sloan <varomodt@gmail.com> +Robert Sloan <varomodt@dhcp-18-189-26-21.dyn.MIT.EDU> Robert Sloan <varomodt@gmail.com> +Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU> Robert Sloan <varomodt@gmail.com> +Rob Sloan <varomodt@gmail.com> Robert Sloan <varomodt@gmail.com> +varomodt <varomodt@localhost.localdomain> Robert Sloan <varomodt@gmail.com> @@ -4,10 +4,21 @@ SRC_DIR := src .PHONY: coq clean install coqprime-8.4 coqprime-8.5 coqprime update-_CoqProject .DEFAULT_GOAL := coq +VERBOSE = 0 + +SILENCE_COQC_0 = @echo "COQC $<"; # +SILENCE_COQC_1 = +SILENCE_COQC = $(SILENCE_COQC_$(VERBOSE)) + +SILENCE_COQDEP_0 = @echo "COQDEP $<"; # +SILENCE_COQDEP_1 = +SILENCE_COQDEP = $(SILENCE_COQDEP_$(VERBOSE)) + SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' update-_CoqProject:: - (echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R Bedrock Bedrock'; (git ls-files 'src/*.v' 'Bedrock/*.v' | $(SORT_COQPROJECT))) > _CoqProject + $(VECHO) "GIT LS-FILES *.V > _COQPROJECT" + $(Q)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R Bedrock Bedrock'; (git ls-files 'src/*.v' 'Bedrock/*.v' | $(SORT_COQPROJECT))) > _CoqProject coq: coqprime Makefile.coq $(MAKE) -f Makefile.coq @@ -28,7 +39,8 @@ coqprime-8.5: $(MAKE) -C coqprime-8.5 Makefile.coq: Makefile _CoqProject - $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + $(VECHO) "COQ_MAKEFILE" + $(Q)$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq clean: Makefile.coq $(MAKE) -f Makefile.coq clean @@ -1,8 +1,12 @@ -Synthesizing Correct-by-Construction Assembly for Cryptographic Primitives +Fiat-Crypto: Synthesizing Correct-by-Construction Assembly for Cryptographic Primitives ----- ... which would make a good paper title. +NOTE: The gibhub.com repo is only intermittently synced with +github.mit.edu. If you're in CSAIL, you should pull from the +github.mit.edu repo. + To build: export COQPATH="$(pwd)/coqprime${COQPATH:+:}$COQPATH" |