1{ lib, stdenv, fetchFromGitHub, z3, ocamlPackages, makeWrapper, installShellFiles }:
2
3stdenv.mkDerivation rec {
4 pname = "fstar";
5 version = "2022.01.15";
6
7 src = fetchFromGitHub {
8 owner = "FStarLang";
9 repo = "FStar";
10 rev = "v${version}";
11 sha256 = "sha256-bK3McF/wTjT9q6luihPaEXjx7Lu6+ZbQ9G61Mc4KoB0=";
12 };
13
14 strictDeps = true;
15
16 nativeBuildInputs = [
17 makeWrapper
18 installShellFiles
19 ] ++ (with ocamlPackages; [
20 ocaml
21 findlib
22 ocamlbuild
23 menhir
24 ]);
25
26 buildInputs = [
27 z3
28 ] ++ (with ocamlPackages; [
29 batteries
30 zarith
31 stdint
32 yojson
33 fileutils
34 menhirLib
35 pprint
36 sedlex
37 ppxlib
38 ppx_deriving
39 ppx_deriving_yojson
40 process
41 ]);
42
43 makeFlags = [ "PREFIX=$(out)" ];
44
45 buildFlags = [ "libs" ];
46
47 enableParallelBuilding = true;
48
49 postPatch = ''
50 patchShebangs ulib/gen_mllib.sh
51 substituteInPlace src/ocaml-output/Makefile --replace '$(COMMIT)' 'v${version}'
52 '';
53
54 preInstall = ''
55 mkdir -p $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstarlib
56 '';
57 postInstall = ''
58 wrapProgram $out/bin/fstar.exe --prefix PATH ":" "${z3}/bin"
59 installShellCompletion --bash .completion/bash/fstar.exe.bash
60 installShellCompletion --fish .completion/fish/fstar.exe.fish
61 installShellCompletion --zsh --name _fstar.exe .completion/zsh/__fstar.exe
62 '';
63
64 meta = with lib; {
65 description = "ML-like functional programming language aimed at program verification";
66 homepage = "https://www.fstar-lang.org";
67 changelog = "https://github.com/FStarLang/FStar/raw/v${version}/CHANGES.md";
68 license = licenses.asl20;
69 maintainers = with maintainers; [ gebner pnmadelaine ];
70 mainProgram = "fstar.exe";
71 platforms = with platforms; darwin ++ linux;
72 };
73}