fstar: build with dune (#275924)

3 files changed, 120 insertions, 45 deletions

diff --git a/pkgs/development/compilers/fstar/default.nix b/pkgs/development/compilers/fstar/default.nix
index 8bb3366655c77..773a0dde281f4 100644
--- a/pkgs/development/compilers/fstar/default.nix
+++ b/pkgs/development/compilers/fstar/default.nix
@@ -1,7 +1,17 @@
-{ lib, stdenv, writeScript, fetchFromGitHub, z3, ocamlPackages, makeWrapper, installShellFiles, removeReferencesTo }:
+{ callPackage
+, fetchFromGitHub
+, installShellFiles
+, lib
+, makeWrapper
+, ocamlPackages
+, removeReferencesTo
+, stdenv
+, writeScript
+, z3
+}:
+
+let
 
-stdenv.mkDerivation rec {
-  pname = "fstar";
   version = "2023.09.03";
 
   src = fetchFromGitHub {
@@ -11,66 +21,54 @@ stdenv.mkDerivation rec {
     hash = "sha256-ymoP5DvaLdrdwJcnhZnLEvwNxUFzhkICajPyK4lvacc=";
   };
 
-  strictDeps = true;
+  fstar-dune = ocamlPackages.callPackage ./dune.nix { inherit version src; };
+
+  fstar-ulib = callPackage ./ulib.nix { inherit version src fstar-dune z3; };
+
+in
+
+stdenv.mkDerivation {
+  pname = "fstar";
+  inherit version src;
 
   nativeBuildInputs = [
-    z3
-    makeWrapper
     installShellFiles
+    makeWrapper
     removeReferencesTo
-  ] ++ (with ocamlPackages; [
-    ocaml
-    dune_3
-    findlib
-    ocamlbuild
-    menhir
-  ]);
-
-  buildInputs = with ocamlPackages; [
-    batteries
-    zarith
-    stdint
-    yojson
-    fileutils
-    memtrace
-    menhirLib
-    pprint
-    sedlex
-    ppxlib
-    ppx_deriving
-    ppx_deriving_yojson
-    process
   ];
 
-  makeFlags = [ "PREFIX=$(out)" ];
+  inherit (fstar-dune) propagatedBuildInputs;
 
-  enableParallelBuilding = true;
+  dontBuild = true;
 
-  postPatch = ''
-    patchShebangs ulib/install-ulib.sh
-  '';
+  installPhase = ''
+    mkdir $out
 
-  preInstall = ''
-    mkdir -p $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstarlib
-  '';
-  postInstall = ''
-    # Remove build artifacts
-    find $out -name _build -type d | xargs -I{} rm -rf "{}"
+    CP="cp -r --no-preserve=mode"
+    $CP ${fstar-dune}/* $out
+    $CP ${fstar-ulib}/* $out
+
+    PREFIX=$out make -C src/ocaml-output install-sides
+
+    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
 
-    wrapProgram $out/bin/fstar.exe --prefix PATH ":" "${z3}/bin"
+    substituteInPlace $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstar/dune-package \
+      --replace ${fstar-dune} $out
+
     installShellCompletion --bash .completion/bash/fstar.exe.bash
     installShellCompletion --fish .completion/fish/fstar.exe.fish
     installShellCompletion --zsh --name _fstar.exe .completion/zsh/__fstar.exe
   '';
 
   passthru.updateScript = writeScript "update-fstar" ''
-      #!/usr/bin/env nix-shell
-      #!nix-shell -i bash -p git gnugrep common-updater-scripts
-      set -eu -o pipefail
+    #!/usr/bin/env nix-shell
+    #!nix-shell -i bash -p git gnugrep common-updater-scripts
+    set -eu -o pipefail
 
-      version="$(git ls-remote --tags git@github.com:FStarLang/FStar.git | grep -Po 'v\K\d{4}\.\d{2}\.\d{2}' | sort | tail -n1)"
-      update-source-version fstar "$version"
+    version="$(git ls-remote --tags git@github.com:FStarLang/FStar.git | grep -Po 'v\K\d{4}\.\d{2}\.\d{2}' | sort | tail -n1)"
+    update-source-version fstar "$version"
   '';
 
   meta = with lib; {
diff --git a/pkgs/development/compilers/fstar/dune.nix b/pkgs/development/compilers/fstar/dune.nix
new file mode 100644
index 0000000000000..1ca476838c8bb
--- /dev/null
+++ b/pkgs/development/compilers/fstar/dune.nix
@@ -0,0 +1,51 @@
+{ batteries
+, buildDunePackage
+, memtrace
+, menhir
+, menhirLib
+, pprint
+, ppx_deriving
+, ppx_deriving_yojson
+, ppxlib
+, process
+, sedlex
+, src
+, stdint
+, version
+, yojson
+, zarith
+}:
+
+buildDunePackage {
+  pname = "fstar";
+  inherit version src;
+
+  postPatch = ''
+    patchShebangs ocaml/fstar-lib/make_fstar_version.sh
+    cd ocaml
+  '';
+
+  nativeBuildInputs = [
+    menhir
+  ];
+
+  buildInputs = [
+    memtrace
+  ];
+
+  propagatedBuildInputs = [
+    batteries
+    menhirLib
+    pprint
+    ppx_deriving
+    ppx_deriving_yojson
+    ppxlib
+    process
+    sedlex
+    stdint
+    yojson
+    zarith
+  ];
+
+  enableParallelBuilding = true;
+}
diff --git a/pkgs/development/compilers/fstar/ulib.nix b/pkgs/development/compilers/fstar/ulib.nix
new file mode 100644
index 0000000000000..4390a7bdb55e3
--- /dev/null
+++ b/pkgs/development/compilers/fstar/ulib.nix
@@ -0,0 +1,26 @@
+{ fstar-dune
+, src
+, stdenv
+, version
+, z3
+}:
+
+stdenv.mkDerivation {
+  pname = "fstar-ulib";
+  inherit version src;
+
+  nativeBuildInputs = [
+    z3
+  ];
+
+  postPatch = ''
+    mkdir -p bin
+    cp ${fstar-dune}/bin/fstar.exe bin
+    patchShebangs ulib/install-ulib.sh
+    cd ulib
+  '';
+
+  makeFlags = [ "PREFIX=$(out)" ];
+
+  enableParallelBuilding = true;
+}