From 5727c481263d189f937f03720fa06c79a53a3f5d Mon Sep 17 00:00:00 2001 From: jlh <48520973+Jlh18@users.noreply.github.com> Date: Thu, 25 Nov 2021 13:30:00 +0000 Subject: [PATCH 1/5] fixed link to site --- README.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.rst b/README.rst index 275324c..9502660 100644 --- a/README.rst +++ b/README.rst @@ -13,4 +13,4 @@ This page will help you get the Game working for you. For instructions on how to get started with the HoTT Game, visit -`this page `_. +`this page `_. From d1645f6c7defb60628e2d7da9f2ff6ffc7dc1ccb Mon Sep 17 00:00:00 2001 From: jlh <48520973+Jlh18@users.noreply.github.com> Date: Thu, 25 Nov 2021 13:47:36 +0000 Subject: [PATCH 2/5] Update README.rst --- README.rst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.rst b/README.rst index 9502660..f88f9e0 100644 --- a/README.rst +++ b/README.rst @@ -14,3 +14,8 @@ This page will help you get the Game working for you. For instructions on how to get started with the HoTT Game, visit `this page `_. + +The creators of this game are +`Joseph Hua `_, +`Ken Lee `_, +and Bendit Chan. From 7c525d69c10714be31c74b51fc10dddc27b649b7 Mon Sep 17 00:00:00 2001 From: jlh <48520973+Jlh18@users.noreply.github.com> Date: Thu, 25 Nov 2021 13:53:48 +0000 Subject: [PATCH 3/5] Update README.rst --- README.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.rst b/README.rst index f88f9e0..b024221 100644 --- a/README.rst +++ b/README.rst @@ -18,4 +18,4 @@ visit The creators of this game are `Joseph Hua `_, `Ken Lee `_, -and Bendit Chan. +and `Bendit Chan `_. From 62e292869303f0727da336740aed65f58091653a Mon Sep 17 00:00:00 2001 From: o1lo01ol1o Date: Thu, 2 Dec 2021 10:54:30 +0000 Subject: [PATCH 4/5] Create shell.nix --- shell.nix | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 shell.nix diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..39aa1e6 --- /dev/null +++ b/shell.nix @@ -0,0 +1,17 @@ +let + emacsOverlay = (import (builtins.fetchGit { + url = "https://github.com/nix-community/emacs-overlay.git"; + ref = "master"; + rev = "bfc8f6edcb7bcf3cf24e4a7199b3f6fed96aaecf"; # change the revision + })); + pkgs = import {overlays = [emacsOverlay] ;}; +in with pkgs; +mkShell { + buildInputs = [ + pkgs.emacs + (agda.withPackages (ps: [ + ps.standard-library + ps.cubical + ])) + ]; +} \ No newline at end of file From 97030e9c158198fa3975308218d4d2063ed48334 Mon Sep 17 00:00:00 2001 From: o1lo01ol1o Date: Thu, 2 Dec 2021 11:25:31 +0000 Subject: [PATCH 5/5] Add nix install instructions --- Installation/Mac.md | 52 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/Installation/Mac.md b/Installation/Mac.md index b328fa6..6f92e89 100644 --- a/Installation/Mac.md +++ b/Installation/Mac.md @@ -40,3 +40,55 @@ git clone https://github.com/hlissner/doom-emacs ~/.emacs.d export PATH=”$HOME/.emacs.d/bin:$PATH” ``` + +Installing TheHoTTGame on MacOS with Nix +======================================== + +`Nixpkgs` maintains a set of `Agda` libraries that can be added to a derivation managed by the nix package manager. See [here](https://github.com/NixOS/nixpkgs/blob/master/doc/languages-frameworks/agda.section.md) for details. `shell.nix` in this project contains a derivation that will add emacs, agda, the agda standard library, and cubical agda to your local nix store and subsequently to a local shell environment by adding these locations to your PATH. + +However, because user configurations for emacs are mutable, it will not (easily) manage your (emacs configuration) dot-files, so we will use the underlying `emacs` provided by `nixpkgs` but install `doom emacs` normally in your local user's environment. + + +Install nix using `curl`: https://nixos.org/download.html + +In the base directory, +```bash +nix-shell +``` + +To enter a nix shell with the above packages loaded on your `PATH`. This shell is defined by package set in `shell.nix`; after installation, to use agda libraries, you will need to use _this_ shell (or another configured similarly) to load the requisite packages onto the `PATH` so that they can be found. + +[Then install `doom emacs`](https://github.com/hlissner/doom-emacs) using the `nix-shell` provided `emacs`: + +```bash +git clone --depth 1 https://github.com/hlissner/doom-emacs ~/.emacs.d +~/.emacs.d/bin/doom install +``` + +You'll probably want to answer "yes" to the options unless you know better. + +[Add the doom utility to your path](https://github.com/hlissner/doom-emacs/blob/develop/docs/getting_started.org#the-bindoom-utility): + +> I recommend you add ~/.emacs.d/bin to your PATH so you can call doom directly and from anywhere. Accomplish this by adding this to your .bashrc or .zshrc file: ~export PATH=”$HOME/.emacs.d/bin:$PATH”~ + +Add `agda` support to `doom` by editing your `~/.doom.d/config.el`. In the languages section `:lang`, you'll see `;; agda`. Replace it with `(agda +local)` to tell doom to use the `agda-mode` version specified by the local environment. + +Once the file is saved, sync `doom` from within the nix-shell that was loaded above: + +```bash +doom sync +``` + +You can now load the agda source code in this by starting doom from the nix-shell: +```bash +doom run . +``` + +open the file at `0Trinitarianism/Quest0.agda` + +and tell `agda-mode` to load and check it by pressing `SPC m l` (`space`, `m` and `l`, in that order.) If everything is configured correctly, you should get nice colors and any `{!!}`s will become interactive holes to fill. + + + + +