Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .envrc
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
use flake
17 changes: 17 additions & 0 deletions .github/workflows/nix.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# This workflow tests the Nix build of pulse. We run it only for PRs (not
# on every push) and we use Github hosted runners.

name: Nix Build

on:
pull_request:

jobs:
nix-build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: DeterminateSystems/nix-installer-action@main
- uses: DeterminateSystems/magic-nix-cache-action@main
- name: Build
run: nix build -L
129 changes: 129 additions & 0 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

117 changes: 117 additions & 0 deletions flake.nix
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
{
inputs = {
flake-parts.url = "github:hercules-ci/flake-parts";
fstar.url = "github:FStarLang/FStar/v2025.03.25";
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
};

outputs = { ... }@inputs:

inputs.flake-parts.lib.mkFlake { inherit inputs; } {

systems = inputs.nixpkgs.lib.systems.flakeExposed;
imports = [ ];

perSystem = { pkgs, config, system, ... }: {

packages.pulse = pkgs.stdenv.mkDerivation rec {

pname = "pulse";
version = "9a03472d2c366bde5f7b0497bf3356dd445ce207";
src = pkgs.fetchFromGitHub {
owner = "FStarLang";
repo = pname;
rev = "${version}";
hash = "sha256-YgWxnX+gCVYx+CCIuprDYKewyEaSekqAilB96eyq+fk=";
};

inherit (pkgs.fstar) nativeBuildInputs;
buildInputs = pkgs.fstar.buildInputs ++ [
pkgs.fstar
pkgs.which
];
PATH = "${pkgs.fstar}/bin:$PATH";

enableParallelBuilding = true;

installPhase = ''
PREFIX=$out make install
'';

};

packages.pulse-exe = pkgs.writeShellScriptBin "pulse.exe" ''
exec ${pkgs.fstar}/bin/fstar.exe "$1" \
--include ${config.packages.pulse}/lib/pulse \
--include ${config.packages.pulse}/lib/pulse/checker \
--include ${config.packages.pulse}/lib/pulse/extraction \
--include ${config.packages.pulse}/lib/pulse/lib \
--include ${config.packages.pulse}/lib/pulse/ml \
--include ${config.packages.pulse}/lib/pulse/syntax_extension \
--load_cmxs pulse \
"$@"
'';
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A nit here, given that lib/fstar.include exists, the only thing needed is --include ${config.packages.pulse}/lib.

(Also F* will try to automatically load plugins when there's is a #lang-X directive, so the --load_cmxs is mostly redundant, but still required for some files currently, so best to keep it.)

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, I have to figure out how to get the lib/fstar.include to be found. For some reason I could not get the command to work unless the paths are exhaustively and explicitly included.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah.. interesting. Then this is fine and we can later try to reduce it, fstar.include is rather new so no worries.


packages.rustast-bindings = pkgs.rustPlatform.buildRustPackage rec {
inherit (config.packages.pulse) version src;
inherit (pkgs.fstar) nativeBuildInputs;
pname = "rustast-bindings";
sourceRoot = "${src.name}/pulse2rust/src/ocaml";
cargoLock = {
lockFile = ./pulse2rust/src/ocaml/Cargo.lock;
};
postPatch = ''
ln -s ${./pulse2rust/src/ocaml/Cargo.lock} Cargo.lock
'';
};

packages.extract = pkgs.stdenv.mkDerivation {
inherit (config.packages.pulse) version src;
pname = "extract";
sourceRoot = "source/pulse2rust/src";
buildInputs = [
pkgs.fstar
pkgs.which
];
PATH = "${pkgs.fstar}/bin:$PATH";

installPhase = ''
mkdir -p $out/ocaml/generated
cp -r ocaml/generated $out/ocaml
'';
};

packages.pulse2rust = pkgs.ocaml-ng.ocamlPackages_4_14.buildDunePackage rec {
inherit (config.packages.pulse) version src;
pname = "main";
sourceRoot = "${src.name}/pulse2rust/src/ocaml";

nativeBuildInputs = pkgs.fstar.nativeBuildInputs ++ [ pkgs.fstar ];
buildInputs = pkgs.fstar.buildInputs ++ [ pkgs.fstar ];

buildPhase = ''
eval $(${pkgs.fstar}/bin/fstar.exe --ocamlenv)
mkdir -p $out/bin
dune build main.exe --build-dir=$out/bin
'';

postPatch = ''
ln -s ${./pulse2rust/src/dune-project} dune-project
ln -s ${config.packages.rustast-bindings}/lib/librustast_bindings.a librustast_bindings.a
mkdir -p ocaml/generated
cp -r ${config.packages.extract}/ocaml/generated ocaml
'';

# overwrites the default dune installPhase
installPhase = '''';

meta.mainProgram = "default/ocaml/main.exe";
};

packages.fstar = pkgs.fstar;

packages.default = config.packages.pulse;

};
};
}
115 changes: 115 additions & 0 deletions pulse2rust/src/ocaml/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.