[Agda] agda under windows WSL

[Jason Hu]

Hi Anton,

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.

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.

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.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Anton Setzer <a.g.setzer at swansea.ac.uk>
Sent: November 19, 2021 9:37 AM
To: Jason Hu <fdhzs2010 at hotmail.com>; agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: RE: agda under windows WSL


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/



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



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?)



Anton



From: Jason Hu <fdhzs2010 at hotmail.com>
Sent: 19 November 2021 13:05
To: Anton Setzer <A.G.Setzer at Swansea.ac.uk>; agda at lists.chalmers.se
Subject: RE: agda under windows WSL



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.



Thanks,

Jason Hu



From: Anton Setzer<mailto:a.g.setzer at swansea.ac.uk>
Sent: Friday, November 19, 2021 8:03 AM
To: agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>
Subject: [Agda] agda under windows WSL



Dear all,



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?



Thanks,

Anton


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211119/ee5d8975/attachment.html>