[Agda] Getting Agda building and running on Windows

[Jason Hu]

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/

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220107/75df6af1/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: B88DCD7B302544DF94F8D206E8303BFB.png
Type: image/png
Size: 159 bytes
Desc: B88DCD7B302544DF94F8D206E8303BFB.png
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220107/75df6af1/attachment-0001.png>