Unverified Commit b5d9b75f authored by Tristan Ross's avatar Tristan Ross Committed by GitHub
Browse files

fstar: 2024.09.05 -> 2025.03.25 (#374917)

parents a2bbba3c 4fe4ed76
Loading
Loading
Loading
Loading
+121 −0
Original line number Diff line number Diff line
@@ -4,87 +4,117 @@
  installShellFiles,
  lib,
  makeWrapper,
  ocamlPackages,
  nix-update-script,
  ocaml-ng,
  removeReferencesTo,
  stdenv,
  writeScript,
  z3,
  util-linux,
  which,
}:

let
  # The version of ocaml fstar uses.
  ocamlPackages = ocaml-ng.ocamlPackages_4_14;

  version = "2024.09.05";
  fstarZ3 = callPackage ./z3 { };
in
ocamlPackages.buildDunePackage rec {
  pname = "fstar";
  version = "2025.03.25";

  src = fetchFromGitHub {
    owner = "FStarLang";
    repo = "FStar";
    rev = "v${version}";
    hash = "sha256-yaA6WpP2XIQhjK7kpXBdBFUgKZyvtThd6JmSchUCfbI=";
  };

  fstar-dune = ocamlPackages.callPackage ./dune.nix { inherit version src; };

  fstar-ulib = callPackage ./ulib.nix {
    inherit
      version
      src
      fstar-dune
      z3
      ;
    hash = "sha256-PhjfThXF6fJlFHtNEURG4igCnM6VegWODypmRvnZPdA=";
  };

in

stdenv.mkDerivation {
  pname = "fstar";
  inherit version src;
  duneVersion = "3";

  nativeBuildInputs = [
    ocamlPackages.menhir
    which
    util-linux
    installShellFiles
    makeWrapper
    removeReferencesTo
  ];

  inherit (fstar-dune) propagatedBuildInputs;
  prePatch = ''
    patchShebangs .scripts/*.sh
    patchShebangs ulib/ml/app/ints/mk_int_file.sh
  '';

  dontBuild = true;
  buildInputs = with ocamlPackages; [
    batteries
    menhir
    menhirLib
    pprint
    ppx_deriving
    ppx_deriving_yojson
    ppxlib
    process
    sedlex
    stdint
    yojson
    zarith
    memtrace
    mtime
  ];

  installPhase = ''
    mkdir $out
  preConfigure = ''
    mkdir -p cache
    export DUNE_CACHE_ROOT="$(pwd)/cache"
    export PATH="${lib.makeBinPath [ fstarZ3 ]}''${PATH:+:}$PATH"
    export PREFIX="$out"
  '';

    CP="cp -r --no-preserve=mode"
    $CP ${fstar-dune}/* $out
    $CP ${fstar-ulib}/* $out
  buildPhase = ''
    runHook preBuild
    make -j$NIX_BUILD_CORES
    runHook postBuild
  '';

    PREFIX=$out make -C src/ocaml-output install-sides
  installPhase = ''
    runHook preInstall

    make install

    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
    for binary in $out/bin/*; do
      wrapProgram "$binary" --prefix PATH : "${lib.makeBinPath [ fstarZ3 ]}"
    done

    src="$(pwd)"
    cd $out
    installShellCompletion --bash $src/.completion/bash/fstar.exe.bash
    installShellCompletion --fish $src/.completion/fish/fstar.exe.fish
    installShellCompletion --zsh --name _fstar.exe $src/.completion/zsh/__fstar.exe
    cd $src

    installShellCompletion --bash .completion/bash/fstar.exe.bash
    installShellCompletion --fish .completion/fish/fstar.exe.fish
    installShellCompletion --zsh --name _fstar.exe .completion/zsh/__fstar.exe
    runHook postInstall
  '';

  passthru.updateScript = writeScript "update-fstar" ''
    #!/usr/bin/env nix-shell
    #!nix-shell -i bash -p git gnugrep common-updater-scripts
    set -eu -o pipefail
  enableParallelBuilding = true;

    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"
  '';
  passthru = {
    updateScript = nix-update-script {
      extraArgs = [
        "--version-regex"
        "v(\d{4}\.\d{2}\.\d{2})$"
      ];
    };
    z3 = fstarZ3;
  };

  meta = with lib; {
    description = "ML-like functional programming language aimed at program verification";
    homepage = "https://www.fstar-lang.org";
    changelog = "https://github.com/FStarLang/FStar/raw/v${version}/CHANGES.md";
    license = licenses.asl20;
    maintainers = with maintainers; [ ];
    maintainers = with maintainers; [
      numinit
    ];
    mainProgram = "fstar.exe";
    platforms = with platforms; darwin ++ linux;
  };
+26 −0
Original line number Diff line number Diff line
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 4c17df2..4c3c311 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -600,8 +600,6 @@ public:
            out << " \n";
     }
 
-    bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; }
-
     bool column_has_upper_bound(unsigned j) const {
         switch(m_column_types[j]) {
         case column_type::free_column:
diff --git a/src/util/lp/static_matrix_def.h b/src/util/lp/static_matrix_def.h
index 7949573..2f1cb42 100644
--- a/src/util/lp/static_matrix_def.h
+++ b/src/util/lp/static_matrix_def.h
@@ -86,7 +86,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * /* basis *
     init_row_columns(m, m);
     while (m--) {
         for (auto & col : A.m_columns[m]){
-            set(col.var(), m, A.get_value_of_column_cell(col));
+            set(col.var(), m, A.get_column_cell(col));
         }
     }
 }
+106 −0
Original line number Diff line number Diff line
{
  fetchFromGitHub,
  fetchpatch,
  lib,
  replaceVars,
  stdenvNoCC,
  z3,
}:

let
  # fstar has a pretty hard dependency on certain z3 patch versions.
  # https://github.com/FStarLang/FStar/issues/3689#issuecomment-2625073641
  # We need to package all the Z3 versions it prefers here.
  fstarNewZ3Version = "4.13.3";
  fstarNewZ3 =
    if z3.version == fstarNewZ3Version then
      z3
    else
      z3.overrideAttrs (final: rec {
        version = fstarNewZ3Version;
        src = fetchFromGitHub {
          owner = "Z3Prover";
          repo = "z3";
          rev = "z3-${version}";
          hash = "sha256-odwalnF00SI+sJGHdIIv4KapFcfVVKiQ22HFhXYtSvA=";
        };
      });

  fstarOldZ3Version = "4.8.5";
  fstarOldZ3 =
    if z3.version == fstarOldZ3Version then
      z3
    else
      z3.overrideAttrs (prev: rec {
        version = fstarOldZ3Version;
        src = fetchFromGitHub {
          owner = "Z3Prover";
          repo = "z3";
          rev = "Z3-${version}"; # caps matter
          hash = "sha256-ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc=";
        };
        patches =
          let
            static-matrix-patch = fetchpatch {
              # clang / gcc fixes. fixes typos in some member names
              name = "gcc-15-fixes.patch";
              url = "https://github.com/Z3Prover/z3/commit/2ce89e5f491fa817d02d8fdce8c62798beab258b.patch";
              includes = [ "src/@dir@/lp/static_matrix.h" ];
              stripLen = 3;
              extraPrefix = "src/@dir@/";
              hash = "sha256-+H1/VJPyI0yq4M/61ay8SRCa6OaoJ/5i+I3zVTAPUVo=";
            };

            # replace @dir@ in the path of the given list of patches
            fixupPatches = dir: map (patch: replaceVars patch { dir = dir; });
          in
          prev.patches or [ ]
          ++ fixupPatches "util" [
            ./lower-bound-typo.diff
            static-matrix-patch
            ./tail-matrix.diff
          ]
          ++ [
            ./4-8-5-typos.diff
          ];

        postPatch =
          let
            python = lib.findFirst (pkg: lib.hasPrefix "python" pkg.pname) null prev.nativeBuildInputs;
          in

          assert python != null;

          prev.postPatch or ""
          +
            lib.optionalString
              ((lib.versionAtLeast python.version "3.12") && (lib.versionOlder version "4.8.14"))
              ''
                # See https://github.com/Z3Prover/z3/pull/5729. This is a specialization of this patch for 4.8.5.
                for file in scripts/mk_util.py src/api/python/CMakeLists.txt; do
                  substituteInPlace "$file" \
                    --replace-fail "distutils.sysconfig.get_python_lib()" "sysconfig.get_path('purelib')" \
                    --replace-fail "distutils.sysconfig" "sysconfig"
                done
              '';

      });
in
stdenvNoCC.mkDerivation {
  name = "fstar-z3";
  dontUnpack = true;

  installPhase = ''
    mkdir -p $out/bin
    ln -s ${lib.getExe fstarNewZ3} $out/bin/z3-${lib.escapeShellArg fstarNewZ3.version}
    ln -s ${lib.getExe fstarOldZ3} $out/bin/z3-${lib.escapeShellArg fstarOldZ3.version}
  '';

  passthru = rec {
    new = fstarNewZ3;
    "z3_${lib.replaceStrings [ "." ] [ "_" ] fstarNewZ3.version}" = new;

    old = fstarOldZ3;
    "z3_${lib.replaceStrings [ "." ] [ "_" ] fstarOldZ3.version}" = old;
  };
}
+13 −0
Original line number Diff line number Diff line
diff --git a/src/@dir@/lp/column_info.h b/src/@dir@/lp/column_info.h
index 1dc0c60..9cbeea6 100644
--- a/src/@dir@/lp/column_info.h
+++ b/src/@dir@/lp/column_info.h
@@ -47,7 +47,7 @@ public:
             m_lower_bound_is_strict == c.m_lower_bound_is_strict &&
             m_upper_bound_is_set == c.m_upper_bound_is_set&&
             m_upper_bound_is_strict == c.m_upper_bound_is_strict&&
-            (!m_lower_bound_is_set || m_lower_bound == c.m_low_bound) &&
+            (!m_lower_bound_is_set || m_lower_bound == c.m_lower_bound) &&
             (!m_upper_bound_is_set || m_upper_bound == c.m_upper_bound) &&
             m_cost == c.m_cost &&
             m_is_fixed == c.m_is_fixed &&
+12 −0
Original line number Diff line number Diff line
diff --git a/src/@dir@/lp/tail_matrix.h b/src/@dir@/lp/tail_matrix.h
index 2047e8c..c84340e 100644
--- a/src/@dir@/lp/tail_matrix.h
+++ b/src/@dir@/lp/tail_matrix.h
@@ -43,7 +43,6 @@ public:
         const tail_matrix & m_A;
         unsigned m_row;
         ref_row(const tail_matrix& m, unsigned row): m_A(m), m_row(row) {}
-        T operator[](unsigned j) const { return m_A.get_elem(m_row, j);}
     };
     ref_row operator[](unsigned i) const { return ref_row(*this, i);}
 };
Loading