❄️ Add building with Nix as an option

.gitignore

@@ -127,3 +127,6 @@ setup.log
 
 # Local OPAM switch
 _opam/
+
+# for Nix
+result/

README.md

@@ -11,11 +11,16 @@ by Gratzer, Sterling, and Birkedal. Code has been incorporated from
 [redtt](https://www.github.com/RedPRL/redtt), implemented by Sterling and
 Favonia.
 
-## building
+A small collection of example programs is contained in the `test/` directory.
+See `test/README.md` for a brief description of each program's purpose.
+
+## Building
 
 cooltt has been built with OCaml 4.13.0 with [opam
-2.0.8](https://opam.ocaml.org/). If you are running an older version of OCaml,
-try executing the following command:
+2.0.8](https://opam.ocaml.org/). 
+
+### With OPAM
+If you are running an older version of OCaml, try executing the following command:
 
 ```
 $ opam switch create 4.13.0
@@ -40,9 +45,24 @@ $ make upgrade-pins                     # update and upgrade dependencies in act
 $ dune exec cooltt                      # from the `cooltt` top-level directory
 ```
 
+### With Nix
+First, you'll need the [Nix package manager](https://nixos.org/download.html), and then
+you'll need to [install or enable flakes](https://nixos.wiki/wiki/Flakes).
 
-A small collection of example programs is contained in the `test/` directory.
-See `test/README.md` for a brief description of each program's purpose.
+Then, cooltt can be built with the command
+```
+nix build --impure
+```
+to put a binary `cooltt` in `result/bin/cooltt`. This is good for if you just want to build
+and play around with cooltt.
+
+If you're working on cooltt, you can enter a development shell with an OCaml compiler, dune,
+and other tools with
+```
+nix develop --impure
+```
+and then build as in the [with OPAM](https://github.com/RedPRL/cooltt/#with-opam=) section 
+above.
 
 ## Acknowledgments
 

cooltt.opam

@@ -26,7 +26,7 @@ depends: [
 ]
 pin-depends: [
   [ "kado.~dev" "git+https://github.com/RedPRL/kado" ]
-  [ "bantorra.0.1.0" "git+https://github.com/RedPRL/bantorra#0.1.0" ]
+  [ "bantorra.0.1.0" "git+https://github.com/RedPRL/bantorra#1e78633d9a2ef7104552a24585bb8bea36d4117b" ]
 ]
 build: [
   ["dune" "build" "-p" name "-j" jobs]

flake.nix

@@ -0,0 +1,36 @@
+{
+  description = "Experimental implementation of Cartesian cubical type theory";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-22.05";
+    flake-utils.url = "github:numtide/flake-utils";
+
+    opam-repository = {
+      url = "github:ocaml/opam-repository";
+      flake = false;
+    };
+
+    opam-nix = {
+      url = "github:tweag/opam-nix";
+      inputs.nixpkgs.follows = "nixpkgs";
+      inputs.flake-utils.follows = "flake-utils";
+      inputs.opam-repository.follows = "opam-repository";
+    };
+  };
+
+  outputs = { self
+            , flake-utils
+            , opam-nix
+            , nixpkgs
+            , opam-repository
+            }@inputs:
+    flake-utils.lib.eachDefaultSystem (system: {
+      legacyPackages = let
+        on = opam-nix.lib.${system};
+      in on.buildDuneProject { } "cooltt" ./. {
+        ocaml-base-compiler = null;
+      };
+
+      defaultPackage = self.legacyPackages.${system}."cooltt";
+    });
+}