diff options
author | Ricardo M. Correia <rcorreia@wizy.org> | 2016-01-19 01:44:21 +0100 |
---|---|---|
committer | Ricardo M. Correia <rcorreia@wizy.org> | 2016-01-19 01:46:30 +0100 |
commit | 097c82f6c5db7dcd6fb4884680e8ba39b99dc00c (patch) | |
tree | a7d4f96f7cd825bed07366a9dd9ad2807183d00d /pkgs/development/compilers/fstar | |
parent | 3b381d37ee7d9a70e6e5f668966b7927353091f6 (diff) |
fstar: init at 2016-01-12
Diffstat (limited to 'pkgs/development/compilers/fstar')
-rw-r--r-- | pkgs/development/compilers/fstar/default.nix | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/pkgs/development/compilers/fstar/default.nix b/pkgs/development/compilers/fstar/default.nix new file mode 100644 index 000000000000..e6fe97c6fe8f --- /dev/null +++ b/pkgs/development/compilers/fstar/default.nix @@ -0,0 +1,78 @@ +{ 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; + }; +} |