<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
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.<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
For windows native installation the only success my students had was using Aaron Strump's installers under
<a href="http://homepage.cs.uiowa.edu/~astump/agda/" id="LPlnk123339">http://homepage.cs.uiowa.edu/~astump/agda/</a>
<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Anton<br>
</div>
<div>
<div id="appendonsend"></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Aaron Gray <aaronngray.lists@gmail.com><br>
<b>Sent:</b> 04 January 2022 22:31<br>
<b>To:</b> agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> [Agda] Getting Agda building and running on Windows</font>
<div> </div>
</div>
<div>
<div dir="ltr">Hi,<br>
<br>
Hi, I am a Agda newbie and trying to get a working platform on Windows.
<div><br>
<div>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 !<br>
<br>
Is there a standard Docker script for Agda ?<br>
<br>
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.
<div><br>
</div>
<div>Its working upto failing on Agda Standard Library, something to do with --guardedness in Codata/Musical/Notation.agda<br>
<br>
I have updated an existing Docker script to support Agda 0.2.6.2 and agda standard library 0.7 and 1.7.1 :-<br>
<br>
<a href="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" originalsrc="https://github.com/AaronNGray/docker-agda-stdlib" shash="dfyu3a+loV39FzFHQHYCiVjxj/+BMxPlnpDJAcoguJqW6sTZ1wlwLO6vNWStIhDmX0Ene47cY6fxyf3LSt3tlzg27giQUQU8YlPrJpxhiAdxEP7o0b0xRqEJwmdm/CwAj++r0yZeKjiDizqPTJAj0hAdDFPQe7VakJxFFLYqyRA=">https://github.com/AaronNGray/docker-agda-stdlib</a>
<div><br>
</div>
<div>I am getting the following :-</div>
<div><br>
</div>
<div> => ERROR [builder 11/13] RUN agda --verbose=0 src/Everything.agda 142.1s<br>
------<br>
> [builder 11/13] RUN agda --verbose=0 src/Everything.agda:<br>
#15 142.0 /root/.agda/lib/standard-library/src/Codata/Musical/Notation.agda:11,1-44<br>
#15 142.0 Importing module Agda.Builtin.Coinduction using the --guardedness<br>
#15 142.0 flag from a module which does not.<br>
#15 142.0 when scope checking the declaration<br>
#15 142.0 open import Agda.Builtin.Coinduction public<br>
------<br>
executor failed running [/bin/sh -c agda --verbose=0 src/Everything.agda]: exit code: 42</div>
<div><br>
</div>
<div>Any help would be appreciated.</div>
<div><br>
</div>
<div>
<div>Aaron</div>
<div>--<br>
</div>
<div>Aaron Gray<br>
<br>
Independent Open Source Software Engineer, Computer Language Researcher, and amateur computer scientist.</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</body>
</html>