diff --git a/pkgs/by-name/fs/fstar/package.nix b/pkgs/by-name/fs/fstar/package.nix new file mode 100644 index 000000000000..5d2561fbb7e7 --- /dev/null +++ b/pkgs/by-name/fs/fstar/package.nix @@ -0,0 +1,121 @@ +{ + callPackage, + fetchFromGitHub, + installShellFiles, + lib, + makeWrapper, + nix-update-script, + ocaml-ng, + removeReferencesTo, + util-linux, + which, +}: + +let + # The version of ocaml fstar uses. + ocamlPackages = ocaml-ng.ocamlPackages_4_14; + + fstarZ3 = callPackage ./z3 { }; +in +ocamlPackages.buildDunePackage rec { + pname = "fstar"; + version = "2025.03.25"; + + src = fetchFromGitHub { + owner = "FStarLang"; + repo = "FStar"; + rev = "v${version}"; + hash = "sha256-PhjfThXF6fJlFHtNEURG4igCnM6VegWODypmRvnZPdA="; + }; + + duneVersion = "3"; + + nativeBuildInputs = [ + ocamlPackages.menhir + which + util-linux + installShellFiles + makeWrapper + removeReferencesTo + ]; + + prePatch = '' + patchShebangs .scripts/*.sh + patchShebangs ulib/ml/app/ints/mk_int_file.sh + ''; + + buildInputs = with ocamlPackages; [ + batteries + menhir + menhirLib + pprint + ppx_deriving + ppx_deriving_yojson + ppxlib + process + sedlex + stdint + yojson + zarith + memtrace + mtime + ]; + + preConfigure = '' + mkdir -p cache + export DUNE_CACHE_ROOT="$(pwd)/cache" + export PATH="${lib.makeBinPath [ fstarZ3 ]}''${PATH:+:}$PATH" + export PREFIX="$out" + ''; + + buildPhase = '' + runHook preBuild + make -j$NIX_BUILD_CORES + runHook postBuild + ''; + + installPhase = '' + runHook preInstall + + make install + + remove-references-to -t '${ocamlPackages.ocaml}' $out/bin/fstar.exe + + 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 + + runHook postInstall + ''; + + enableParallelBuilding = true; + + 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; [ + numinit + ]; + mainProgram = "fstar.exe"; + platforms = with platforms; darwin ++ linux; + }; +} diff --git a/pkgs/by-name/fs/fstar/z3/4-8-5-typos.diff b/pkgs/by-name/fs/fstar/z3/4-8-5-typos.diff new file mode 100644 index 000000000000..64a4887e0ef4 --- /dev/null +++ b/pkgs/by-name/fs/fstar/z3/4-8-5-typos.diff @@ -0,0 +1,26 @@ +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::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)); + } + } + } diff --git a/pkgs/by-name/fs/fstar/z3/default.nix b/pkgs/by-name/fs/fstar/z3/default.nix new file mode 100644 index 000000000000..b0429deb8d0c --- /dev/null +++ b/pkgs/by-name/fs/fstar/z3/default.nix @@ -0,0 +1,106 @@ +{ + 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; + }; +} diff --git a/pkgs/by-name/fs/fstar/z3/lower-bound-typo.diff b/pkgs/by-name/fs/fstar/z3/lower-bound-typo.diff new file mode 100644 index 000000000000..254c35be5369 --- /dev/null +++ b/pkgs/by-name/fs/fstar/z3/lower-bound-typo.diff @@ -0,0 +1,13 @@ +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 && diff --git a/pkgs/by-name/fs/fstar/z3/tail-matrix.diff b/pkgs/by-name/fs/fstar/z3/tail-matrix.diff new file mode 100644 index 000000000000..4f680e7617d2 --- /dev/null +++ b/pkgs/by-name/fs/fstar/z3/tail-matrix.diff @@ -0,0 +1,12 @@ +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);} + }; diff --git a/pkgs/development/compilers/fstar/default.nix b/pkgs/development/compilers/fstar/default.nix deleted file mode 100644 index 0dd7a1819fa9..000000000000 --- a/pkgs/development/compilers/fstar/default.nix +++ /dev/null @@ -1,91 +0,0 @@ -{ - callPackage, - fetchFromGitHub, - installShellFiles, - lib, - makeWrapper, - ocamlPackages, - removeReferencesTo, - stdenv, - writeScript, - z3, -}: - -let - - version = "2024.09.05"; - - 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 - ; - }; - -in - -stdenv.mkDerivation { - pname = "fstar"; - inherit version src; - - nativeBuildInputs = [ - installShellFiles - makeWrapper - removeReferencesTo - ]; - - inherit (fstar-dune) propagatedBuildInputs; - - dontBuild = true; - - installPhase = '' - mkdir $out - - 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 - - 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 - - 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; { - 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; [ ]; - mainProgram = "fstar.exe"; - platforms = with platforms; darwin ++ linux; - }; -} diff --git a/pkgs/development/compilers/fstar/dune.nix b/pkgs/development/compilers/fstar/dune.nix deleted file mode 100644 index 3bdd62e88c47..000000000000 --- a/pkgs/development/compilers/fstar/dune.nix +++ /dev/null @@ -1,52 +0,0 @@ -{ - 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 deleted file mode 100644 index cc7651800df2..000000000000 --- a/pkgs/development/compilers/fstar/ulib.nix +++ /dev/null @@ -1,27 +0,0 @@ -{ - 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; -} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index e695a90ed900..cfc023b5c6a1 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -6486,11 +6486,6 @@ with pkgs; stdenv = gcc10Stdenv; }; - fstar = callPackage ../development/compilers/fstar { - ocamlPackages = ocaml-ng.ocamlPackages_4_14; - z3 = z3_4_8_5; - }; - dotnetPackages = recurseIntoAttrs (callPackage ./dotnet-packages.nix { }); gopro-tool = callPackage ../by-name/go/gopro-tool/package.nix {