fstar: 2024.09.05 -> 2025.03.25
The F* team significantly cleaned up the build. Based on the Nix expression here: https://github.com/FStarLang/FStar/blob/master/.nix/fstar.nix Move to by-name and adopt the Z3 4.8.5 patches since we are now the only package that depends on Z3 4.8.5 in nixpkgs.
This commit is contained in:
Morgan Jones
@@ -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;
|
||||
};
|
||||
}
|
||||
@@ -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<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));
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -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;
|
||||
};
|
||||
}
|
||||
@@ -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 &&
|
||||
@@ -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);}
|
||||
};
|
||||
@@ -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;
|
||||
};
|
||||
}
|
||||
@@ -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;
|
||||
}
|
||||
@@ -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;
|
||||
}
|
||||
@@ -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 {
|
||||
|
||||
Reference in New Issue
Block a user