Nix build + CI

.envrc

@@ -0,0 +1,2 @@
+use flake
+unset COQPATH

.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 .

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.
 

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;
+      });
+}