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 | |
parent | a2c2bb945cf4e848225692f23aa337feae9747d2 (diff) | |
download | vericert-a2aafb7de592a60a86add13e184396e07b75ab07.tar.gz vericert-a2aafb7de592a60a86add13e184396e07b75ab07.zip |
Add Extraction
-rw-r--r-- | Makefile | 26 | ||||
-rw-r--r-- | default.nix | 2 | ||||
-rw-r--r-- | extraction/Extraction.v | 4 |
3 files changed, 19 insertions, 13 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 diff --git a/default.nix b/default.nix index 4e1cfbb..1a1d32b 100644 --- a/default.nix +++ b/default.nix @@ -4,7 +4,7 @@ stdenv.mkDerivation { name = "CoqUp"; src = ./.; - buildInputs = [ coq_8_10 ]; + buildInputs = [ coq_8_10 ocamlPackages.menhir dune ]; buildPhase = "make"; } diff --git a/extraction/Extraction.v b/extraction/Extraction.v index 40bbe54..4c5f034 100644 --- a/extraction/Extraction.v +++ b/extraction/Extraction.v @@ -1,4 +1,4 @@ -Require Import Verilog. +From CoqUp Require Import Verilog. -Cd "src". +Cd "extraction". Separate Extraction Verilog.nat_to_value Verilog.value_to_nat. |