<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>
<div id="appendonsend" style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
I have the feeling we will see more on WSL and Agda in the future, since this might be a good way to get Agda installed on windows machines.</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
It seems that the standard setting which is provided by windows sets the home directory under WSL so that it is mounted under windows, and the reason is that this way it is well integrated into the windows file system, at the cost that fileaccess is slow. If
one moves files to the root directory of the linux file system then one doesn't have this problem anymore. However one needs to make sure that the standard library is in the linux root directory as well, since it requires a lot of file access. It could even
be that the main culprit is the standard library and one could keep the normal files in the home directory (it's not an issue for me since it is all on git).
<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
What is highlighted by this is the fact that Agda seems to make a lot of file access in the standard library - I would usually expect that once it has been loaded it is kept in memory. But maybe all what happens is that it continously checks whether files have
changed and that slows it down.<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 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)">
<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> Jason Hu <fdhzs2010@hotmail.com><br>
<b>Sent:</b> 19 November 2021 14:44<br>
<b>To:</b> Anton Setzer <A.G.Setzer@Swansea.ac.uk>; agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: agda under windows WSL</font>
<div> </div>
</div>
<div dir="ltr">
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
Hi Anton,</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
If you look up the internet, you will find that WSL2 uses some network file system to mount your windows drives, and for that reason, this performance issue has been known for ages. As fundamental as it is, I don't see it can be fixed in any near future. Of
course, WSL has no such issue.</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
However, based on your description, I am further convinced that there is a problem with your setup. Essentially, WSL2 is a shallow wrapper of hyper-v VM. The file associated with your linux subsystem should be a hyper-v disk. On my machine, my Ubuntu WSL2 uses
this hyper-v disk for home folder as well as all Agda related stuff, and thus IO is performed in native speed. The home folder is not supposed to be mounted. I suggest you to try a clean setup and see if this problem goes away.<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0); background-color:rgb(255,255,255)">
If you are attempting a workflow where you put files in your windows drives and switch to WSL2 for work, this won't work well.<br>
</div>
<div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div id="x_Signature">
<div>
<div></div>
<div id="x_divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fhustmphrrr.github.io%2F&data=04%7C01%7CA.G.Setzer%40Swansea.ac.uk%7C9377f5e91c134a4e84b708d9ab6b22cc%7Cbbcab52e9fbe43d6a2f39f66c43df268%7C0%7C0%7C637729299510792117%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=uc%2B3mePUIX0IV6P3clHgNpjGrnUJeFk0lGGrjsbUp9w%3D&reserved=0" originalsrc="https://hustmphrrr.github.io/" shash="LVqu5yOqMqdLrDcyj+T9dOI5qxWnJIhoO4B1v8S0J0td0DwOqs/kGpdRnlqPCzCxtZPs/9wnY39vuFt0ujpf2WNUL2Rvbb2h4l0rfxuSa3LAMCs9LnlflxuK95XYUDub+E47rXoEwPS3IusaZVxVEbohSHHLOQs9obxVkN3R9eo=">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
</div>
</div>
<div id="x_appendonsend"></div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="x_divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Anton Setzer <a.g.setzer@swansea.ac.uk><br>
<b>Sent:</b> November 19, 2021 9:37 AM<br>
<b>To:</b> Jason Hu <fdhzs2010@hotmail.com>; agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> RE: agda under windows WSL</font>
<div> </div>
</div>
<div lang="EN-GB">
<div class="x_x_WordSection1">
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">I found the culprit why agda under wsl was so slow on my machine. It is that Agda seems to be doing a lot of file access esp when using the standard library, and under wsl one should not put such files under /mnt/</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style=""> </span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">The problem was that one needs to put the agda code and the standard library so that they are not under /mnt/. Unfortunately the linux home directory is under /mnt/ I just put them as an experiment into /tmp/ and got a speedup from 8 min
20 sec down to 24 sec. What is important is to put the standard library so that it is not in /mnt/ if one just does it for the normal agda files I saw only a small speedup from 8 min 20 to 6 min 10 sec</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style=""> </span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">So it seems that Agda is making an incredible amount of file access in the standard library and is not cashing the data in memory (actually memory usage was quite low and the maximum load for a processor I could see was 60% so it seems most of
the time been busy with file access. I assume if one did more cashing Agda could become faster (or do I need to compile it in a different way so that this is automatically done?)</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style=""> </span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">Anton</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style=""> </span></p>
<div>
<div style="border:none; border-top:solid #E1E1E1 1.0pt; padding:3.0pt 0cm 0cm 0cm">
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<b><span lang="EN-US">From:</span></b><span lang="EN-US"> Jason Hu <fdhzs2010@hotmail.com>
<br>
<b>Sent:</b> 19 November 2021 13:05<br>
<b>To:</b> Anton Setzer <A.G.Setzer@Swansea.ac.uk>; agda@lists.chalmers.se<br>
<b>Subject:</b> RE: agda under windows WSL</span></p>
</div>
</div>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
</p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span lang="EN-US">It depends on your setup and CPU. I have a laptop which does exactly WSL2 + agda and it runs very fast, probably at native speed.</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span lang="EN-US"> </span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span lang="EN-US">Thanks,</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span lang="EN-US">Jason Hu</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span lang="EN-US"> </span></p>
<div style="border:none; border-top:solid #E1E1E1 1.0pt; padding:3.0pt 0cm 0cm 0cm">
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<b><span lang="EN-US">From: </span></b><span lang="EN-US"><a href="mailto:a.g.setzer@swansea.ac.uk">Anton Setzer</a><br>
<b>Sent: </b>Friday, November 19, 2021 8:03 AM<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><br>
<b>Subject: </b>[Agda] agda under windows WSL</span></p>
</div>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span lang="EN-US"> </span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">Dear all,</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style=""> </span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">My university provided me with a windows only laptop and I have installed agda under windows WSL2. But it is incredibly slow, it takes about 10x longer than under a normal linux mschine with similar spec to type check. Does anybody have any hints
how to speed it up?</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style=""> </span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">Thanks,</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="">Anton</span></p>
<p class="x_x_MsoNormal" style="margin-top: 0px; margin-bottom: 0px;margin: 0cm 0cm 0.0001pt; font-size: 11pt; font-family: "Calibri", sans-serif;">
<span style="" lang="EN-US"> </span></p>
</div>
</div>
</div>
</div>
</body>
</html>