Remove CompCert from gitmodules

5 files changed, 58 insertions, 34 deletions

diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index f30817e..0000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "lib/CompCert"]
-	path = lib/CompCert
-	url = https://github.com/ymherklotz/CompCert.git
diff --git a/Makefile b/Makefile
index 218598a..5dc8707 100644
--- a/Makefile
+++ b/Makefile
@@ -6,15 +6,10 @@ ifeq ($(UNAME_S),Darwin)
 	ARCH := verilog-macosx
 endif
 
-COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser
-
 COQINCLUDES := -R src/common vericert.common \
                -R src/extraction vericert.extraction \
                -R src/hls vericert.hls \
-               -R src vericert \
-               $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) \
-               -R lib/CompCert/flocq Flocq \
-               -R lib/CompCert/MenhirLib MenhirLib
+               -R src vericert
 
 COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
 COQMAKE := $(COQBIN)coq_makefile
@@ -27,17 +22,10 @@ PREFIX ?= .
 
 .PHONY: all install proof clean extraction test
 
-all: lib/COMPCERTSTAMP
+all:
 	$(MAKE) proof
 	$(MAKE) compile
 
-lib/CompCert/Makefile.config: lib/CompCert/configure
-	(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
-
-lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
-	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
-	touch $@
-
 install:
 	install -d $(PREFIX)/bin
 	sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
diff --git a/_CoqProject b/_CoqProject
index 69d12c1..43b3ecc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,13 +3,4 @@
 -R src/hls vericert.hls
 -R src vericert
 
--R lib/CompCert/backend compcert.backend
--R lib/CompCert/cfrontend compcert.cfrontend
--R lib/CompCert/common compcert.common
--R lib/CompCert/cparser compcert.cparser
--R lib/CompCert/driver compcert.driver
--R lib/CompCert/exportclight compcert.exportclight
--R lib/CompCert/lib compcert.lib
--R lib/CompCert/verilog compcert.verilog
--R lib/CompCert/flocq Flocq
--R lib/CompCert/MenhirLib MenhirLib
+-R /nix/store/66l13gkqf431c0lm3x1lcn7zvfqxz6sq-coq8.14-compcert-dev-lib/lib/coq/8.14/user-contrib/compcert/flocq Flocq
diff --git a/default.nix b/default.nix
index e3ce09b..841a140 100644
--- a/default.nix
+++ b/default.nix
@@ -2,16 +2,64 @@ with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/00197eff36bb
 let
   ncoq = coq_8_14;
   ncoqPackages = coqPackages_8_14;
+  ncompcert = ncoqPackages.callPackage
+    ( { coq, flocq, ocamlPackages, gcc, stdenv, fetchFromGithub, mkCoqDerivation }:
+      mkCoqDerivation {
+        pname = "compcert";
+        owner = "ymherklotz";
+        releaseRev = v: "v${v}";
+
+        defaultVersion = "3.10";
+
+        src = fetchFromGitHub {
+          owner = "ymherklotz";
+          repo = "CompCert";
+          rev = "4f467596f8674f5f4fbf84a793cb8fcfc35a44a2";
+          sha256 = "0m435pscfdb4irjxhzazzpl8jv63piwl4rb3nnpdirs9dg7msl2j";
+        };
+
+        buildInputs = with ocamlPackages; [ ocaml findlib menhir menhirLib gcc ] ++ [ coq ];
+        propagatedBuildInputs = [ flocq ];
+
+        enableParallelBuilding = true;
+
+        outputs = [ "out" "lib" ];
+
+        configurePhase = ''
+          ./configure \
+          -prefix $out \
+          -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \
+          -no-runtime-lib \
+          -no-standard-headers \
+          -install-coqdev \
+          -use-external-Flocq \
+          ${if stdenv.isDarwin then "verilog-macosx" else "verilog-linux"}
+        '';
+
+        meta = with lib; {
+          description = "Formally verified C compiler";
+          homepage    = "https://compcert.org";
+          license     = licenses.inria-compcert;
+          platforms   = [ "x86_64-linux" "x86_64-darwin" ];
+          maintainers = [ ];
+        };
+      } ) { } ;
 in
-stdenv.mkDerivation {
-  name = "vericert";
+ncoqPackages.mkCoqDerivation {
+  pname = "vericert";
   src = ./.;
 
-  buildInputs = [ ncoq dune_2 gcc
-                  ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir
-                  ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin
-                  ncoq.ocamlPackages.menhirLib
-                ];
+  owner = "ymherklotz";
+  releaseRev = v: "v${v}";
+
+  defaultVersion = "3.10";
+
+  buildInputs = with ncoq.ocamlPackages; [ ncoq dune_2 gcc
+                                           ncoq.ocaml findlib menhir
+                                           ocamlgraph merlin
+                                           menhirLib
+                                           ncompcert
+                                         ];
 
   enableParallelBuilding = true;
 }
diff --git a/lib/CompCert b/lib/CompCert
deleted file mode 160000
-Subproject 4f467596f8674f5f4fbf84a793cb8fcfc35a44a