diff options
| -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. |