79 lines
2.2 KiB
Nix
79 lines
2.2 KiB
Nix
|
{ stdenv, fetchFromGitHub, mono, fsharp, dotnetPackages, z3, ocamlPackages, openssl, makeWrapper }:
|
||
|
|
|
||
|
|
stdenv.mkDerivation rec {
|
||
|
|
name = "fstar-${version}";
|
||
|
|
version = "2016-01-12";
|
||
|
|
|
||
|
|
src = fetchFromGitHub {
|
||
|
|
owner = "FStarLang";
|
||
|
|
repo = "FStar";
|
||
|
|
rev = "af9a231566ca52c9bc3409398c801ae9e8191cfa";
|
||
|
|
sha256 = "1zri4gqr6j6hygnh0ckfhq93mqwk9i19vng8chnmvlr27zq734a2";
|
||
|
|
};
|
||
|
|
|
||
|
|
buildInputs = with ocamlPackages; [
|
||
|
|
mono fsharp z3 dotnetPackages.FsLexYacc ocaml findlib ocaml_batteries openssl makeWrapper
|
||
|
|
];
|
||
|
|
|
||
|
|
preBuild = ''
|
||
|
|
substituteInPlace src/Makefile --replace "\$(RUNTIME) VS/.nuget/NuGet.exe" "true"
|
||
|
|
|
||
|
|
source setenv.sh
|
||
|
|
'';
|
||
|
|
|
||
|
|
makeFlags = [
|
||
|
|
"FSYACC=${dotnetPackages.FsLexYacc}/bin/fsyacc"
|
||
|
|
"FSLEX=${dotnetPackages.FsLexYacc}/bin/fslex"
|
||
|
|
"NUGET=true"
|
||
|
|
"PREFIX=$(out)"
|
||
|
|
];
|
||
|
|
|
||
|
|
buildFlags = "-C src";
|
||
|
|
|
||
|
|
# Now that the .NET fstar.exe is built, use it to build the native OCaml binary
|
||
|
|
postBuild = ''
|
||
|
|
patchShebangs bin/fstar.exe
|
||
|
|
|
||
|
|
# Workaround for fsharp/fsharp#419
|
||
|
|
cp ${fsharp}/lib/mono/4.5/FSharp.Core.dll bin/
|
||
|
|
|
||
|
|
# Use the built .NET binary to extract the sources of itself from F* to OCaml
|
||
|
|
make ''${enableParallelBuilding:+-j''${NIX_BUILD_CORES} -l''${NIX_BUILD_CORES}} \
|
||
|
|
$makeFlags "''${makeFlagsArray[@]}" \
|
||
|
|
ocaml -C src
|
||
|
|
|
||
|
|
# Build the extracted OCaml sources
|
||
|
|
make ''${enableParallelBuilding:+-j''${NIX_BUILD_CORES} -l''${NIX_BUILD_CORES}} \
|
||
|
|
$makeFlags "''${makeFlagsArray[@]}" \
|
||
|
|
-C src/ocaml-output
|
||
|
|
'';
|
||
|
|
|
||
|
|
doCheck = true;
|
||
|
|
|
||
|
|
preCheck = "ulimit -s unlimited";
|
||
|
|
|
||
|
|
# Basic test suite:
|
||
|
|
#checkFlags = "VERBOSE=y -C examples";
|
||
|
|
|
||
|
|
# Complete, but heavyweight test suite:
|
||
|
|
checkTarget = "regressions";
|
||
|
|
checkFlags = "VERBOSE=y -C src";
|
||
|
|
|
||
|
|
installFlags = "-C src/ocaml-output";
|
||
|
|
|
||
|
|
postInstall = ''
|
||
|
|
# Workaround for FStarLang/FStar#456
|
||
|
|
mv $out/lib/fstar/* $out/lib/
|
||
|
|
rmdir $out/lib/fstar
|
||
|
|
|
||
|
|
wrapProgram $out/bin/fstar.exe --prefix PATH ":" "${z3}/bin"
|
||
|
|
'';
|
||
|
|
|
||
|
|
meta = with stdenv.lib; {
|
||
|
|
description = "ML-like functional programming language aimed at program verification";
|
||
|
|
homepage = "https://www.fstar-lang.org";
|
||
|
|
license = licenses.asl20;
|
||
|
|
platforms = with platforms; linux;
|
||
|
|
};
|
||
|
|
}
|