search

thehottgame / TheHoTTGame

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT
124 stars 15 forks source link

Issues trying to Install TheHoTTGame on Windows 10 #5

Closed kram1032 closed 2 years ago

kram1032 commented 2 years ago

I'm a near complete beginner with emacs, so a lot of the below is probably some form of silly. That said, maybe the issues I've had are a good guide for looking at blind spots such as they currently exist in the documentation.

I tried following along with the installation guide. It didn't quite work as described, but I managed to get there. In hoping for a completely foolproof guide in the future, I'll detail what I had to do.

  1. install chocolatey - I already had this installed, so no issues here for me
  2. choco install ghc cabal - worked fine
  3. cabal install happy alex - this was the first thing that tirpped me up a bit. In order to make cabal see ghc, I had to close the editor and open it again, so it would see the updated environment variables. There is a refreshenv function that ought to help with this as well, but for some reason that did nothing.
  4. follow the doom emacs guide - worked as written. Basically, get a bunch of files, register them in path, use git-bash to install emacs, register that too, download the fonts, and install them by navigating to the files and doubleclicking them. After restarting, doom emacs looks correct.
  5. git clone agda - works
  6. cabal install make - cabal does not find this package and as far as I can tell it really does not exist. I tried cabal update too. To no avail. At that point I broke with the guide. I was suggested to try using stack instead.

Here is my process with stack:

  1. install stack using the installer here https://docs.haskellstack.org/en/stable/install_and_upgrade/#windows
  2. in git-bash, run stack upgrade
  3. cabal get Agda
  4. it creates a folder Agda-2.6.2, so cd Agda-2.6.2
  5. in the folder, there is a stack-9.0.1.yaml. This is for a different version of ghc than I previously installed. But that's the most recent version of ghc there is a yaml for currently, so: stack --stack-yaml stack-9.0.1.yaml install

I now have the correct version of agda installed. At that point, I went back to the guide:

  1. open emacs
  2. Alt+x package-install
  3. agda2-mode - was not found. I tried proceeding anyway.
  4. at this point I did not know how to navigate to .doom.d/init.el within doom, so I did it in a different editor instead. found ;;agda and removed the leading ;s
  5. in a shell, doom sync - the text there mentioned agda2-mode
  6. in emacs, space q R to restart
  7. made a test.agda
  8. I had to google how to actually open a file in doom emacs. The command, if you are already in the right folder, is Ctrl x Ctrl f, then start typing the file name and enter
  9. in the file, type in open import Agda.Builtin.Nat
  10. Control C Control d, "Nat"
  11. "The Agda mode's version (2.6.3) does not match that of agda (2.6.2)"

So at this point, I have no idea what else I did. It must have been something, but I forget. Maybe all I had to do was once again to close and open emacs again. Because I tried again, and suddenly, I get Set, as the guide suggests. No idea where it got the 2.6.3 version from in the first place. But if that can be reverse-engineered somehow, it'd probably be good information for the guide as well.

Next up, the cubical library. From here on out, things basically worked without a hassle, but for completeness sake, here is how it went for me:

  1. find the source file as linked
  2. unpack it wherever you like, say in LOCATION/cubical-0.3 (in windows, clicking on that file won't just turn it into a folder. You'll be taken inside instead) - the folder inside is called "cubical-0.3" so the step of renaming it to that is unnecessary
  3. in a shell, agda -l fjdsk Dummy.agda - works
  4. navigate to the file it mentions, namely %AppData%\agda\libraries - that folder and file did not exist. So I created them, as instructed.
  5. agda -l fjdsk Dummy.agda again - the library is listed as installed

finally, The HoTT Game

  1. in a shell, cd to a location you'd like the HoTT Game to be installed
  2. git clone https://github.com/Jlh18/TheHoTTGame.git
  3. put it in the libraries file again, check that it's installed - yup, works
  4. open the file (don't yet know how to navigate folders in emacs - I navigated to the right folder in git-bash and opened emacs there, then Ctrl x Ctrl f Quest0.a to open the actual file
  5. Ctrl c Ctrl l - it now loads a bunch of stuff. Success!
Jlh18 commented 2 years ago

Thanks so much for such a detailed account of the installation - I'll try to incorporate it into our guide for windows. Hopefully we can cover more of the various issues that come up. We have a basic guide to using Doom Emacs but of course it doesn't cover everything (it doesn't cover navigation). The most use command from there is SPC h b b, which you can use to search for other commands. https://thehottgameguide.readthedocs.io/en/latest/getting-started/emacs-commands.html#general-doom-emacs-usage but of course it doesn't cover everything.

For navigating files one thing you can do is get treemacs, which is a bit more visually helpful, or you can also use SPC .

I'm glad you got it working, and I hope you enjoy the game :)

Jlh18 commented 2 years ago

Just to let you know I have made a ton of edits (a lot according to what you wrote above) to the installation page

https://thehottgameguide.readthedocs.io/en/latest/getting-started/installation.html

kram1032 commented 2 years ago

I later saw the guide for Emacs which was very helpful. It's just listed after the install guide and since I was focused on installation, I didn't see that that exists as well The installation guide looks much more complete now, thanks :)

o1lo01ol1o commented 2 years ago

@kram1032 see #12 for a more streamlined way to get support on Windows via WSL2