thehottgame / TheHoTTGame

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

Pin nix sources using niv / support WSL2 #12

Closed o1lo01ol1o closed 2 years ago

o1lo01ol1o commented 2 years ago

This pins nixpkgs and emacs-overlay to the versions specified in the niv-created nix directory. It also removes the version requirement on cubical.

This shell will now work on Windows WSL2 containers running nixos as documented here: https://github.com/Trundle/NixOS-WSL.

Jlh18 commented 2 years ago

Hi there. Thanks for this! I still haven't tried installing everything via Nix but I will do so now :) and then if it's all working I'll probably update the instructions on the website (currently it says mentions Nix as a way for Macs only).

Does changing the dependency cubical-0.3 to cubical mean that if the cubical.agda-lib must label the library cubical? I'm not sure exactly how it works

o1lo01ol1o commented 2 years ago

No, the version of cubical available must match the one specified locally if agda is to import it. Removing the version just means that agda will use whatever version of the library is locally available. At least I think that's how it works.

On Wed, Jan 12, 2022 at 11:09 AM jlh @.***> wrote:

Hi there. Thanks for this! I still haven't tried installing everything via Nix but I will do so now :) and then if it's all working I'll probably update the instructions on the website (currently it says mentions Nix as a way for Macs only).

Does changing the dependency cubical-0.3 to cubical mean that if the cubical.agda-lib must label the library cubical? I'm not sure exactly how it works

— Reply to this email directly, view it on GitHub https://github.com/thehottgame/TheHoTTGame/pull/12#issuecomment-1010926153, or unsubscribe https://github.com/notifications/unsubscribe-auth/AB5DC5IVK3CCQ4ZYLKDX7GTUVVONVANCNFSM5LYUD2DQ . You are receiving this because you authored the thread.Message ID: @.***>

-- 328 Plymouth St Brooklyn, NY 11201

617 990 7876

Jlh18 commented 2 years ago

I just tried installing agda with Nix (on linux and using the new branch) and I'm impressed! I will keep using this setup and see how it goes. I'm about to update the main site for instructions on the Nix install, hopefully including some links to WSL2 (which by the way looks super cool for people wanting to try out linux).

I'll be merging now. Thanks again :)