[Agda] agda under windows WSL

[Anton Setzer]

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/7b8d5319/attachment-0001.html>