nix: various improvements

.nix/bootstrap.nix

@@ -1,5 +1,10 @@
-{ fstar, fstar-dune, fstar-ocaml-snapshot, fstar-ulib, stdenv }:
-
+{
+  fstar,
+  fstar-dune,
+  fstar-ocaml-snapshot,
+  fstar-ulib,
+  stdenv,
+}:
 let
   ocaml-src = stdenv.mkDerivation {
     name = "src";
@@ -15,11 +20,18 @@ let
     pname = "fstar-bootstrap-dune";
     src = ocaml-src;
   });
-  fstar-ulib-bootstrap = (fstar-ulib.override
-    (_: { fstar-dune = fstar-dune-bootstrap; })).overrideAttrs
-    (_: { pname = "fstar-bootstrap-ulib"; });
-
-in (fstar.override (_: {
+  fstar-ulib-bootstrap =
+    (fstar-ulib.override (_: {
+      fstar-dune = fstar-dune-bootstrap;
+    })).overrideAttrs
+      (_: {
+        pname = "fstar-bootstrap-ulib";
+      });
+in
+(fstar.override (_: {
   fstar-dune = fstar-dune-bootstrap;
   fstar-ulib = fstar-ulib-bootstrap;
-})).overrideAttrs (_: { pname = "fstar-bootstrap"; })
+})).overrideAttrs
+  (_: {
+    pname = "fstar-bootstrap";
+  })

.nix/dune.nix

@@ -0,0 +1,57 @@
+{
+  batteries,
+  buildDunePackage,
+  lib,
+  memtrace,
+  menhir,
+  menhirLib,
+  ocaml,
+  pprint,
+  ppx_deriving,
+  ppx_deriving_yojson,
+  ppxlib,
+  process,
+  sedlex,
+  stdint,
+  version,
+  yojson,
+  zarith,
+}:
+buildDunePackage {
+  pname = "fstar";
+  inherit version;
+
+  duneVersion = "3";
+
+  src = lib.sourceByRegex ./.. [
+    "ocaml.*"
+    "version.txt"
+  ];
+
+  prePatch = ''
+    patchShebangs ocaml/fstar-lib/make_fstar_version.sh
+    cd ocaml
+  '';
+
+  FSTAR_COMMIT = version;
+
+  nativeBuildInputs = [ menhir ];
+
+  buildInputs = [ memtrace ];
+
+  propagatedBuildInputs = [
+    batteries
+    menhirLib
+    pprint
+    ppx_deriving
+    ppx_deriving_yojson
+    ppxlib
+    process
+    sedlex
+    stdint
+    yojson
+    zarith
+  ];
+
+  enableParallelBuilding = true;
+}

.nix/fstar.nix

@@ -1,11 +1,24 @@
-{ callPackage, fstar-dune, fstar-ulib, installShellFiles, lib, makeWrapper
-, stdenv, version, z3 }:
-
+{
+  fstar-dune,
+  fstar-ulib,
+  installShellFiles,
+  lib,
+  makeWrapper,
+  ocamlPackages,
+  stdenv,
+  removeReferencesTo,
+  version,
+  z3,
+}:
 stdenv.mkDerivation {
   pname = "fstar";
   inherit version;
 
-  buildInputs = [ installShellFiles makeWrapper ];
+  buildInputs = [
+    installShellFiles
+    makeWrapper
+    removeReferencesTo
+  ];
 
   src = lib.sourceByRegex ./.. [
     ".common.mk"
@@ -15,6 +28,8 @@ stdenv.mkDerivation {
     "ucontrib.*"
   ];
 
+  inherit (fstar-dune) propagatedBuildInputs;
+
   dontBuild = true;
 
   installPhase = ''
@@ -26,17 +41,15 @@ stdenv.mkDerivation {
 
     PREFIX=$out make -C src/ocaml-output install-sides
 
-    for binary in $out/bin/*
-    do
-      chmod +x $binary
-      wrapProgram $binary --prefix PATH ":" ${z3}/bin
-    done
+    chmod +x $out/bin/fstar.exe
+    wrapProgram $out/bin/fstar.exe --prefix PATH ":" ${z3}/bin
+    remove-references-to -t '${ocamlPackages.ocaml}' $out/bin/fstar.exe
+
+    substituteInPlace $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstar/dune-package \
+      --replace ${fstar-dune} $out
 
-    cd $out
     installShellCompletion --bash ${../.completion/bash/fstar.exe.bash}
     installShellCompletion --fish ${../.completion/fish/fstar.exe.fish}
-    installShellCompletion --zsh --name _fstar.exe ${
-      ../.completion/zsh/__fstar.exe
-    }
+    installShellCompletion --zsh --name _fstar.exe ${../.completion/zsh/__fstar.exe}
   '';
 }

.nix/ocaml-snapshot.nix

@@ -0,0 +1,45 @@
+{
+  fstar,
+  lib,
+  ocamlPackages,
+  stdenv,
+  version,
+}:
+stdenv.mkDerivation {
+  pname = "fstar-ocaml-snapshot";
+  inherit version;
+
+  src = lib.cleanSourceWith {
+    src = ./..;
+    filter =
+      path: _:
+      let
+        relPath = lib.removePrefix (toString ./.. + "/") (toString path);
+      in
+      lib.any (lib.flip lib.hasPrefix relPath) [
+        "src"
+        "ulib"
+      ]
+      || (
+        lib.hasPrefix "ocaml" relPath
+        && !(lib.hasInfix "/generated/" relPath)
+        && !(lib.hasInfix "/dynamic/" relPath)
+      )
+      || lib.hasSuffix ".common.mk" relPath;
+  };
+
+  postPatch = ''
+    mkdir -p bin
+    cp ${fstar}/bin/fstar.exe bin
+    cd src/ocaml-output
+  '';
+
+  nativeBuildInputs = with ocamlPackages; [
+    ocaml
+    menhir
+  ];
+
+  installPhase = "mv ../../ocaml $out";
+
+  enableParallelBuilding = true;
+}

ulib/default.nix → .nix/ulib.nix

@@ -1,20 +1,29 @@
-{ fstar-dune, lib, stdenv, version, z3 }:
-
+{
+  fstar-dune,
+  lib,
+  stdenv,
+  version,
+  z3,
+}:
 stdenv.mkDerivation {
   pname = "fstar-ulib";
   inherit version;
 
-  src = lib.sourceByRegex ./.. [ "ulib.*" ".common.mk" ];
+  src = lib.sourceByRegex ./.. [
+    "ulib.*"
+    ".common.mk"
+  ];
+
+  nativeBuildInputs = [ z3 ];
 
   postPatch = ''
     mkdir -p bin
     cp ${fstar-dune}/bin/fstar.exe bin
-    export PATH="$(pwd)/bin:${z3}/bin:$PATH"
     patchShebangs ulib/install-ulib.sh
     cd ulib
   '';
 
-  enableParallelBuilding = true;
+  makeFlags = [ "PREFIX=$(out)" ];
 
-  preInstall = "export PREFIX=$out";
+  enableParallelBuilding = true;
 }