From b63945de40b4201fda13871ad0d8541d9f17af34 Mon Sep 17 00:00:00 2001 From: Calvin Beck Date: Thu, 9 Oct 2025 15:38:35 -0400 Subject: [PATCH] Adding nix flake with nix CI in GitHub actions. --- .envrc | 2 + .github/workflows/nix-build.yml | 21 ++++++ Readme.md | 1 + flake.lock | 111 ++++++++++++++++++++++++++++++++ flake.nix | 104 ++++++++++++++++++++++++++++++ 5 files changed, 239 insertions(+) create mode 100644 .envrc create mode 100644 .github/workflows/nix-build.yml create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..e9e8bb2 --- /dev/null +++ b/.envrc @@ -0,0 +1,2 @@ +use flake +unset COQPATH diff --git a/.github/workflows/nix-build.yml b/.github/workflows/nix-build.yml new file mode 100644 index 0000000..d20b268 --- /dev/null +++ b/.github/workflows/nix-build.yml @@ -0,0 +1,21 @@ +name: "Build ctrees under nix" +on: + pull_request: + push: +jobs: + tests: + strategy: + matrix: + os: + - ubuntu-latest + runs-on: ${{ matrix.os }} + permissions: + id-token: "write" + contents: "read" + steps: + - uses: actions/checkout@v4 + - uses: DeterminateSystems/nix-installer-action@v19 + - uses: DeterminateSystems/magic-nix-cache-action@v13 + - uses: DeterminateSystems/flake-checker-action@v12 + - name: Run nix build + run: nix build . diff --git a/Readme.md b/Readme.md index ac9cb48..a9bb3b7 100644 --- a/Readme.md +++ b/Readme.md @@ -1,5 +1,6 @@ # Choice Trees [![Docker CI](https://github.com/vellvm/ctrees/workflows/Docker%20CI/badge.svg?branch=master)](https://github.com/vellvm/ctrees/actions?query=workflow:"Docker%20CI") +[![Nix](https://github.com/vellvm/ctrees/actions/workflows/nix-build.yml/badge.svg)](https://github.com/vellvm/ctrees/actions/workflows/nix-build.yml) We develop a cousin of Interaction Trees, dubbed _ctrees_ with native support for internal non-determinism. diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..bbc2e75 --- /dev/null +++ b/flake.lock @@ -0,0 +1,111 @@ +{ + "nodes": { + "coinduction-repo": { + "flake": false, + "locked": { + "lastModified": 1758090858, + "narHash": "sha256-S/stL5bpJsJt+bvOg4F2b/WaEt5IDOop3ruBIbde9GI=", + "owner": "damien-pous", + "repo": "coinduction", + "rev": "a88f0f4f170dcb9b24e3d470c76801a765423598", + "type": "github" + }, + "original": { + "owner": "damien-pous", + "repo": "coinduction", + "type": "github" + } + }, + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nix-filter": { + "locked": { + "lastModified": 1757882181, + "narHash": "sha256-+cCxYIh2UNalTz364p+QYmWHs0P+6wDhiWR4jDIKQIU=", + "owner": "numtide", + "repo": "nix-filter", + "rev": "59c44d1909c72441144b93cf0f054be7fe764de5", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "nix-filter", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1762943920, + "narHash": "sha256-ITeH8GBpQTw9457ICZBddQEBjlXMmilML067q0e6vqY=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "91c9a64ce2a84e648d0cf9671274bb9c2fb9ba60", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "relation-algebra-repo": { + "flake": false, + "locked": { + "lastModified": 1758092026, + "narHash": "sha256-RnY+a57KnStACteaT5dKQoCCH0qp7/W+4qoaApIilj0=", + "owner": "damien-pous", + "repo": "relation-algebra", + "rev": "062d5cf9468ce367fe11220b336dff254a51702b", + "type": "github" + }, + "original": { + "owner": "damien-pous", + "repo": "relation-algebra", + "type": "github" + } + }, + "root": { + "inputs": { + "coinduction-repo": "coinduction-repo", + "flake-utils": "flake-utils", + "nix-filter": "nix-filter", + "nixpkgs": "nixpkgs", + "relation-algebra-repo": "relation-algebra-repo" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..0b373de --- /dev/null +++ b/flake.nix @@ -0,0 +1,104 @@ +{ + description = "CTrees: a cousin of Interaction Trees, dubbed Choice Trees, with native support for non-determinism."; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable"; + flake-utils.url = "github:numtide/flake-utils"; + nix-filter.url = "github:numtide/nix-filter"; + coinduction-repo = { + url = "github:damien-pous/coinduction"; + flake = false; + }; + relation-algebra-repo = { + url = "github:damien-pous/relation-algebra"; + flake = false; + }; + }; + + outputs = { self, nixpkgs, flake-utils, nix-filter, coinduction-repo, relation-algebra-repo }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = import nixpkgs { inherit system; }; + lib = pkgs.lib; + rocq = pkgs.rocq-core; + rocqPkgs = pkgs.rocqPackages_9_0; + coqPkgs = pkgs.coqPackages_9_0; + + coinduction = rocqPkgs.callPackage + ( { rocq, stdenv }: + rocqPkgs.mkRocqDerivation { + owner = "damien-pous"; + pname = "coinduction"; + version = "coinduction:master"; + src = coinduction-repo; + + buildInputs = + with rocqPkgs; + with coqPkgs; + with rocq.ocamlPackages; + [ ocaml camlp5 rocq pkgs.coq dune_3 stdlib rocq-core findlib ]; + propagatedBuildInputs = + with rocqPkgs; + with coqPkgs; + with rocq.ocamlPackages; + [ rocq ]; + }) { inherit rocq; } ; + + relation-algebra = rocqPkgs.callPackage + ( { rocq, stdenv }: + rocqPkgs.mkRocqDerivation { + owner = "damien-pous"; + pname = "relation-algebra"; + version = "relation-algebra:master"; + src = relation-algebra-repo; + + buildInputs = + with rocqPkgs; + with coqPkgs; + with rocq.ocamlPackages; + [ ocaml camlp5 rocq pkgs.coq dune_3 stdlib rocq-core findlib ]; + propagatedBuildInputs = + with rocqPkgs; + with coqPkgs; + with rocq.ocamlPackages; + [ rocq ]; + }) { inherit rocq; } ; + in rec { + packages = { + default =rocqPkgs.callPackage + ( { rocq, stdenv }: + rocqPkgs.mkRocqDerivation { + owner = "vellvm"; + pname = "ctrees"; + version = "ctrees:dev"; + opam-name = "coq-ctree"; + useDune = true; + src = ./.; + + buildInputs = + with rocqPkgs; + with coqPkgs; + with rocq.ocamlPackages; + [ ocaml camlp5 rocq pkgs.coq dune_3 ITree coinduction relation-algebra stdlib equations ExtLib zarith findlib ]; + propagatedBuildInputs = [ rocq ]; + + }) { inherit rocq; }; + }; + + defaultPackage = packages.default; + + app.default = flake-utils.lib.mkApp { drv = packages.default; }; + + devShells = { + default = pkgs.mkShell { + inputsFrom = [ packages.default]; + buildInputs = [ ]; + shellHook = '' + unset COQPATH + ''; + }; + }; + + devShell = devShells.default; + }); +}