diff --git a/Installation/Mac.md b/Installation/Mac.md deleted file mode 100644 index 6f92e89..0000000 --- a/Installation/Mac.md +++ /dev/null @@ -1,94 +0,0 @@ -Installing TheHoTTGame on MacOS -=============================== - - -`https://sourceforge.net/projects/git-osx-installer/` -`brew link --overwrite git` -`rm -r .emacs.d` - -`export PATH="/usr/local/bin:$PATH"` -in `.bash_profile` (if old) - -``` -# required dependencies -brew install git ripgrep - -# makes computer use latest git -export PATH=/usr/local/bin:$PATH - -# optional dependencies -brew install coreutils fd - -# Installs clang -xcode-select --install - -# For fonts -brew install fontconfig - -# Installs emacs-mac wth sexy icon and no title bars -brew tap railwaycat/emacsmacport -brew install emacs-mac --with-modules --with-emacs-sexy-icon --with-no-title-bars - -# Make an app link in Applications -ln -s /usr/local/opt/emacs-mac/Emacs.app /Applications/Emacs.app - -# doom emacs -git clone https://github.com/hlissner/doom-emacs ~/.emacs.d -~/.emacs.d/bin/doom install - -# so that you can use 'doom' anywhere -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. - - - - - diff --git a/Installation/Windows.md b/Installation/Windows.md deleted file mode 100644 index e05b63d..0000000 --- a/Installation/Windows.md +++ /dev/null @@ -1,196 +0,0 @@ -How to Install the HoTT Game on Windows -======================================= - -## Prerequisites - -MUST USE POWERSHELL AS ADMIN -- chocolatey: follow instructions on - [their page](https://chocolatey.org/install) -- In (admin) powershell do (via chocolatey, cabal) - - `choco install ghc` - - `choco install cabal` - - `cabal install happy` - - `cabal install alex` - - - - - - -## Doom Emacs -Get doom emacs following instructions made [here]( -earvingad.github.io/posts/doom_emacs_windows/ -) - - - - - - - - - - - - - - - -## Development Version of Agda - -POWERSHALL IN LOCAL -- Directly clone the repo for development version. - _You can choose where to put this_. - ``` - git clone https://github.com/agda/agda.git - ``` -- We need to install `make` for windows. Easiest via cabal. - ``` - cabal install make - ``` -- Go into folder of agda repo then do - ``` - cabal update - make install - ``` -- Agda should be finished. Use `agda` in powershell to check version. - -Now agda-mode in Doom Emacs. -- to install agda2-mode. - ``` - M-x package-install - ``` -- In `init.el`, uncomment `agda` in `lang`. -- `doom sync` to update. Then `SPC-q-R` to restart. - -To test things, make a `test.agda` file anywhere you'd like. -- Using Doom Emacs, open `test.agda`. -- Type in - ```agda - open import Agda.Builtin.Nat - ``` -- Use `C-c C-d` then enter `Nat`. - The output in the agda info window should be `Set`. - -Congratulations, you now have Agda and -can use emacs bindings for Agda. -However, you have nothing more than the -builtin types. - -## The Cubical Library - -The HoTT Game currently requires the `cubical-0.3` library. -We walk through _a_ installation of the `cubical-0.3` library. -See the [Agda documentation](https://agda.readthedocs.io/en/latest/tools/package-system.html) -for more about libraries. - -- Go to [here](https://github.com/agda/cubical/releases). - Under 'version 0.3', - download the 'Source Code' file in either formats `zip` or `tar.gz`. -- Open the 'Source Code' file. - It should turn into a folder which contains a folder called - 'cubical'. -- Rename 'cubical' to 'cubical-0.3'. - Inside it, there should be a `cubical.agda-lib` file - with contents - ``` - name: cubical-0.3 - include: . - depend: - flags: --cubical --no-import-sorts - ``` - This is the file that tells Agda "this is a library" when - Agda looks into this folder. - You can place 'cubical' anywhere you like. - For the sake of this guide, - let's say you put it in a place so that - the path is `LOCATION/cubical-0.3`. - -Now we need to tell Agda this 'cubical-0.3' library exists, -so that it will look for it when an Agda file uses code from it. - -- Open Powershell locally and do - ``` - agda -l fjdsk Dummy.agda - ``` -- Assuming you don't already have an Agda library called `fjdsk`, - you should see an error message of the form - ``` - Library 'fjdsk' not found. - Add the path to its .agda-lib file to - 'BLAHBLAHBLAH/libraries' - to install. - Installed libraries: - none - ``` - The `BLAHBLAHBLAH/libraries` is where we tell Agda of - the location of libraries. - For Windows, it should look like - ``` - C:\Users\USERNAME\AppData\Roaming\agda\libraries - ``` - where `USERNAME` is your username on your computer. -- Navigate to the folder - `C:\Users\USERNAME\AppData\Roaming\agda`. - _If there is no `agda` folder in - `C:\Users\USERNAME\AppData\Roaming`, - simply create one_. -- In `C:\Users\USERNAME\AppData\Roaming\agda`, - create a file `libraries` if there isn't one already. - Inside it, put - ``` - LOCATION/cubical-0.3/cubical.agda-lib - ``` -- Now do `agda -l fjdsk Dummy.agda` in powershell locally again. - This time the error message should be - ``` - Library 'fjdsk' not found. - Add the path to its .agda-lib file to - 'BLAHBLAHBLAH/libraries' - to install. - Installed libraries: - cubical-0.3 - (LOCATION/cubical-0.3/cubical.agda-lib) - ``` - Congratulations, Agda is now aware of - the existence of the `cubical-0.3` library. - -## The HoTT Game - -The HoTT Game is also an Agda library -so we need to repeat the above process for it. - -- In Powershell, navigate to - where you would like to put the HoTT Game. -- Use `git clone https://github.com/Jlh18/TheHoTTGame.git`. - This should copy the HoTT Game repository as - a folder called `TheHoTTGame`. - For the purposes of this guide, - let's say you have put the HoTT Game in your computer - at the path - ``` - LOCATION1/TheHoTTGame - ``` - Inside it, you should see many files, - one of which should be `TheHoTTGame.agda-lib`. -- Go back to `BLAHBLAHBLAH/libraries` - and add the following line - ``` - LOCATION1/TheHoTTGame/TheHoTTGame.agda-lib - ``` -- In Powershell, use `agda -l fjdsk Dummy.agda` again. - The error message should now look something like - ``` - Library 'fjdsk' not found. - Add the path to its .agda-lib file to - 'BLAHBLAHBLAH/libraries' - to install. - Installed libraries: - cubical-0.3 - (LOCATION/cubical-0.3/cubical-0.3.agda-lib) - TheHoTTGame - (LOCATION1/TheHoTTGame/TheHoTTGame.agda-lib) - ``` -- Using Doom Emacs, - open `Trinitarianism/Quest0.agda` and do `C-c C-l`. - Congratulations, you can now play the HoTT Game.