fstar: build with dune (#275924)

{ lib, stdenv, writeScript, fetchFromGitHub, z3, ocamlPackages, makeWrapper, installShellFiles, removeReferencesTo }:

{ callPackage

, fetchFromGitHub

, installShellFiles

, lib

, makeWrapper

, ocamlPackages

, removeReferencesTo

, stdenv

, writeScript

, z3

}:

let

stdenv.mkDerivation rec {

  pname = "fstar";

  version = "2023.09.03";

  src = fetchFromGitHub {

    hash = "sha256-ymoP5DvaLdrdwJcnhZnLEvwNxUFzhkICajPyK4lvacc=";

  };

  strictDeps = true;

  fstar-dune = ocamlPackages.callPackage ./dune.nix { inherit version src; };

  fstar-ulib = callPackage ./ulib.nix { inherit version src fstar-dune z3; };

in

stdenv.mkDerivation {

  pname = "fstar";

  inherit version src;

  nativeBuildInputs = [

    z3

    makeWrapper

    installShellFiles

    makeWrapper

    removeReferencesTo

  ] ++ (with ocamlPackages; [

    ocaml

    dune_3

    findlib

    ocamlbuild

    menhir

  ]);

  buildInputs = with ocamlPackages; [

    batteries

    zarith

    stdint

    yojson

    fileutils

    memtrace

    menhirLib

    pprint

    sedlex

    ppxlib

    ppx_deriving

    ppx_deriving_yojson

    process

  ];

  makeFlags = [ "PREFIX=$(out)" ];

  inherit (fstar-dune) propagatedBuildInputs;

  enableParallelBuilding = true;

  dontBuild = true;

  postPatch = ''

    patchShebangs ulib/install-ulib.sh

  '';

  installPhase = ''

    mkdir $out

  preInstall = ''

    mkdir -p $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstarlib

  '';

  postInstall = ''

    # Remove build artifacts

    find $out -name _build -type d | xargs -I{} rm -rf "{}"

    CP="cp -r --no-preserve=mode"

    $CP ${fstar-dune}/* $out

    $CP ${fstar-ulib}/* $out

    PREFIX=$out make -C src/ocaml-output install-sides

    chmod +x $out/bin/fstar.exe

    wrapProgram $out/bin/fstar.exe --prefix PATH ":" ${z3}/bin

    remove-references-to -t '${ocamlPackages.ocaml}' $out/bin/fstar.exe

    wrapProgram $out/bin/fstar.exe --prefix PATH ":" "${z3}/bin"

    substituteInPlace $out/lib/ocaml/${ocamlPackages.ocaml.version}/site-lib/fstar/dune-package \

      --replace ${fstar-dune} $out

    installShellCompletion --bash .completion/bash/fstar.exe.bash

    installShellCompletion --fish .completion/fish/fstar.exe.fish

    installShellCompletion --zsh --name _fstar.exe .completion/zsh/__fstar.exe

{ batteries

, buildDunePackage

, memtrace

, menhir

, menhirLib

, pprint

, ppx_deriving

, ppx_deriving_yojson

, ppxlib

, process

, sedlex

, src

, stdint

, version

, yojson

, zarith

}:

buildDunePackage {

  pname = "fstar";

  inherit version src;

  postPatch = ''

    patchShebangs ocaml/fstar-lib/make_fstar_version.sh

    cd ocaml

  '';

  nativeBuildInputs = [

    menhir

  ];

  buildInputs = [

    memtrace

  ];

  propagatedBuildInputs = [

    batteries

    menhirLib

    pprint

    ppx_deriving

    ppx_deriving_yojson

    ppxlib

    process

    sedlex

    stdint

    yojson

    zarith

  ];

  enableParallelBuilding = true;

}

{ fstar-dune

, src

, stdenv

, version

, z3

}:

stdenv.mkDerivation {

  pname = "fstar-ulib";

  inherit version src;

  nativeBuildInputs = [

    z3

  ];

  postPatch = ''

    mkdir -p bin

    cp ${fstar-dune}/bin/fstar.exe bin

    patchShebangs ulib/install-ulib.sh

    cd ulib

  '';

  makeFlags = [ "PREFIX=$(out)" ];

  enableParallelBuilding = true;

}