flake: bump fstar and pulse revision

Author: jhvst

flake.lock

@@ -3,7 +3,7 @@
     devenv.inputs.nixpkgs.follows = "nixpkgs";
     devenv.url = "github:cachix/devenv";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    fstar.url = "github:FStarLang/FStar/a94456863e3f971a7c63a64aca1a07d2cd9eb9a1";
+    fstar.url = "github:FStarLang/FStar/v2025.02.17";
     nixpkgs.url = "github:cachix/devenv-nixpkgs/rolling";
     treefmt-nix.inputs.nixpkgs.follows = "nixpkgs";
     treefmt-nix.url = "github:numtide/treefmt-nix";
@@ -36,40 +36,21 @@
           };
         };
 
-        packages.pulse-dune = pkgs.ocaml-ng.ocamlPackages_4_14.buildDunePackage rec {
-
-          pname = "pulse";
-          version = "2024.06.02";
-          sourceRoot = "${src.name}/src/ocaml";
-
-          src = pkgs.fetchFromGitHub {
-            owner = "FStarLang";
-            repo = pname;
-            rev = "v${version}";
-            hash = "sha256-jRm21FtPorAW/eQlXbqPyo2Ev0Kdv0evvGmSoPpNE7A=";
-          };
-
-          inherit (inputs.fstar.packages.${system}.fstar-dune) nativeBuildInputs;
-
-          buildInputs = inputs.fstar.packages.${system}.fstar-dune.buildInputs ++ [ inputs.fstar.packages.${system}.fstar-dune ];
-
-        };
-
         packages.pulse = pkgs.stdenv.mkDerivation rec {
 
           pname = "pulse";
-          version = "2024.06.02";
+          version = "84b3fc39e2ba16059408d4df039d4a03efa85b16";
 
           src = pkgs.fetchFromGitHub {
             owner = "FStarLang";
             repo = pname;
-            rev = "v${version}";
-            hash = "sha256-jRm21FtPorAW/eQlXbqPyo2Ev0Kdv0evvGmSoPpNE7A=";
+            rev = "${version}";
+            hash = "sha256-Cg6z4pbSbPIaU1Jfcw78XVTxqLq5Jt+CajoyxHaeCVo=";
           };
 
-          inherit (inputs.fstar.packages.${system}.fstar-dune) nativeBuildInputs;
+          inherit (inputs.fstar.packages.${system}.fstar) nativeBuildInputs;
 
-          buildInputs = inputs.fstar.packages.${system}.fstar-dune.buildInputs ++ [
+          buildInputs = inputs.fstar.packages.${system}.fstar.buildInputs ++ [
             inputs.fstar.packages.${system}.fstar
             pkgs.which
           ];
@@ -86,12 +67,11 @@
         packages.pulse-exe = pkgs.writeShellScriptBin "pulse.exe" ''
           exec ${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe "$1" \
             --include ${config.packages.pulse}/lib/pulse \
-            --include ${config.packages.pulse}/lib/pulse/c \
-            --include ${config.packages.pulse}/lib/pulse/core \
+            --include ${config.packages.pulse}/lib/pulse/checker \
+            --include ${config.packages.pulse}/lib/pulse/extraction \
             --include ${config.packages.pulse}/lib/pulse/lib \
-            --include ${config.packages.pulse}/lib/pulse/lib/class \
-            --include ${config.packages.pulse}/lib/pulse/lib/ml \
-            --include ${config.packages.pulse}/lib/pulse/lib/pledge \
+            --include ${config.packages.pulse}/lib/pulse/ml \
+            --include ${config.packages.pulse}/lib/pulse/syntax_extension \
             --load_cmxs pulse \
             "$@"
         '';
@@ -102,12 +82,12 @@
             modules = [
               {
                 # https://devenv.sh/reference/options/
-                packages = with inputs.fstar.packages.${system}; [ z3 ]
-                  ++ fstar-dune.buildInputs
-                  ++ fstar-dune.nativeBuildInputs;
+                packages = with inputs.fstar.packages.${system}; [ z3 ];
 
+                env.FSTAR_EXE = "${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe";
+                env.FSTAR_HOME = "${inputs.fstar.packages.${system}.fstar}/lib/fstar";
+                env.PULSE_HOME = "${config.packages.pulse}/lib/pulse";
                 env.OCAMLPATH = "${inputs.fstar.packages.${system}.fstar}/lib/ocaml/4.14.1/site-lib";
-                env.PULSE_HOME = ".";
                 enterShell = ''
                   export PATH="${inputs.fstar.packages.${system}.fstar}/bin:$PATH"
                 '';
@@ -138,7 +118,7 @@
           devenv-up = self.devShells.${system}.default.config.procfileScript;
           devenv-test = self.devShells.${system}.default.config.test;
 
-          inherit (inputs.fstar.packages.${system}) fstar fstar-dune;
+          inherit (inputs.fstar.packages.${system}) fstar;
         };
 
       };