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

[Andrea Vezzosi]

Yeah, it's worth a try at least, you only need to put --caching as one
of the arguments for agda.

On Thu, Jun 8, 2017 at 10:28 AM, Andreas Abel <abela at chalmers.se> wrote:
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda