diff options
| -rw-r--r-- | Makefile | 19 | ||||
| -rw-r--r-- | _CoqProject | 12 | ||||
| -rw-r--r-- | src/Assembly/Pipeline.v | 2 |
3 files changed, 21 insertions, 12 deletions
@@ -1,27 +1,26 @@ + MOD_NAME := Crypto SRC_DIR := src .PHONY: coq clean install coqprime update-_CoqProject .DEFAULT_GOAL := coq -SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' - update-_CoqProject:: - (echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files 'src/*.v' | $(SORT_COQPROJECT))) > _CoqProject + @(echo "-R $(SRC_DIR) $(MOD_NAME)"; git ls-files src/*.v) > _CoqProject coq: coqprime Makefile.coq - $(MAKE) -f Makefile.coq + @$(MAKE) -f Makefile.coq coqprime: - $(MAKE) -C coqprime + @$(MAKE) -C coqprime Makefile.coq: Makefile _CoqProject - coq_makefile -f _CoqProject -o Makefile.coq + @coq_makefile -f _CoqProject -o Makefile.coq 2> /dev/null clean: Makefile.coq - $(MAKE) -f Makefile.coq clean - rm -f Makefile.coq + @$(MAKE) -f Makefile.coq clean + @rm -f Makefile.coq install: coq Makefile.coq - $(MAKE) -f Makefile.coq install - $(MAKE) -C coqprime install + @$(MAKE) -f Makefile.coq install + @$(MAKE) -C coqprime install diff --git a/_CoqProject b/_CoqProject index 416b29176..c92f9481c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,5 @@ -R src Crypto +-R Coqprime/Coqprime Coqprime src/BaseSystem.v src/BaseSystemProofs.v src/EdDSAProofs.v @@ -45,3 +46,14 @@ src/Util/NumTheoryUtil.v src/Util/Tactics.v src/Util/WordUtil.v src/Util/ZUtil.v +src/Assembly/QhasmCommon.v +src/Assembly/QhasmUtil.v +src/Assembly/State.v +src/Assembly/QhasmEvalCommon.v +src/Assembly/Pseudo.v +src/Assembly/AlmostQhasm.v +src/Assembly/Qhasm.v +src/Assembly/PseudoConversion.v +src/Assembly/AlmostConversion.v +src/Assembly/StringConversion.v +src/Assembly/Pipeline.v diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index 1283c5673..58215cdf2 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -25,6 +25,4 @@ Module PipelineExample. Program Definition asdf: Program Unary32 := ($0 :+: $0)%p. Definition exStr := Pipeline.toString asdf. - - Eval vm_compute in exStr. End PipelineExample. |