<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">WSL2 works well for me too. </p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">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.</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">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?</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:a.g.setzer@swansea.ac.uk">Anton Setzer</a><br>
<b>Sent: </b>Thursday, January 6, 2022 9:30 PM<br>
<b>To: </b><a href="mailto:aaronngray.lists@gmail.com">Aaron Gray</a>; <a href="mailto:agda@lists.chalmers.se">
agda@lists.chalmers.se</a><br>
<b>Subject: </b>Re: [Agda] Getting Agda building and running on Windows</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">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.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">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/">http://homepage.cs.uiowa.edu/~astump/agda/</a>
<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">Anton<o:p></o:p></span></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<p class="MsoNormal"><img border="0" width="463" height="2" style="width:4.8194in;height:.0208in" id="Horizontal_x0020_Line_x0020_1" src="cid:image001.png@01D80347.C5AE85A0"><o:p></o:p></p>
<div id="divRplyFwdMsg">
<p class="MsoNormal"><b><span style="color:black">From:</span></b><span style="color:black"> 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</span> <o:p></o:p></p>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Hi,<br>
<br>
Hi, I am a Agda newbie and trying to get a working platform on Windows. <o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">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.
<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">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">https://github.com/AaronNGray/docker-agda-stdlib</a>
<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I am getting the following :-<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> => 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<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Any help would be appreciated.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal">Aaron<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">--<o:p></o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<p class="MsoNormal">Aaron Gray<br>
<br>
Independent Open Source Software Engineer, Computer Language Researcher, and amateur computer scientist.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>