diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-02-18 12:08:07 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-02-18 12:08:07 +0000 |
| commit | 2a4153de356f8d29359c5950d1d9cbc498d7c2f3 (patch) | |
| tree | fe3ed481130b63d6833a14f75571a2f4e75cd3c4 /Makefile | |
| parent | 31176813d3f18db6c7f76257be416b7b8b60b92d (diff) | |
| download | vericert-2a4153de356f8d29359c5950d1d9cbc498d7c2f3.tar.gz vericert-2a4153de356f8d29359c5950d1d9cbc498d7c2f3.zip | |
Create translation
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -1,28 +1,28 @@ COMPCERTRECDIRS := lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ MenhirLib cparser -COMPCERTCOQINCLUDES := $(foreach d, $(RECDIRS), -R lib/CompCert/$(d) compcert.$(d)) +COMPCERTCOQINCLUDES := $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) COQINCLUDES := -R src/Common CoqUp.Common -R src/Verilog CoqUp.Verilog -R src/Driver CoqUp.Driver -R src/Extraction CoqUp.Extraction $(COMPCERTCOQINCLUDES) COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source COQMAKE := "$(COQBIN)coq_makefile" -COQUPDIRS := Common Driver Verilog +COQUPDIRS := SMTrans Common Driver Verilog VS := $(foreach d, $(COQUPDIRS), src/$(d)/*.v) -.PHONY: all install coq clean +.PHONY: all install proof clean all: (cd lib/CompCert && ./configure x86_64-linux) $(MAKE) -C lib/CompCert all - $(MAKE) coq + $(MAKE) proof $(MAKE) compile install: $(MAKE) -f Makefile.coq install -coq: Makefile.coq +proof: Makefile.coq $(MAKE) -f Makefile.coq extraction: src/Extraction/STAMP @@ -40,7 +40,7 @@ src/Extraction/STAMP: Makefile.coq: @echo "COQMAKE Makefile.coq" - @$(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq + $(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq clean:: Makefile.coq $(MAKE) -f Makefile.coq clean |