tjh.dev
1{ callPackage
2, fetchFromGitHub
3, installShellFiles
4, lib
5, makeWrapper
6, ocamlPackages
7, removeReferencesTo
8, stdenv
9, writeScript
10, z3
11}:
12
13let
14
15 version = "2024.01.13";
16
17 src = fetchFromGitHub {
18 owner = "FStarLang";
19 repo = "FStar";
20 rev = "v${version}";
21 hash = "sha256-xjSWDP8mSjLcn+0hsRpEdzsBgBR+mKCZB8yLmHl+WqE=";
22 };
23
24 fstar-dune = ocamlPackages.callPackage ./dune.nix { inherit version src; };
25
26 fstar-ulib = callPackage ./ulib.nix { inherit version src fstar-dune z3; };
27
28in
29
30stdenv.mkDerivation {
31 pname = "fstar";
32 inherit version src;
33
34 nativeBuildInputs = [
35 installShellFiles
36 makeWrapper
37 removeReferencesTo
38 ];
39
40 inherit (fstar-dune) propagatedBuildInputs;
41
42 dontBuild = true;
43
44 installPhase = ''
45 mkdir $out
46
47 CP="cp -r --no-preserve=mode"
48 $CP ${fstar-dune}/* $out
49 $CP ${fstar-ulib}/* $out
50
51 PREFIX=$out make -C src/ocaml-output install-sides
52
53 chmod +x $out/bin/fstar.exe
54 wrapProgram $out/bin/fstar.exe --prefix PATH ":" ${z3}/bin
55 remove-references-to -t '${ocamlPackages.ocaml}' $out/bin/fstar.exe
56
57 substituteInPlace $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstar/dune-package \
58 --replace ${fstar-dune} $out
59
60 installShellCompletion --bash .completion/bash/fstar.exe.bash
61 installShellCompletion --fish .completion/fish/fstar.exe.fish
62 installShellCompletion --zsh --name _fstar.exe .completion/zsh/__fstar.exe
63 '';
64
65 passthru.updateScript = writeScript "update-fstar" ''
66 #!/usr/bin/env nix-shell
67 #!nix-shell -i bash -p git gnugrep common-updater-scripts
68 set -eu -o pipefail
69
70 version="$(git ls-remote --tags git@github.com:FStarLang/FStar.git | grep -Po 'v\K\d{4}\.\d{2}\.\d{2}' | sort | tail -n1)"
71 update-source-version fstar "$version"
72 '';
73
74 meta = with lib; {
75 description = "ML-like functional programming language aimed at program verification";
76 homepage = "https://www.fstar-lang.org";
77 changelog = "https://github.com/FStarLang/FStar/raw/v${version}/CHANGES.md";
78 license = licenses.asl20;
79 maintainers = with maintainers; [ gebner pnmadelaine ];
80 mainProgram = "fstar.exe";
81 platforms = with platforms; darwin ++ linux;
82 };
83}