From ea5d963d238ee1d667d488bdc32d600b38bcbaf5 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Thu, 28 Nov 2024 11:28:12 +0000 Subject: [PATCH 01/17] nix: init --- .envrc | 10 ++ flake.lock | 385 +++++++++++++++++++++++++++++++++++++++++++++++++++++ flake.nix | 97 ++++++++++++++ 3 files changed, 492 insertions(+) create mode 100644 .envrc create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.envrc b/.envrc new file mode 100644 index 000000000..dc25ec711 --- /dev/null +++ b/.envrc @@ -0,0 +1,10 @@ +if ! has nix_direnv_version || ! nix_direnv_version 2.2.1; then + source_url "https://raw.githubusercontent.com/nix-community/nix-direnv/2.2.1/direnvrc" "sha256-zelF0vLbEl5uaqrfIzbgNzJWGmLzCmYAkInj/LNxvKs=" +fi + +watch_file flake.nix +watch_file flake.lock +if ! use flake . --no-pure-eval +then + echo "devenv could not be built. The devenv environment was not loaded. Make the necessary changes to devenv.nix and hit enter to try again." >&2 +fi diff --git a/flake.lock b/flake.lock new file mode 100644 index 000000000..93186cc18 --- /dev/null +++ b/flake.lock @@ -0,0 +1,385 @@ +{ + "nodes": { + "cachix": { + "inputs": { + "devenv": [ + "devenv" + ], + "flake-compat": [ + "devenv" + ], + "git-hooks": [ + "devenv" + ], + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1728672398, + "narHash": "sha256-KxuGSoVUFnQLB2ZcYODW7AVPAh9JqRlD5BrfsC/Q4qs=", + "owner": "cachix", + "repo": "cachix", + "rev": "aac51f698309fd0f381149214b7eee213c66ef0a", + "type": "github" + }, + "original": { + "owner": "cachix", + "ref": "latest", + "repo": "cachix", + "type": "github" + } + }, + "devenv": { + "inputs": { + "cachix": "cachix", + "flake-compat": "flake-compat", + "git-hooks": "git-hooks", + "nix": "nix", + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1732585607, + "narHash": "sha256-6ffeaSMuaL326f7KrCeScpSJtdHsFKS9gPrsSZkndvU=", + "owner": "cachix", + "repo": "devenv", + "rev": "a520f05c40ebecaf5e17064b27e28ba8e70c49fb", + "type": "github" + }, + "original": { + "owner": "cachix", + "repo": "devenv", + "type": "github" + } + }, + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, + "flake-parts": { + "inputs": { + "nixpkgs-lib": [ + "devenv", + "nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1712014858, + "narHash": "sha256-sB4SWl2lX95bExY2gMFG5HIzvva5AVMJd4Igm+GpZNw=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "9126214d0a59633752a136528f5f3b9aa8565b7d", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "flake-parts_2": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, + "locked": { + "lastModified": 1730504689, + "narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "506278e768c2a08bec68eb62932193e341f55c90", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1692799911, + "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44", + "type": "github" + }, + "original": { + "id": "flake-utils", + "type": "indirect" + } + }, + "fstar": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs_3" + }, + "locked": { + "lastModified": 1714406088, + "narHash": "sha256-v4oEXSb8gVgc1xTU+A8/7VhzPYI5AV1cgYXmPWYaHIg=", + "owner": "FStarLang", + "repo": "FStar", + "rev": "a94456863e3f971a7c63a64aca1a07d2cd9eb9a1", + "type": "github" + }, + "original": { + "owner": "FStarLang", + "repo": "FStar", + "rev": "a94456863e3f971a7c63a64aca1a07d2cd9eb9a1", + "type": "github" + } + }, + "git-hooks": { + "inputs": { + "flake-compat": [ + "devenv" + ], + "gitignore": "gitignore", + "nixpkgs": [ + "devenv", + "nixpkgs" + ], + "nixpkgs-stable": [ + "devenv" + ] + }, + "locked": { + "lastModified": 1730302582, + "narHash": "sha256-W1MIJpADXQCgosJZT8qBYLRuZls2KSiKdpnTVdKBuvU=", + "owner": "cachix", + "repo": "git-hooks.nix", + "rev": "af8a16fe5c264f5e9e18bcee2859b40a656876cf", + "type": "github" + }, + "original": { + "owner": "cachix", + "repo": "git-hooks.nix", + "type": "github" + } + }, + "gitignore": { + "inputs": { + "nixpkgs": [ + "devenv", + "git-hooks", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1709087332, + "narHash": "sha256-HG2cCnktfHsKV0s4XW83gU3F57gaTljL9KNSuG6bnQs=", + "owner": "hercules-ci", + "repo": "gitignore.nix", + "rev": "637db329424fd7e46cf4185293b9cc8c88c95394", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "gitignore.nix", + "type": "github" + } + }, + "libgit2": { + "flake": false, + "locked": { + "lastModified": 1697646580, + "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=", + "owner": "libgit2", + "repo": "libgit2", + "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5", + "type": "github" + }, + "original": { + "owner": "libgit2", + "repo": "libgit2", + "type": "github" + } + }, + "nix": { + "inputs": { + "flake-compat": [ + "devenv" + ], + "flake-parts": "flake-parts", + "libgit2": "libgit2", + "nixpkgs": "nixpkgs_2", + "nixpkgs-23-11": [ + "devenv" + ], + "nixpkgs-regression": [ + "devenv" + ], + "pre-commit-hooks": [ + "devenv" + ] + }, + "locked": { + "lastModified": 1727438425, + "narHash": "sha256-X8ES7I1cfNhR9oKp06F6ir4Np70WGZU5sfCOuNBEwMg=", + "owner": "domenkozar", + "repo": "nix", + "rev": "f6c5ae4c1b2e411e6b1e6a8181cc84363d6a7546", + "type": "github" + }, + "original": { + "owner": "domenkozar", + "ref": "devenv-2.24", + "repo": "nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1730531603, + "narHash": "sha256-Dqg6si5CqIzm87sp57j5nTaeBbWhHFaVyG7V6L8k3lY=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "7ffd9ae656aec493492b44d0ddfb28e79a1ea25d", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-lib": { + "locked": { + "lastModified": 1730504152, + "narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=", + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz" + }, + "original": { + "type": "tarball", + "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1717432640, + "narHash": "sha256-+f9c4/ZX5MWDOuB1rKoWj+lBNm0z0rs4CK47HBLxy1o=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "88269ab3044128b7c2f4c7d68448b2fb50456870", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "release-24.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_3": { + "locked": { + "lastModified": 1693158576, + "narHash": "sha256-aRTTXkYvhXosGx535iAFUaoFboUrZSYb1Ooih/auGp0=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "a999c1cc0c9eb2095729d5aa03e0d8f7ed256780", + "type": "github" + }, + "original": { + "id": "nixpkgs", + "ref": "nixos-unstable", + "type": "indirect" + } + }, + "nixpkgs_4": { + "locked": { + "lastModified": 1716977621, + "narHash": "sha256-Q1UQzYcMJH4RscmpTkjlgqQDX5yi1tZL0O345Ri6vXQ=", + "owner": "cachix", + "repo": "devenv-nixpkgs", + "rev": "4267e705586473d3e5c8d50299e71503f16a6fb6", + "type": "github" + }, + "original": { + "owner": "cachix", + "ref": "rolling", + "repo": "devenv-nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "devenv": "devenv", + "flake-parts": "flake-parts_2", + "fstar": "fstar", + "nixpkgs": "nixpkgs_4", + "systems": "systems_2", + "treefmt-nix": "treefmt-nix" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_2": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "treefmt-nix": { + "inputs": { + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1732643199, + "narHash": "sha256-uI7TXEb231o8dkwB5AUCecx3AQtosRmL6hKgnckvjps=", + "owner": "numtide", + "repo": "treefmt-nix", + "rev": "84637a7ab04179bdc42aa8fd0af1909fba76ad0c", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "treefmt-nix", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 000000000..45b51e05d --- /dev/null +++ b/flake.nix @@ -0,0 +1,97 @@ +{ + inputs = { + nixpkgs.url = "github:cachix/devenv-nixpkgs/rolling"; + systems.url = "github:nix-systems/default"; + fstar.url = "github:FStarLang/FStar/a94456863e3f971a7c63a64aca1a07d2cd9eb9a1"; + devenv.url = "github:cachix/devenv"; + devenv.inputs.nixpkgs.follows = "nixpkgs"; + flake-parts.url = "github:hercules-ci/flake-parts"; + treefmt-nix.url = "github:numtide/treefmt-nix"; + treefmt-nix.inputs.nixpkgs.follows = "nixpkgs"; + }; + + nixConfig = { + extra-trusted-public-keys = "devenv.cachix.org-1:w1cLUi8dv3hnoSPGAuibQv+f9TZLr6cv/Hm9XgU50cw="; + extra-substituters = "https://devenv.cachix.org"; + }; + + outputs = { self, ... }@inputs: + + inputs.flake-parts.lib.mkFlake { inherit inputs; } rec { + + systems = inputs.nixpkgs.lib.systems.flakeExposed; + imports = [ + inputs.treefmt-nix.flakeModule + ]; + + perSystem = { pkgs, config, system, ... }: { + + treefmt.config = { + projectRootFile = "flake.nix"; + flakeFormatter = true; + flakeCheck = true; + programs = { + nixpkgs-fmt.enable = true; + deadnix.enable = true; + statix.enable = true; + }; + }; + + devShells = { + default = inputs.devenv.lib.mkShell { + inherit inputs pkgs; + modules = [ + { + # https://devenv.sh/reference/options/ + packages = [ + inputs.fstar.packages.${system}.z3 + ] ++ (with inputs.fstar.packages.${system}.ocamlPackages; [ + menhir + batteries + menhirLib + pprint + ppx_deriving + ppx_deriving_yojson + ppxlib + process + sedlex + stdint + yojson + zarith + ]); + + env.OCAMLPATH = "${inputs.fstar.packages.${system}.fstar}/lib/ocaml/4.14.1/site-lib"; + env.PULSE_HOME = "."; + enterShell = '' + export PATH="${inputs.fstar.packages.${system}.fstar}/bin:$PATH" + ''; + + languages.ocaml = { + enable = true; + packages = inputs.fstar.packages.${system}.ocamlPackages; + }; + + scripts.pulse.exec = '' + fstar.exe $1 \ + --include ./lib/pulse/lib/class \ + --include ./lib/pulse/lib/pledge \ + --include ./lib/pulse/lib/pulse \ + --include ./lib/pulse/lib/pulse/core \ + --include ./lib/pulse/lib/pulse/lib \ + --load_cmxs lib/pulse/pulse + ''; + } + ]; + }; + }; + + packages = { + devenv-up = self.devShells.${system}.default.config.procfileScript; + devenv-test = self.devShells.${system}.default.config.test; + + inherit (inputs.fstar.packages.${system}) fstar fstar-dune; + }; + + }; + }; +} From d160c8d2dec0d486fe412ec7efa18e2d9fc6af03 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Sat, 30 Nov 2024 21:31:59 +0000 Subject: [PATCH 02/17] flake/packages: add pulse-dune --- flake.nix | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/flake.nix b/flake.nix index 45b51e05d..b161c697d 100644 --- a/flake.nix +++ b/flake.nix @@ -37,6 +37,24 @@ }; }; + packages.pulse-dune = pkgs.ocaml-ng.ocamlPackages_4_14.buildDunePackage rec { + + pname = "pulse-dune"; + version = "2024.06.02"; + sourceRoot = "${src.name}/src/ocaml"; + + src = pkgs.fetchFromGitHub { + owner = "FStarLang"; + repo = pname; + rev = "v${version}"; + hash = "sha256-jRm21FtPorAW/eQlXbqPyo2Ev0Kdv0evvGmSoPpNE7A="; + }; + + inherit (inputs.fstar.packages.${system}.fstar-dune) nativeBuildInputs; + + buildInputs = inputs.fstar.packages.${system}.fstar-dune.buildInputs ++ [ inputs.fstar.packages.${system}.fstar-dune ]; + + }; devShells = { default = inputs.devenv.lib.mkShell { inherit inputs pkgs; From 9dc2fce728b7ace68b6f01061bb55d051856c8c4 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Sat, 30 Nov 2024 21:33:09 +0000 Subject: [PATCH 03/17] flake/packages: add pulse --- flake.nix | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/flake.nix b/flake.nix index b161c697d..1de4eb4bb 100644 --- a/flake.nix +++ b/flake.nix @@ -54,6 +54,34 @@ buildInputs = inputs.fstar.packages.${system}.fstar-dune.buildInputs ++ [ inputs.fstar.packages.${system}.fstar-dune ]; + }; + + packages.pulse = pkgs.stdenv.mkDerivation rec { + + pname = "pulse"; + version = "2024.06.02"; + + src = pkgs.fetchFromGitHub { + owner = "FStarLang"; + repo = pname; + rev = "v${version}"; + hash = "sha256-jRm21FtPorAW/eQlXbqPyo2Ev0Kdv0evvGmSoPpNE7A="; + }; + + inherit (inputs.fstar.packages.${system}.fstar-dune) nativeBuildInputs; + + buildInputs = inputs.fstar.packages.${system}.fstar-dune.buildInputs ++ [ + inputs.fstar.packages.${system}.fstar + pkgs.which + ]; + PATH = "${inputs.fstar.packages.${system}.fstar}/bin:$PATH"; + + enableParallelBuilding = true; + + installPhase = '' + PREFIX=$out make install + ''; + }; devShells = { default = inputs.devenv.lib.mkShell { From 11247d80d9fb5c2feee76a84be3f18d4419c66c2 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Sat, 30 Nov 2024 21:34:01 +0000 Subject: [PATCH 04/17] flake/packages: add pulse-exe --- flake.nix | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/flake.nix b/flake.nix index 1de4eb4bb..5548fb001 100644 --- a/flake.nix +++ b/flake.nix @@ -83,6 +83,20 @@ ''; }; + + packages.pulse-exe = pkgs.writeShellScriptBin "pulse.exe" '' + exec ${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe "$1" \ + --include ${config.packages.pulse}/lib/pulse \ + --include ${config.packages.pulse}/lib/pulse/c \ + --include ${config.packages.pulse}/lib/pulse/core \ + --include ${config.packages.pulse}/lib/pulse/lib \ + --include ${config.packages.pulse}/lib/pulse/lib/class \ + --include ${config.packages.pulse}/lib/pulse/lib/ml \ + --include ${config.packages.pulse}/lib/pulse/lib/pledge \ + --load_cmxs pulse \ + "$@" + ''; + devShells = { default = inputs.devenv.lib.mkShell { inherit inputs pkgs; From d7a5d7e571937bd240e9609ef9cb2c02505ee3e5 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 9 Dec 2024 15:52:21 +0000 Subject: [PATCH 05/17] flake/packages: dynamic upstream ocaml imports --- flake.nix | 19 +++---------------- 1 file changed, 3 insertions(+), 16 deletions(-) diff --git a/flake.nix b/flake.nix index 5548fb001..54cdd9168 100644 --- a/flake.nix +++ b/flake.nix @@ -103,22 +103,9 @@ modules = [ { # https://devenv.sh/reference/options/ - packages = [ - inputs.fstar.packages.${system}.z3 - ] ++ (with inputs.fstar.packages.${system}.ocamlPackages; [ - menhir - batteries - menhirLib - pprint - ppx_deriving - ppx_deriving_yojson - ppxlib - process - sedlex - stdint - yojson - zarith - ]); + packages = with inputs.fstar.packages.${system}; [ z3 ] + ++ fstar-dune.buildInputs + ++ fstar-dune.nativeBuildInputs; env.OCAMLPATH = "${inputs.fstar.packages.${system}.fstar}/lib/ocaml/4.14.1/site-lib"; env.PULSE_HOME = "."; From 3a4cf12f9395b9e80760e5dc1ad6038d75e59078 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 9 Dec 2024 15:57:48 +0000 Subject: [PATCH 06/17] flake,CI: add nix build CI support for pulse --- .envrc | 2 +- .github/workflows/nix.yaml | 17 +++++++++++++++++ flake.nix | 2 ++ 3 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/nix.yaml diff --git a/.envrc b/.envrc index dc25ec711..f63cb7a1f 100644 --- a/.envrc +++ b/.envrc @@ -4,7 +4,7 @@ fi watch_file flake.nix watch_file flake.lock -if ! use flake . --no-pure-eval +if ! use flake . --no-pure-eval --accept-flake-config then echo "devenv could not be built. The devenv environment was not loaded. Make the necessary changes to devenv.nix and hit enter to try again." >&2 fi diff --git a/.github/workflows/nix.yaml b/.github/workflows/nix.yaml new file mode 100644 index 000000000..8338fb08b --- /dev/null +++ b/.github/workflows/nix.yaml @@ -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 diff --git a/flake.nix b/flake.nix index 54cdd9168..3fab27e62 100644 --- a/flake.nix +++ b/flake.nix @@ -133,6 +133,8 @@ }; packages = { + default = config.packages.pulse; + devenv-up = self.devShells.${system}.default.config.procfileScript; devenv-test = self.devShells.${system}.default.config.test; From 0d06220e1fd910571e784427539ff3f9f08003ff Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 6 Jan 2025 16:42:59 +0000 Subject: [PATCH 07/17] nix: add Cargo.lock --- pulse2rust/src/ocaml/Cargo.lock | 115 ++++++++++++++++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 pulse2rust/src/ocaml/Cargo.lock diff --git a/pulse2rust/src/ocaml/Cargo.lock b/pulse2rust/src/ocaml/Cargo.lock new file mode 100644 index 000000000..724c43893 --- /dev/null +++ b/pulse2rust/src/ocaml/Cargo.lock @@ -0,0 +1,115 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "cc" +version = "1.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "27f657647bcff5394bf56c7317665bbf790a137a50eaaa5c6bfbb9e27a518f2d" +dependencies = [ + "shlex", +] + +[[package]] +name = "cty" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b365fabc795046672053e29c954733ec3b05e4be654ab130fe8f1f94d7051f35" + +[[package]] +name = "ocaml-boxroot-sys" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5186393bfbee4ce2bc5bbb82beafb77e85c1d0a557e3cfc8c8a0d63d7845fed5" +dependencies = [ + "cc", +] + +[[package]] +name = "ocaml-interop" +version = "0.9.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ce6dfec8cfe7907ee7c62a853f849861f05747f3514126bfdb7c0c842513a9e" +dependencies = [ + "ocaml-boxroot-sys", + "ocaml-sys", + "static_assertions", +] + +[[package]] +name = "ocaml-sys" +version = "0.22.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73ec6ca7d41458442627435afb8f4671e83fd642e8a560171d671a1f679aa3cf" +dependencies = [ + "cty", +] + +[[package]] +name = "prettyplease" +version = "0.2.25" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "64d1ec885c64d0457d564db4ec299b2dae3f9c02808b8ad9c3a089c591b18033" +dependencies = [ + "proc-macro2", + "syn", +] + +[[package]] +name = "proc-macro2" +version = "1.0.92" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rustast_bindings" +version = "0.1.0" +dependencies = [ + "ocaml-interop", + "prettyplease", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "static_assertions" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" + +[[package]] +name = "syn" +version = "2.0.90" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83" From f9e6faadc634c65fc5618f3f01229e88abc3dfcc Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 6 Jan 2025 17:07:50 +0000 Subject: [PATCH 08/17] nix: fix pulse-dune build --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 3fab27e62..a6d1dc40a 100644 --- a/flake.nix +++ b/flake.nix @@ -39,7 +39,7 @@ packages.pulse-dune = pkgs.ocaml-ng.ocamlPackages_4_14.buildDunePackage rec { - pname = "pulse-dune"; + pname = "pulse"; version = "2024.06.02"; sourceRoot = "${src.name}/src/ocaml"; From 939a35fe6a55259d5cfffdda01425a031291cf5e Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 6 Jan 2025 17:10:47 +0000 Subject: [PATCH 09/17] nix: allow extra flags to pulse --- flake.nix | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index a6d1dc40a..caf8820ff 100644 --- a/flake.nix +++ b/flake.nix @@ -125,7 +125,8 @@ --include ./lib/pulse/lib/pulse \ --include ./lib/pulse/lib/pulse/core \ --include ./lib/pulse/lib/pulse/lib \ - --load_cmxs lib/pulse/pulse + --load_cmxs lib/pulse/pulse \ + "$@" ''; } ]; From 38604785152cf5e45f546671c232407fbaf5513d Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 6 Jan 2025 17:11:43 +0000 Subject: [PATCH 10/17] nix: sort inputs, remove systems input --- flake.lock | 16 ---------------- flake.nix | 9 ++++----- 2 files changed, 4 insertions(+), 21 deletions(-) diff --git a/flake.lock b/flake.lock index 93186cc18..9f670bd39 100644 --- a/flake.lock +++ b/flake.lock @@ -325,7 +325,6 @@ "flake-parts": "flake-parts_2", "fstar": "fstar", "nixpkgs": "nixpkgs_4", - "systems": "systems_2", "treefmt-nix": "treefmt-nix" } }, @@ -344,21 +343,6 @@ "type": "github" } }, - "systems_2": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "owner": "nix-systems", - "repo": "default", - "type": "github" - } - }, "treefmt-nix": { "inputs": { "nixpkgs": [ diff --git a/flake.nix b/flake.nix index caf8820ff..9e74c2f6b 100644 --- a/flake.nix +++ b/flake.nix @@ -1,13 +1,12 @@ { inputs = { - nixpkgs.url = "github:cachix/devenv-nixpkgs/rolling"; - systems.url = "github:nix-systems/default"; - fstar.url = "github:FStarLang/FStar/a94456863e3f971a7c63a64aca1a07d2cd9eb9a1"; - devenv.url = "github:cachix/devenv"; devenv.inputs.nixpkgs.follows = "nixpkgs"; + devenv.url = "github:cachix/devenv"; flake-parts.url = "github:hercules-ci/flake-parts"; - treefmt-nix.url = "github:numtide/treefmt-nix"; + fstar.url = "github:FStarLang/FStar/a94456863e3f971a7c63a64aca1a07d2cd9eb9a1"; + nixpkgs.url = "github:cachix/devenv-nixpkgs/rolling"; treefmt-nix.inputs.nixpkgs.follows = "nixpkgs"; + treefmt-nix.url = "github:numtide/treefmt-nix"; }; nixConfig = { From e343420906453fc43bd89e2842d529ffa0c905fa Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Sun, 2 Mar 2025 21:26:52 +0000 Subject: [PATCH 11/17] flake: bump fstar and pulse revision --- flake.lock | 8 ++++---- flake.nix | 50 +++++++++++++++----------------------------------- 2 files changed, 19 insertions(+), 39 deletions(-) diff --git a/flake.lock b/flake.lock index 9f670bd39..5da9db088 100644 --- a/flake.lock +++ b/flake.lock @@ -131,17 +131,17 @@ "nixpkgs": "nixpkgs_3" }, "locked": { - "lastModified": 1714406088, - "narHash": "sha256-v4oEXSb8gVgc1xTU+A8/7VhzPYI5AV1cgYXmPWYaHIg=", + "lastModified": 1739895440, + "narHash": "sha256-QRZdyaHpVZafdk398yQ4LXmSrcqL/cQeYUBj9dwLDlQ=", "owner": "FStarLang", "repo": "FStar", - "rev": "a94456863e3f971a7c63a64aca1a07d2cd9eb9a1", + "rev": "4b3fc11774003a6ff7c09500ecb5f0145ca6d862", "type": "github" }, "original": { "owner": "FStarLang", + "ref": "v2025.02.17", "repo": "FStar", - "rev": "a94456863e3f971a7c63a64aca1a07d2cd9eb9a1", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 9e74c2f6b..9f2bcdea4 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ devenv.inputs.nixpkgs.follows = "nixpkgs"; devenv.url = "github:cachix/devenv"; flake-parts.url = "github:hercules-ci/flake-parts"; - fstar.url = "github:FStarLang/FStar/a94456863e3f971a7c63a64aca1a07d2cd9eb9a1"; + fstar.url = "github:FStarLang/FStar/v2025.02.17"; nixpkgs.url = "github:cachix/devenv-nixpkgs/rolling"; treefmt-nix.inputs.nixpkgs.follows = "nixpkgs"; treefmt-nix.url = "github:numtide/treefmt-nix"; @@ -36,40 +36,21 @@ }; }; - packages.pulse-dune = pkgs.ocaml-ng.ocamlPackages_4_14.buildDunePackage rec { - - pname = "pulse"; - version = "2024.06.02"; - sourceRoot = "${src.name}/src/ocaml"; - - src = pkgs.fetchFromGitHub { - owner = "FStarLang"; - repo = pname; - rev = "v${version}"; - hash = "sha256-jRm21FtPorAW/eQlXbqPyo2Ev0Kdv0evvGmSoPpNE7A="; - }; - - inherit (inputs.fstar.packages.${system}.fstar-dune) nativeBuildInputs; - - buildInputs = inputs.fstar.packages.${system}.fstar-dune.buildInputs ++ [ inputs.fstar.packages.${system}.fstar-dune ]; - - }; - packages.pulse = pkgs.stdenv.mkDerivation rec { pname = "pulse"; - version = "2024.06.02"; + version = "84b3fc39e2ba16059408d4df039d4a03efa85b16"; src = pkgs.fetchFromGitHub { owner = "FStarLang"; repo = pname; - rev = "v${version}"; - hash = "sha256-jRm21FtPorAW/eQlXbqPyo2Ev0Kdv0evvGmSoPpNE7A="; + rev = "${version}"; + hash = "sha256-Cg6z4pbSbPIaU1Jfcw78XVTxqLq5Jt+CajoyxHaeCVo="; }; - inherit (inputs.fstar.packages.${system}.fstar-dune) nativeBuildInputs; + inherit (inputs.fstar.packages.${system}.fstar) nativeBuildInputs; - buildInputs = inputs.fstar.packages.${system}.fstar-dune.buildInputs ++ [ + buildInputs = inputs.fstar.packages.${system}.fstar.buildInputs ++ [ inputs.fstar.packages.${system}.fstar pkgs.which ]; @@ -86,12 +67,11 @@ packages.pulse-exe = pkgs.writeShellScriptBin "pulse.exe" '' exec ${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe "$1" \ --include ${config.packages.pulse}/lib/pulse \ - --include ${config.packages.pulse}/lib/pulse/c \ - --include ${config.packages.pulse}/lib/pulse/core \ + --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/lib/class \ - --include ${config.packages.pulse}/lib/pulse/lib/ml \ - --include ${config.packages.pulse}/lib/pulse/lib/pledge \ + --include ${config.packages.pulse}/lib/pulse/ml \ + --include ${config.packages.pulse}/lib/pulse/syntax_extension \ --load_cmxs pulse \ "$@" ''; @@ -102,12 +82,12 @@ modules = [ { # https://devenv.sh/reference/options/ - packages = with inputs.fstar.packages.${system}; [ z3 ] - ++ fstar-dune.buildInputs - ++ fstar-dune.nativeBuildInputs; + packages = with inputs.fstar.packages.${system}; [ z3 ]; + env.FSTAR_EXE = "${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe"; + env.FSTAR_HOME = "${inputs.fstar.packages.${system}.fstar}/lib/fstar"; + env.PULSE_HOME = "${config.packages.pulse}/lib/pulse"; env.OCAMLPATH = "${inputs.fstar.packages.${system}.fstar}/lib/ocaml/4.14.1/site-lib"; - env.PULSE_HOME = "."; enterShell = '' export PATH="${inputs.fstar.packages.${system}.fstar}/bin:$PATH" ''; @@ -138,7 +118,7 @@ devenv-up = self.devShells.${system}.default.config.procfileScript; devenv-test = self.devShells.${system}.default.config.test; - inherit (inputs.fstar.packages.${system}) fstar fstar-dune; + inherit (inputs.fstar.packages.${system}) fstar; }; }; From 690cddf746efa8c4f573ed82371dc26851a5e019 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 3 Mar 2025 17:15:13 +0000 Subject: [PATCH 12/17] rust: rm Cargo.lock, enable devenv Rust Getting the rust bingings to compile does not seem like a productive approach. Instead, I enable Rust in the devenv so the Makefile can be run interactively. --- flake.nix | 3 +- pulse2rust/src/ocaml/Cargo.lock | 115 -------------------------------- 2 files changed, 1 insertion(+), 117 deletions(-) delete mode 100644 pulse2rust/src/ocaml/Cargo.lock diff --git a/flake.nix b/flake.nix index 9f2bcdea4..f11f0e589 100644 --- a/flake.nix +++ b/flake.nix @@ -92,9 +92,8 @@ export PATH="${inputs.fstar.packages.${system}.fstar}/bin:$PATH" ''; - languages.ocaml = { + languages.rust = { enable = true; - packages = inputs.fstar.packages.${system}.ocamlPackages; }; scripts.pulse.exec = '' diff --git a/pulse2rust/src/ocaml/Cargo.lock b/pulse2rust/src/ocaml/Cargo.lock deleted file mode 100644 index 724c43893..000000000 --- a/pulse2rust/src/ocaml/Cargo.lock +++ /dev/null @@ -1,115 +0,0 @@ -# This file is automatically @generated by Cargo. -# It is not intended for manual editing. -version = 3 - -[[package]] -name = "cc" -version = "1.2.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "27f657647bcff5394bf56c7317665bbf790a137a50eaaa5c6bfbb9e27a518f2d" -dependencies = [ - "shlex", -] - -[[package]] -name = "cty" -version = "0.2.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b365fabc795046672053e29c954733ec3b05e4be654ab130fe8f1f94d7051f35" - -[[package]] -name = "ocaml-boxroot-sys" -version = "0.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5186393bfbee4ce2bc5bbb82beafb77e85c1d0a557e3cfc8c8a0d63d7845fed5" -dependencies = [ - "cc", -] - -[[package]] -name = "ocaml-interop" -version = "0.9.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ce6dfec8cfe7907ee7c62a853f849861f05747f3514126bfdb7c0c842513a9e" -dependencies = [ - "ocaml-boxroot-sys", - "ocaml-sys", - "static_assertions", -] - -[[package]] -name = "ocaml-sys" -version = "0.22.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "73ec6ca7d41458442627435afb8f4671e83fd642e8a560171d671a1f679aa3cf" -dependencies = [ - "cty", -] - -[[package]] -name = "prettyplease" -version = "0.2.25" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "64d1ec885c64d0457d564db4ec299b2dae3f9c02808b8ad9c3a089c591b18033" -dependencies = [ - "proc-macro2", - "syn", -] - -[[package]] -name = "proc-macro2" -version = "1.0.92" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0" -dependencies = [ - "unicode-ident", -] - -[[package]] -name = "quote" -version = "1.0.37" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" -dependencies = [ - "proc-macro2", -] - -[[package]] -name = "rustast_bindings" -version = "0.1.0" -dependencies = [ - "ocaml-interop", - "prettyplease", - "proc-macro2", - "quote", - "syn", -] - -[[package]] -name = "shlex" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" - -[[package]] -name = "static_assertions" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" - -[[package]] -name = "syn" -version = "2.0.90" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "unicode-ident" -version = "1.0.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83" From bc780dd836d4dcd602870611c84c3e2025300ac7 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Mon, 3 Mar 2025 17:17:36 +0000 Subject: [PATCH 13/17] flake: remove unused stuff, nits --- flake.nix | 21 +-------------------- 1 file changed, 1 insertion(+), 20 deletions(-) diff --git a/flake.nix b/flake.nix index f11f0e589..4f076be61 100644 --- a/flake.nix +++ b/flake.nix @@ -16,7 +16,7 @@ outputs = { self, ... }@inputs: - inputs.flake-parts.lib.mkFlake { inherit inputs; } rec { + inputs.flake-parts.lib.mkFlake { inherit inputs; } { systems = inputs.nixpkgs.lib.systems.flakeExposed; imports = [ @@ -40,7 +40,6 @@ pname = "pulse"; version = "84b3fc39e2ba16059408d4df039d4a03efa85b16"; - src = pkgs.fetchFromGitHub { owner = "FStarLang"; repo = pname; @@ -49,7 +48,6 @@ }; inherit (inputs.fstar.packages.${system}.fstar) nativeBuildInputs; - buildInputs = inputs.fstar.packages.${system}.fstar.buildInputs ++ [ inputs.fstar.packages.${system}.fstar pkgs.which @@ -82,30 +80,13 @@ modules = [ { # https://devenv.sh/reference/options/ - packages = with inputs.fstar.packages.${system}; [ z3 ]; - env.FSTAR_EXE = "${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe"; env.FSTAR_HOME = "${inputs.fstar.packages.${system}.fstar}/lib/fstar"; env.PULSE_HOME = "${config.packages.pulse}/lib/pulse"; - env.OCAMLPATH = "${inputs.fstar.packages.${system}.fstar}/lib/ocaml/4.14.1/site-lib"; - enterShell = '' - export PATH="${inputs.fstar.packages.${system}.fstar}/bin:$PATH" - ''; languages.rust = { enable = true; }; - - scripts.pulse.exec = '' - fstar.exe $1 \ - --include ./lib/pulse/lib/class \ - --include ./lib/pulse/lib/pledge \ - --include ./lib/pulse/lib/pulse \ - --include ./lib/pulse/lib/pulse/core \ - --include ./lib/pulse/lib/pulse/lib \ - --load_cmxs lib/pulse/pulse \ - "$@" - ''; } ]; }; From 296b0c0b4b9a48733b6ee2b8dffc2cdb77abd91c Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Tue, 4 Mar 2025 14:22:45 +0000 Subject: [PATCH 14/17] pulse2rust: init on main --- flake.nix | 62 +++++++++++++++++ pulse2rust/src/ocaml/Cargo.lock | 115 ++++++++++++++++++++++++++++++++ 2 files changed, 177 insertions(+) create mode 100644 pulse2rust/src/ocaml/Cargo.lock diff --git a/flake.nix b/flake.nix index 4f076be61..60e8a346a 100644 --- a/flake.nix +++ b/flake.nix @@ -74,6 +74,68 @@ "$@" ''; + packages.rustast-bindings = pkgs.rustPlatform.buildRustPackage rec { + inherit (config.packages.pulse) version src; + inherit (inputs.fstar.packages.${system}.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 { + pname = "extract"; + inherit (config.packages.pulse) version; + src = pkgs.fetchFromGitHub { + owner = "FStarLang"; + repo = "pulse"; + rev = "42842b823c45f83376b65bc10ffa803ad6f21dc4"; + hash = "sha256-CRlrfiDXoSn9s0tiU4dunsUsUu00jb8U9/QApfu+Qtw="; + }; + sourceRoot = "source/pulse2rust/src"; + buildInputs = [ + inputs.fstar.packages.${system}.fstar + pkgs.which + ]; + PATH = "${inputs.fstar.packages.${system}.fstar}/bin:$PATH"; + + installPhase = '' + mkdir -p $out/ocaml/generated + cp -r ocaml/generated $out/ocaml + ''; + }; + + packages.pulse2rust = inputs.fstar.inputs.nixpkgs.legacyPackages.${system}.ocaml-ng.ocamlPackages_4_14.buildDunePackage rec { + inherit (config.packages.pulse) version src; + pname = "main"; + sourceRoot = "${src.name}/pulse2rust/src/ocaml"; + + nativeBuildInputs = inputs.fstar.packages.${system}.fstar.nativeBuildInputs ++ [ inputs.fstar.packages.${system}.fstar ]; + buildInputs = inputs.fstar.packages.${system}.fstar.buildInputs ++ [ inputs.fstar.packages.${system}.fstar ]; + + buildPhase = '' + eval $(${inputs.fstar.packages.${system}.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"; + }; + devShells = { default = inputs.devenv.lib.mkShell { inherit inputs pkgs; diff --git a/pulse2rust/src/ocaml/Cargo.lock b/pulse2rust/src/ocaml/Cargo.lock new file mode 100644 index 000000000..c76e9cb84 --- /dev/null +++ b/pulse2rust/src/ocaml/Cargo.lock @@ -0,0 +1,115 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "cc" +version = "1.2.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "be714c154be609ec7f5dad223a33bf1482fff90472de28f7362806e6d4832b8c" +dependencies = [ + "shlex", +] + +[[package]] +name = "cty" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b365fabc795046672053e29c954733ec3b05e4be654ab130fe8f1f94d7051f35" + +[[package]] +name = "ocaml-boxroot-sys" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5186393bfbee4ce2bc5bbb82beafb77e85c1d0a557e3cfc8c8a0d63d7845fed5" +dependencies = [ + "cc", +] + +[[package]] +name = "ocaml-interop" +version = "0.9.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ce6dfec8cfe7907ee7c62a853f849861f05747f3514126bfdb7c0c842513a9e" +dependencies = [ + "ocaml-boxroot-sys", + "ocaml-sys", + "static_assertions", +] + +[[package]] +name = "ocaml-sys" +version = "0.22.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73ec6ca7d41458442627435afb8f4671e83fd642e8a560171d671a1f679aa3cf" +dependencies = [ + "cty", +] + +[[package]] +name = "prettyplease" +version = "0.2.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6924ced06e1f7dfe3fa48d57b9f74f55d8915f5036121bef647ef4b204895fac" +dependencies = [ + "proc-macro2", + "syn", +] + +[[package]] +name = "proc-macro2" +version = "1.0.94" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a31971752e70b8b2686d7e46ec17fb38dad4051d94024c88df49b667caea9c84" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.39" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c1f1914ce909e1658d9907913b4b91947430c7d9be598b15a1912935b8c04801" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rustast_bindings" +version = "0.1.0" +dependencies = [ + "ocaml-interop", + "prettyplease", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "static_assertions" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" + +[[package]] +name = "syn" +version = "2.0.99" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e02e925281e18ffd9d640e234264753c43edc62d64b2d4cf898f1bc5e75f3fc2" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "00e2473a93778eb0bad35909dff6a10d28e63f792f16ed15e404fca9d5eeedbe" From e326225085bde8f32b40d77f7914635c599fafff Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Tue, 11 Mar 2025 14:13:45 +0000 Subject: [PATCH 15/17] flake: rm treefmt-nix --- flake.lock | 23 +---------------------- flake.nix | 17 +---------------- 2 files changed, 2 insertions(+), 38 deletions(-) diff --git a/flake.lock b/flake.lock index 5da9db088..74c516ea7 100644 --- a/flake.lock +++ b/flake.lock @@ -324,8 +324,7 @@ "devenv": "devenv", "flake-parts": "flake-parts_2", "fstar": "fstar", - "nixpkgs": "nixpkgs_4", - "treefmt-nix": "treefmt-nix" + "nixpkgs": "nixpkgs_4" } }, "systems": { @@ -342,26 +341,6 @@ "repo": "default", "type": "github" } - }, - "treefmt-nix": { - "inputs": { - "nixpkgs": [ - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1732643199, - "narHash": "sha256-uI7TXEb231o8dkwB5AUCecx3AQtosRmL6hKgnckvjps=", - "owner": "numtide", - "repo": "treefmt-nix", - "rev": "84637a7ab04179bdc42aa8fd0af1909fba76ad0c", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "treefmt-nix", - "type": "github" - } } }, "root": "root", diff --git a/flake.nix b/flake.nix index 60e8a346a..9b41a649a 100644 --- a/flake.nix +++ b/flake.nix @@ -5,8 +5,6 @@ flake-parts.url = "github:hercules-ci/flake-parts"; fstar.url = "github:FStarLang/FStar/v2025.02.17"; nixpkgs.url = "github:cachix/devenv-nixpkgs/rolling"; - treefmt-nix.inputs.nixpkgs.follows = "nixpkgs"; - treefmt-nix.url = "github:numtide/treefmt-nix"; }; nixConfig = { @@ -19,23 +17,10 @@ inputs.flake-parts.lib.mkFlake { inherit inputs; } { systems = inputs.nixpkgs.lib.systems.flakeExposed; - imports = [ - inputs.treefmt-nix.flakeModule - ]; + imports = [ ]; perSystem = { pkgs, config, system, ... }: { - treefmt.config = { - projectRootFile = "flake.nix"; - flakeFormatter = true; - flakeCheck = true; - programs = { - nixpkgs-fmt.enable = true; - deadnix.enable = true; - statix.enable = true; - }; - }; - packages.pulse = pkgs.stdenv.mkDerivation rec { pname = "pulse"; From 09173da8895039285f2f6a5e1b4669129998e027 Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Thu, 1 May 2025 14:37:47 +0100 Subject: [PATCH 16/17] flake: rm devenv, update fstar --- .envrc | 11 +-- flake.lock | 277 ++++++----------------------------------------------- flake.nix | 68 ++++--------- 3 files changed, 47 insertions(+), 309 deletions(-) diff --git a/.envrc b/.envrc index f63cb7a1f..3550a30f2 100644 --- a/.envrc +++ b/.envrc @@ -1,10 +1 @@ -if ! has nix_direnv_version || ! nix_direnv_version 2.2.1; then - source_url "https://raw.githubusercontent.com/nix-community/nix-direnv/2.2.1/direnvrc" "sha256-zelF0vLbEl5uaqrfIzbgNzJWGmLzCmYAkInj/LNxvKs=" -fi - -watch_file flake.nix -watch_file flake.lock -if ! use flake . --no-pure-eval --accept-flake-config -then - echo "devenv could not be built. The devenv environment was not loaded. Make the necessary changes to devenv.nix and hit enter to try again." >&2 -fi +use flake diff --git a/flake.lock b/flake.lock index 74c516ea7..3a0045f35 100644 --- a/flake.lock +++ b/flake.lock @@ -1,105 +1,15 @@ { "nodes": { - "cachix": { - "inputs": { - "devenv": [ - "devenv" - ], - "flake-compat": [ - "devenv" - ], - "git-hooks": [ - "devenv" - ], - "nixpkgs": "nixpkgs" - }, - "locked": { - "lastModified": 1728672398, - "narHash": "sha256-KxuGSoVUFnQLB2ZcYODW7AVPAh9JqRlD5BrfsC/Q4qs=", - "owner": "cachix", - "repo": "cachix", - "rev": "aac51f698309fd0f381149214b7eee213c66ef0a", - "type": "github" - }, - "original": { - "owner": "cachix", - "ref": "latest", - "repo": "cachix", - "type": "github" - } - }, - "devenv": { - "inputs": { - "cachix": "cachix", - "flake-compat": "flake-compat", - "git-hooks": "git-hooks", - "nix": "nix", - "nixpkgs": [ - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1732585607, - "narHash": "sha256-6ffeaSMuaL326f7KrCeScpSJtdHsFKS9gPrsSZkndvU=", - "owner": "cachix", - "repo": "devenv", - "rev": "a520f05c40ebecaf5e17064b27e28ba8e70c49fb", - "type": "github" - }, - "original": { - "owner": "cachix", - "repo": "devenv", - "type": "github" - } - }, - "flake-compat": { - "flake": false, - "locked": { - "lastModified": 1696426674, - "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", - "type": "github" - }, - "original": { - "owner": "edolstra", - "repo": "flake-compat", - "type": "github" - } - }, "flake-parts": { - "inputs": { - "nixpkgs-lib": [ - "devenv", - "nix", - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1712014858, - "narHash": "sha256-sB4SWl2lX95bExY2gMFG5HIzvva5AVMJd4Igm+GpZNw=", - "owner": "hercules-ci", - "repo": "flake-parts", - "rev": "9126214d0a59633752a136528f5f3b9aa8565b7d", - "type": "github" - }, - "original": { - "owner": "hercules-ci", - "repo": "flake-parts", - "type": "github" - } - }, - "flake-parts_2": { "inputs": { "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1730504689, - "narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=", + "lastModified": 1743550720, + "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "506278e768c2a08bec68eb62932193e341f55c90", + "rev": "c621e8422220273271f52058f618c94e405bb0f5", "type": "github" }, "original": { @@ -128,203 +38,74 @@ "fstar": { "inputs": { "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs_3" + "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1739895440, - "narHash": "sha256-QRZdyaHpVZafdk398yQ4LXmSrcqL/cQeYUBj9dwLDlQ=", + "lastModified": 1742959035, + "narHash": "sha256-PhjfThXF6fJlFHtNEURG4igCnM6VegWODypmRvnZPdA=", "owner": "FStarLang", "repo": "FStar", - "rev": "4b3fc11774003a6ff7c09500ecb5f0145ca6d862", + "rev": "71d8221589d4d438af3706d89cb653cf53e18aab", "type": "github" }, "original": { "owner": "FStarLang", - "ref": "v2025.02.17", + "ref": "v2025.03.25", "repo": "FStar", "type": "github" } }, - "git-hooks": { - "inputs": { - "flake-compat": [ - "devenv" - ], - "gitignore": "gitignore", - "nixpkgs": [ - "devenv", - "nixpkgs" - ], - "nixpkgs-stable": [ - "devenv" - ] - }, - "locked": { - "lastModified": 1730302582, - "narHash": "sha256-W1MIJpADXQCgosJZT8qBYLRuZls2KSiKdpnTVdKBuvU=", - "owner": "cachix", - "repo": "git-hooks.nix", - "rev": "af8a16fe5c264f5e9e18bcee2859b40a656876cf", - "type": "github" - }, - "original": { - "owner": "cachix", - "repo": "git-hooks.nix", - "type": "github" - } - }, - "gitignore": { - "inputs": { - "nixpkgs": [ - "devenv", - "git-hooks", - "nixpkgs" - ] - }, - "locked": { - "lastModified": 1709087332, - "narHash": "sha256-HG2cCnktfHsKV0s4XW83gU3F57gaTljL9KNSuG6bnQs=", - "owner": "hercules-ci", - "repo": "gitignore.nix", - "rev": "637db329424fd7e46cf4185293b9cc8c88c95394", - "type": "github" - }, - "original": { - "owner": "hercules-ci", - "repo": "gitignore.nix", - "type": "github" - } - }, - "libgit2": { - "flake": false, - "locked": { - "lastModified": 1697646580, - "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=", - "owner": "libgit2", - "repo": "libgit2", - "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5", - "type": "github" - }, - "original": { - "owner": "libgit2", - "repo": "libgit2", - "type": "github" - } - }, - "nix": { - "inputs": { - "flake-compat": [ - "devenv" - ], - "flake-parts": "flake-parts", - "libgit2": "libgit2", - "nixpkgs": "nixpkgs_2", - "nixpkgs-23-11": [ - "devenv" - ], - "nixpkgs-regression": [ - "devenv" - ], - "pre-commit-hooks": [ - "devenv" - ] - }, - "locked": { - "lastModified": 1727438425, - "narHash": "sha256-X8ES7I1cfNhR9oKp06F6ir4Np70WGZU5sfCOuNBEwMg=", - "owner": "domenkozar", - "repo": "nix", - "rev": "f6c5ae4c1b2e411e6b1e6a8181cc84363d6a7546", - "type": "github" - }, - "original": { - "owner": "domenkozar", - "ref": "devenv-2.24", - "repo": "nix", - "type": "github" - } - }, "nixpkgs": { "locked": { - "lastModified": 1730531603, - "narHash": "sha256-Dqg6si5CqIzm87sp57j5nTaeBbWhHFaVyG7V6L8k3lY=", + "lastModified": 1743588408, + "narHash": "sha256-WRZyK13yucGjwNBMOGjU8ljRJ8FYFv8MBru/bXqZUn0=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "7ffd9ae656aec493492b44d0ddfb28e79a1ea25d", + "rev": "88efe689298b1863db0310c0a22b3ebb4d04fbc3", "type": "github" }, "original": { - "owner": "NixOS", + "id": "nixpkgs", "ref": "nixos-unstable", - "repo": "nixpkgs", - "type": "github" + "type": "indirect" } }, "nixpkgs-lib": { "locked": { - "lastModified": 1730504152, - "narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=", - "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz" - }, - "original": { - "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz" - } - }, - "nixpkgs_2": { - "locked": { - "lastModified": 1717432640, - "narHash": "sha256-+f9c4/ZX5MWDOuB1rKoWj+lBNm0z0rs4CK47HBLxy1o=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "88269ab3044128b7c2f4c7d68448b2fb50456870", + "lastModified": 1743296961, + "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa", "type": "github" }, "original": { - "owner": "NixOS", - "ref": "release-24.05", - "repo": "nixpkgs", + "owner": "nix-community", + "repo": "nixpkgs.lib", "type": "github" } }, - "nixpkgs_3": { + "nixpkgs_2": { "locked": { - "lastModified": 1693158576, - "narHash": "sha256-aRTTXkYvhXosGx535iAFUaoFboUrZSYb1Ooih/auGp0=", - "owner": "NixOS", + "lastModified": 1745930157, + "narHash": "sha256-y3h3NLnzRSiUkYpnfvnS669zWZLoqqI6NprtLQ+5dck=", + "owner": "nixos", "repo": "nixpkgs", - "rev": "a999c1cc0c9eb2095729d5aa03e0d8f7ed256780", + "rev": "46e634be05ce9dc6d4db8e664515ba10b78151ae", "type": "github" }, "original": { - "id": "nixpkgs", + "owner": "nixos", "ref": "nixos-unstable", - "type": "indirect" - } - }, - "nixpkgs_4": { - "locked": { - "lastModified": 1716977621, - "narHash": "sha256-Q1UQzYcMJH4RscmpTkjlgqQDX5yi1tZL0O345Ri6vXQ=", - "owner": "cachix", - "repo": "devenv-nixpkgs", - "rev": "4267e705586473d3e5c8d50299e71503f16a6fb6", - "type": "github" - }, - "original": { - "owner": "cachix", - "ref": "rolling", - "repo": "devenv-nixpkgs", + "repo": "nixpkgs", "type": "github" } }, "root": { "inputs": { - "devenv": "devenv", - "flake-parts": "flake-parts_2", + "flake-parts": "flake-parts", "fstar": "fstar", - "nixpkgs": "nixpkgs_4" + "nixpkgs": "nixpkgs_2" } }, "systems": { diff --git a/flake.nix b/flake.nix index 9b41a649a..c6db260fa 100644 --- a/flake.nix +++ b/flake.nix @@ -1,18 +1,11 @@ { inputs = { - devenv.inputs.nixpkgs.follows = "nixpkgs"; - devenv.url = "github:cachix/devenv"; flake-parts.url = "github:hercules-ci/flake-parts"; - fstar.url = "github:FStarLang/FStar/v2025.02.17"; - nixpkgs.url = "github:cachix/devenv-nixpkgs/rolling"; + fstar.url = "github:FStarLang/FStar/v2025.03.25"; + nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; }; - nixConfig = { - extra-trusted-public-keys = "devenv.cachix.org-1:w1cLUi8dv3hnoSPGAuibQv+f9TZLr6cv/Hm9XgU50cw="; - extra-substituters = "https://devenv.cachix.org"; - }; - - outputs = { self, ... }@inputs: + outputs = { ... }@inputs: inputs.flake-parts.lib.mkFlake { inherit inputs; } { @@ -24,20 +17,20 @@ packages.pulse = pkgs.stdenv.mkDerivation rec { pname = "pulse"; - version = "84b3fc39e2ba16059408d4df039d4a03efa85b16"; + version = "9a03472d2c366bde5f7b0497bf3356dd445ce207"; src = pkgs.fetchFromGitHub { owner = "FStarLang"; repo = pname; rev = "${version}"; - hash = "sha256-Cg6z4pbSbPIaU1Jfcw78XVTxqLq5Jt+CajoyxHaeCVo="; + hash = "sha256-YgWxnX+gCVYx+CCIuprDYKewyEaSekqAilB96eyq+fk="; }; - inherit (inputs.fstar.packages.${system}.fstar) nativeBuildInputs; - buildInputs = inputs.fstar.packages.${system}.fstar.buildInputs ++ [ - inputs.fstar.packages.${system}.fstar + inherit (pkgs.fstar) nativeBuildInputs; + buildInputs = pkgs.fstar.buildInputs ++ [ + pkgs.fstar pkgs.which ]; - PATH = "${inputs.fstar.packages.${system}.fstar}/bin:$PATH"; + PATH = "${pkgs.fstar}/bin:$PATH"; enableParallelBuilding = true; @@ -48,7 +41,7 @@ }; packages.pulse-exe = pkgs.writeShellScriptBin "pulse.exe" '' - exec ${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe "$1" \ + 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 \ @@ -61,7 +54,7 @@ packages.rustast-bindings = pkgs.rustPlatform.buildRustPackage rec { inherit (config.packages.pulse) version src; - inherit (inputs.fstar.packages.${system}.fstar) nativeBuildInputs; + inherit (pkgs.fstar) nativeBuildInputs; pname = "rustast-bindings"; sourceRoot = "${src.name}/pulse2rust/src/ocaml"; cargoLock = { @@ -83,10 +76,10 @@ }; sourceRoot = "source/pulse2rust/src"; buildInputs = [ - inputs.fstar.packages.${system}.fstar + pkgs.fstar pkgs.which ]; - PATH = "${inputs.fstar.packages.${system}.fstar}/bin:$PATH"; + PATH = "${pkgs.fstar}/bin:$PATH"; installPhase = '' mkdir -p $out/ocaml/generated @@ -99,11 +92,11 @@ pname = "main"; sourceRoot = "${src.name}/pulse2rust/src/ocaml"; - nativeBuildInputs = inputs.fstar.packages.${system}.fstar.nativeBuildInputs ++ [ inputs.fstar.packages.${system}.fstar ]; - buildInputs = inputs.fstar.packages.${system}.fstar.buildInputs ++ [ inputs.fstar.packages.${system}.fstar ]; + nativeBuildInputs = pkgs.fstar.nativeBuildInputs ++ [ pkgs.fstar ]; + buildInputs = pkgs.fstar.buildInputs ++ [ pkgs.fstar ]; buildPhase = '' - eval $(${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe --ocamlenv) + eval $(${pkgs.fstar}/bin/fstar.exe --ocamlenv) mkdir -p $out/bin dune build main.exe --build-dir=$out/bin ''; @@ -121,33 +114,6 @@ meta.mainProgram = "default/ocaml/main.exe"; }; - devShells = { - default = inputs.devenv.lib.mkShell { - inherit inputs pkgs; - modules = [ - { - # https://devenv.sh/reference/options/ - env.FSTAR_EXE = "${inputs.fstar.packages.${system}.fstar}/bin/fstar.exe"; - env.FSTAR_HOME = "${inputs.fstar.packages.${system}.fstar}/lib/fstar"; - env.PULSE_HOME = "${config.packages.pulse}/lib/pulse"; - - languages.rust = { - enable = true; - }; - } - ]; - }; - }; - - packages = { - default = config.packages.pulse; - - devenv-up = self.devShells.${system}.default.config.procfileScript; - devenv-test = self.devShells.${system}.default.config.test; - - inherit (inputs.fstar.packages.${system}) fstar; - }; - }; }; -} +} \ No newline at end of file From 65e317e666c7a4af1560198c3fd397e0a25a40ae Mon Sep 17 00:00:00 2001 From: Juuso Haavisto Date: Thu, 1 May 2025 14:41:17 +0100 Subject: [PATCH 17/17] flake: vendor fstar, packages.default -> pulse --- flake.nix | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/flake.nix b/flake.nix index c6db260fa..4f657c547 100644 --- a/flake.nix +++ b/flake.nix @@ -114,6 +114,10 @@ meta.mainProgram = "default/ocaml/main.exe"; }; + packages.fstar = pkgs.fstar; + + packages.default = config.packages.pulse; + }; }; } \ No newline at end of file