tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{ stdenv, fetchFromGitHub, mono, fsharp, dotnetPackages, z3, ocamlPackages, openssl, makeWrapper, pkgconfig, file }:
2
3stdenv.mkDerivation rec {
4 name = "fstar-${version}";
5 version = "0.9.4.0";
6
7 src = fetchFromGitHub {
8 owner = "FStarLang";
9 repo = "FStar";
10 rev = "v${version}";
11 sha256 = "130779p5plsgvz0dkcqycns3vwrvyfl138nq2xdhd3rkdsbyyvb7";
12 };
13
14 nativeBuildInputs = [ makeWrapper ];
15
16 buildInputs = with ocamlPackages; [
17 mono fsharp z3 dotnetPackages.FsLexYacc ocaml findlib ocaml_batteries
18 zarith camlp4 yojson pprint openssl pkgconfig file
19 ];
20
21 preBuild = ''
22 substituteInPlace src/Makefile --replace "\$(RUNTIME) VS/.nuget/NuGet.exe" "true" \
23 --replace Darwin xyz
24 substituteInPlace src/VS/.nuget/NuGet.targets --replace "mono" "true"
25
26 # Fails with bad interpreter otherwise
27 patchShebangs src/tools
28 patchShebangs bin
29
30 export FSharpTargetsPath="$(dirname $(pkg-config FSharp.Core --variable=Libraries))/Microsoft.FSharp.Targets"
31 # remove hardcoded windows paths
32 sed -i '/<FSharpTargetsPath/d' src/*/*.fsproj
33
34 mkdir -p src/VS/packages/FsLexYacc.6.1.0
35 ln -s ${dotnetPackages.FsLexYacc}/lib/dotnet/FsLexYacc src/VS/packages/FsLexYacc.6.1.0/build
36 '';
37
38 makeFlags = [
39 "FSYACC=${dotnetPackages.FsLexYacc}/bin/fsyacc"
40 "FSLEX=${dotnetPackages.FsLexYacc}/bin/fslex"
41 "NUGET=true"
42 "PREFIX=$(out)"
43 ];
44
45 buildFlags = "-C src";
46
47 # Now that the .NET fstar.exe is built, use it to build the native OCaml binary
48 postBuild = ''
49 patchShebangs bin/fstar.exe
50
51 # Workaround for fsharp/fsharp#419
52 cp ${fsharp}/lib/mono/4.5/FSharp.Core.dll bin/
53
54 # Use the built .NET binary to extract the sources of itself from F* to OCaml
55 make ''${enableParallelBuilding:+-j''${NIX_BUILD_CORES} -l''${NIX_BUILD_CORES}} \
56 $makeFlags "''${makeFlagsArray[@]}" \
57 ocaml -C src
58
59 # Build the extracted OCaml sources
60 make ''${enableParallelBuilding:+-j''${NIX_BUILD_CORES} -l''${NIX_BUILD_CORES}} \
61 $makeFlags "''${makeFlagsArray[@]}" \
62 -C src/ocaml-output
63 '';
64
65 # https://github.com/FStarLang/FStar/issues/676
66 doCheck = false;
67
68 preCheck = "ulimit -s unlimited";
69
70 # Basic test suite:
71 #checkFlags = "VERBOSE=y -C examples";
72
73 # Complete, but heavyweight test suite:
74 checkTarget = "regressions";
75 checkFlags = "VERBOSE=y -C src";
76
77 installFlags = "-C src/ocaml-output";
78
79 postInstall = ''
80 wrapProgram $out/bin/fstar.exe --prefix PATH ":" "${z3}/bin"
81 '';
82
83 meta = with stdenv.lib; {
84 description = "ML-like functional programming language aimed at program verification";
85 homepage = https://www.fstar-lang.org;
86 license = licenses.asl20;
87 platforms = with platforms; darwin ++ linux;
88 };
89}