[Agda] agda under windows WSL

[Xuanrui Qi]

Dear Anton,

Yes, yes, that's the problem. WSL2 is a VM, so I don't think there's an
easy fix for the file access problem, since you're breaking a
abstraction barrier here. If you store your files under WSL /home, then
everything runs just fine.

If you need to store your files on the Windows side, then maybe you
should use WSL 1. AFAIK, WSL 1 runs Agda just fine. Here I don't think
caching is a problem; even if it fixes the problem for this particular
use case, I'm not sure it's the right way to go as using Agda on WSL2
with Windows files is such a rare use case...

Xuanrui

On Fri, 2021-11-19 at 14:37 +0000, Anton Setzer wrote:
> 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
> Sent: Friday, November 19, 2021 8:03 AM
> To: 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
>  
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda