From a2aafb7de592a60a86add13e184396e07b75ab07 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 4 Feb 2020 19:50:29 +0000
Subject: Add Extraction

---
 Makefile                | 26 ++++++++++++++++----------
 default.nix             |  2 +-
 extraction/Extraction.v |  4 ++--
 3 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/Makefile b/Makefile
index 46d2573..1302e6e 100644
--- a/Makefile
+++ b/Makefile
@@ -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.
-- 
cgit