[Agda] agda under windows WSL

Tue Nov 23 19:37:40 CET 2021

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

Anton

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

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/<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>
________________________________
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/20211123/20f74769/attachment.html>