[Agda] Caching [Re: Type checking times and a solution.]

[Andreas Abel]

We are a bit short of emacs-lisp programmers, but if you implement 
something, we are happy to receive a pull request.

What makes Agda slow here is that the file is reloaded after each case 
split.  Ideally, the caching feature of Agda should speed things up in 
case you only work at the end of the file (not on holes somewhere in the 
middle where lots of definitions come after that).

@Andrea: is it reasonable to expect that the caching feature eliminates 
the 10s of seconds that Apostolis describes?

Best,
Andreas

On 07.06.2017 10:52, Apostolis Xekoukoulotakis wrote:
> Let us say that we have a big agda file and we have a function at the 
> bottom that has holes.
> Whenever we case split , it takes tens of seconds to do it.
> 
> Since all the previous functions are complete, one could simply create a 
> new file with the new function and work there. The type checking will be 
> instantaneous.
> 
> But this method is very tedious. An emacs command that copies the 
> function to another file and performs the typechecking there would be 
> much appreciated.
> 
> It needs to grab all the imports. It also needs to find the beginning 
> and ending of a function.
> We could use "empty" lines as the boundaries.
> 
> If there is code after that function, it is commented out.
> 
> This seems like an easy solution to me.
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/