a13cdfe520
To keep this for the future we also strictDeps where possible, including for janePackages, topkg, oasis and ocamlbuild. This makes some closures significantly smaller and makes cross compilation easier
72 lines
1.7 KiB
Nix
72 lines
1.7 KiB
Nix
{ lib, stdenv, fetchFromGitHub, z3, ocamlPackages, makeWrapper, installShellFiles }:
|
|
|
|
stdenv.mkDerivation rec {
|
|
pname = "fstar";
|
|
version = "2022.01.15";
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "FStarLang";
|
|
repo = "FStar";
|
|
rev = "v${version}";
|
|
sha256 = "sha256-bK3McF/wTjT9q6luihPaEXjx7Lu6+ZbQ9G61Mc4KoB0=";
|
|
};
|
|
|
|
strictDeps = true;
|
|
|
|
nativeBuildInputs = [
|
|
makeWrapper
|
|
installShellFiles
|
|
] ++ (with ocamlPackages; [
|
|
ocaml
|
|
findlib
|
|
ocamlbuild
|
|
menhir
|
|
]);
|
|
|
|
buildInputs = [
|
|
z3
|
|
] ++ (with ocamlPackages; [
|
|
batteries
|
|
zarith
|
|
stdint
|
|
yojson
|
|
fileutils
|
|
menhirLib
|
|
pprint
|
|
sedlex_2
|
|
ppxlib
|
|
ppx_deriving
|
|
ppx_deriving_yojson
|
|
process
|
|
]);
|
|
|
|
makeFlags = [ "PREFIX=$(out)" ];
|
|
|
|
buildFlags = [ "libs" ];
|
|
|
|
enableParallelBuilding = true;
|
|
|
|
postPatch = ''
|
|
patchShebangs ulib/gen_mllib.sh
|
|
substituteInPlace src/ocaml-output/Makefile --replace '$(COMMIT)' 'v${version}'
|
|
'';
|
|
|
|
preInstall = ''
|
|
mkdir -p $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstarlib
|
|
'';
|
|
postInstall = ''
|
|
wrapProgram $out/bin/fstar.exe --prefix PATH ":" "${z3}/bin"
|
|
installShellCompletion --bash .completion/bash/fstar.exe.bash
|
|
installShellCompletion --fish .completion/fish/fstar.exe.fish
|
|
installShellCompletion --zsh --name _fstar.exe .completion/zsh/__fstar.exe
|
|
'';
|
|
|
|
meta = with lib; {
|
|
description = "ML-like functional programming language aimed at program verification";
|
|
homepage = "https://www.fstar-lang.org";
|
|
license = licenses.asl20;
|
|
changelog = "https://github.com/FStarLang/FStar/raw/v${version}/CHANGES.md";
|
|
platforms = with platforms; darwin ++ linux;
|
|
maintainers = with maintainers; [ gebner pnmadelaine ];
|
|
};
|
|
}
|