<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body 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="Signature">
<div>
<div></div>
<div id="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://hustmphrrr.github.io/">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="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" 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>
<style>
<!--
@font-face
{font-family:"Cambria Math"}
@font-face
{font-family:Calibri}
p.x_MsoNormal, li.x_MsoNormal, div.x_MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif}
a:link, span.x_MsoHyperlink
{color:blue;
text-decoration:underline}
a:visited, span.x_MsoHyperlinkFollowed
{color:#954F72;
text-decoration:underline}
p.x_msonormal0, li.x_msonormal0, div.x_msonormal0
{margin-right:0cm;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif}
span.x_EmailStyle18
{font-family:"Calibri",sans-serif;
color:windowtext}
.x_MsoChpDefault
{font-size:10.0pt}
@page WordSection1
{margin:72.0pt 90.0pt 72.0pt 90.0pt}
div.x_WordSection1
{}
-->
</style>
<div lang="EN-GB" link="blue" vlink="#954F72">
<div class="x_WordSection1">
<p class="x_MsoNormal"><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_MsoNormal"><span style=""> </span></p>
<p class="x_MsoNormal"><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_MsoNormal"><span style=""> </span></p>
<p class="x_MsoNormal"><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_MsoNormal"><span style=""> </span></p>
<p class="x_MsoNormal"><span style="">Anton</span></p>
<p class="x_MsoNormal"><span style=""> </span></p>
<div>
<div style="border:none; border-top:solid #E1E1E1 1.0pt; padding:3.0pt 0cm 0cm 0cm">
<p class="x_MsoNormal"><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_MsoNormal"> </p>
<p class="x_MsoNormal"><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_MsoNormal"><span lang="EN-US"> </span></p>
<p class="x_MsoNormal"><span lang="EN-US">Thanks,</span></p>
<p class="x_MsoNormal"><span lang="EN-US">Jason Hu</span></p>
<p class="x_MsoNormal"><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_MsoNormal"><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_MsoNormal"><span lang="EN-US"> </span></p>
<p class="x_MsoNormal"><span style="">Dear all,</span></p>
<p class="x_MsoNormal"><span style=""> </span></p>
<p class="x_MsoNormal"><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_MsoNormal"><span style=""> </span></p>
<p class="x_MsoNormal"><span style="">Thanks,</span></p>
<p class="x_MsoNormal"><span style="">Anton</span></p>
<p class="x_MsoNormal"><span lang="EN-US" style=""> </span></p>
</div>
</div>
</body>
</html>