Add initial development files

9 files changed, 75 insertions, 0 deletions

diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..dd1db2f
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,23 @@
+VS:=$(shell find . -type f -name '*.v')
+
+.PHONY: coq clean force
+
+coq: Makefile.coq.all $(VS)
+	$(MAKE) -f Makefile.coq.all
+
+Makefile.coq.all: force
+	@echo "GEN $@"
+	@$(COQBIN)coq_makefile -f _CoqProject $(VS) -o Makefile.coq.all
+
+force:
+
+clean:: Makefile.coq.all
+	$(MAKE) -f Makefile.coq.all clean
+	rm -rf *.v.d *.glob *.vo *~ *.hi *.o
+	rm -f Makefile.coq.all Makefile.coq.all.conf
+
+install: Makefile.coq.all
+	$(MAKE) -f Makefile.coq.all install
+
+uninstall: Makefile.coq.all
+	$(MAKE) -f Makefile.coq.all uninstall
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000..0f7247f
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1 @@
+-Q src biteq
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..208db0a
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,45 @@
+with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/00197eff36bb8f7dd7f53a59f730e1fd8e11b1f4.tar.gz") {};
+let
+  ncoq = coq_8_14;
+  ncoqPackages = coqPackages_8_14;
+  bbv = ncoqPackages.callPackage
+    ( { coq, stdenv, fetchFromGithub, mkCoqDerivation }:
+      mkCoqDerivation {
+        pname = "bbv";
+        owner = "ymherklotz";
+
+        defaultVersion = "1.0-dev";
+
+        src = fetchFromGitHub {
+          owner = "mit-plv";
+          repo = "bbv";
+          rev = "d5ab9c04db85eb85688816dc687d118000a65736";
+          sha256 = "0qlgkzwrg80j50md9s3fbnq62xc7fx1cb9f3y8iz714824ihkhbj";
+        };
+
+        buildInputs = [ ];
+        propagatedBuildInputs = [ coq ];
+        enableParallelBuilding = true;
+
+        outputs = [ "out" ];
+
+        meta = with lib; {
+          description = "Bedrock Bit Vector Library";
+          homepage    = "https://github.com/mit-plv/bbv";
+          license     = licenses.mit;
+          platforms   = [ "x86_64-linux" "x86_64-darwin" ];
+          maintainers = [ ];
+        };
+      } ) { } ;
+in
+ncoqPackages.mkCoqDerivation {
+  pname = "biteq";
+  owner = "ymherklotz";
+  defaultVersion = "0.1.0";
+
+  src = ./.;
+
+  buildInputs = [ ncoq bbv ];
+
+  enableParallelBuilding = true;
+}
diff --git a/src/.BitEQ.aux b/src/.BitEQ.aux
new file mode 100644
index 0000000..b85cf5b
--- /dev/null
+++ b/src/.BitEQ.aux
@@ -0,0 +1,2 @@
+COQAUX1 0c779ed0297eab017740eaf15e9ad89b /home/ymherklotz/projects/biteq/src/BitEQ.v
+0 0 vo_compile_time "0.140"
diff --git a/src/BitEQ.glob b/src/BitEQ.glob
new file mode 100644
index 0000000..5adc945
--- /dev/null
+++ b/src/BitEQ.glob
@@ -0,0 +1,3 @@
+DIGEST 0c779ed0297eab017740eaf15e9ad89b
+Fbiteq.BitEQ
+R15:22 bbv.Word <> <> lib
diff --git a/src/BitEQ.v b/src/BitEQ.v
new file mode 100644
index 0000000..f648f40
--- /dev/null
+++ b/src/BitEQ.v
@@ -0,0 +1 @@
+Require Import bbv.Word.
diff --git a/src/BitEQ.vo b/src/BitEQ.vo
new file mode 100644
index 0000000..73a61d6
--- /dev/null
+++ b/src/BitEQ.vo
diff --git a/src/BitEQ.vok b/src/BitEQ.vok
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/BitEQ.vok
diff --git a/src/BitEQ.vos b/src/BitEQ.vos
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/src/BitEQ.vos