[Agda] Getting Agda building and running on Windows

[Felix Cherubini]

I don't know anything about gWSL, but it worked for me some time ago to 
install an X-server on Windows 10 (as Anton did, but I used Xming) and 
connect to that from WSL. That worked out of the box and I blogged about 
it here:

https://schneide.blog/2019/11/11/compiling-and-using-agda-through-the-windows-linux-subsystem/

On 1/7/22 03:51, Jason Hu wrote:
> WSL2 works well for me too.
> 
> I heard that windows 11 is not very stable(especially for video games). 
> As always, Microsoft seems always to need a few years to polish their 
> new systems. If your laptop is not exclusive for work, I wouldn’t say 
> jumping directly to upgrading is a good idea. But if you do, it will 
> definitely be helpful for others if you can share your experience with 
> running Agda on windows 11.
> 
> I am curious how Linux GUI would work on windows 11? Is it just gonna 
> work out of the box? I’ve watched some videos on YouTube about some 
> windows 10 dev build which has what they called gWSL. So that’s 
> discontinued on windows 10?
> 
> Thanks,
> 
> Jason Hu
> 
> *From: *Anton Setzer <mailto:a.g.setzer at swansea.ac.uk>
> *Sent: *Thursday, January 6, 2022 9:30 PM
> *To: *Aaron Gray <mailto:aaronngray.lists at gmail.com>; 
> agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>
> *Subject: *Re: [Agda] Getting Agda building and running on Windows
> 
> Installing Agda using WSL worked for me very well. However, I needed to 
> put all agda files including the standard library into the root 
> directory (not into ~/  but into a folder in  / ) then the preformance 
> is quite good. However you need to get a GUI running so that you have 
> the emacs menus (which under Windows 11 will be provided which hopefully 
> makes life easier, under Windows 10 you have to set it up yourself), I 
> succeeded under windows 10 using vcXsrv, but that's a bit of work, 
> documentation is not very good since it's quite new.  Maybe upgrading to 
> Windows 11 first is a smart move.
> 
> For windows native installation the only success my students had was 
> using Aaron Strump's installers under 
> http://homepage.cs.uiowa.edu/~astump/agda/ 
> <http://homepage.cs.uiowa.edu/~astump/agda/>
> 
> Anton
> 
> *From:*Agda <agda-bounces at lists.chalmers.se> on behalf of Aaron Gray 
> <aaronngray.lists at gmail.com>
> *Sent:* 04 January 2022 22:31
> *To:* agda at lists.chalmers.se <agda at lists.chalmers.se>
> *Subject:* [Agda] Getting Agda building and running on Windows
> 
> Hi,
> 
> Hi, I am a Agda newbie and trying to get a working platform on Windows.
> 
> I have tried Ubuntu on WLS on Windows 10, versions are well old, why I 
> don't know, Chocolatey, issues with Agda Standard Library and now trying 
> Docker !
> 
> Is there a standard Docker script for Agda ?
> 
> I tried a docker script that presumably I thought worked on older 
> versions but I have just found does not even get as far as I have.
> 
> Its working upto failing on Agda Standard Library, something to do with  
> --guardedness in Codata/Musical/Notation.agda
> 
> I have updated an existing Docker script to support Agda 0.2.6.2 and 
> agda standard library 0.7 and 1.7.1 :-
> 
> https://github.com/AaronNGray/docker-agda-stdlib 
> <https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FAaronNGray%2Fdocker-agda-stdlib&data=04%7C01%7CA.G.Setzer%40Swansea.ac.uk%7C24acb3542b4a40d82ea108d9cfd1fbd5%7Cbbcab52e9fbe43d6a2f39f66c43df268%7C0%7C0%7C637769323461737818%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=6%2BIY7b9midNtbC6MwQ1Bm%2B3DUI4NiH4E5SH5YGqJxm0%3D&reserved=0> 
> 
> 
> I am getting the following :-
> 
>       => ERROR [builder 11/13] RUN agda --verbose=0 src/Everything.agda 
>                                                142.1s
>      ------
>       > [builder 11/13] RUN agda --verbose=0 src/Everything.agda:
>      #15 142.0 
> /root/.agda/lib/standard-library/src/Codata/Musical/Notation.agda:11,1-44
>      #15 142.0 Importing module Agda.Builtin.Coinduction using the 
> --guardedness
>      #15 142.0 flag from a module which does not.
>      #15 142.0 when scope checking the declaration
>      #15 142.0   open import Agda.Builtin.Coinduction public
>      ------
>      executor failed running [/bin/sh -c agda --verbose=0 
> src/Everything.agda]: exit code: 42
> 
> Any help would be appreciated.
> 
> Aaron
> 
> --
> 
> Aaron Gray
> 
> Independent Open Source Software Engineer, Computer Language Researcher, 
> and amateur computer scientist.
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>