diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-02-04 19:50:29 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-02-04 19:50:29 +0000 |
| commit | a2aafb7de592a60a86add13e184396e07b75ab07 (patch) | |
| tree | 58c30cb6aeb12ae90933a488b39f3e67fc9fca84 /Makefile | |
| parent | a2c2bb945cf4e848225692f23aa337feae9747d2 (diff) | |
| download | vericert-a2aafb7de592a60a86add13e184396e07b75ab07.tar.gz vericert-a2aafb7de592a60a86add13e184396e07b75ab07.zip | |
Add Extraction
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 26 |
1 files changed, 16 insertions, 10 deletions
@@ -1,16 +1,15 @@ -IGNORE:= +COQINCLUDES=-R src/CoqUp CoqUp -LIBVS:=$(wildcard src/CoqUp/Lib/*.v) -LIBVS:=$(filter-out $(IGNORE:%=%.v),$(LIBVS)) +COQEXEC=$(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source +COQMAKE="$(COQBIN)coq_makefile" -VS:=$(wildcard src/CoqUp/*.v) -VS:=$(filter-out $(LIBVS) $(IGNORE:%=%.v),$(VS)) +VS=$(wildcard src/CoqUp/*.v) .PHONY: all install coq clean -ARGS := -R src/CoqUp CoqUp - -all: coq +all: + $(MAKE) coq + $(MAKE) extraction install: $(MAKE) -f Makefile.coq install @@ -18,8 +17,15 @@ install: coq: Makefile.coq $(MAKE) -f Makefile.coq -Makefile.coq: Makefile $(LIBVS) $(VS) - $(COQBIN)coq_makefile $(ARGS) $(LIBVS) $(VS) -o Makefile.coq +extraction: extraction/STAMP + +extraction/STAMP: + rm -f extraction/*.ml extraction/*.mli + $(COQEXEC) ./extraction/Extraction.v + touch $@ + +Makefile.coq: Makefile + $(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq clean:: Makefile.coq $(MAKE) -f Makefile.coq clean |