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

[Andreas Abel]

So it is off by default?

Does {-# OPTIONS --caching #-} work on top of the file?

On 08.06.2017 10:37, Andrea Vezzosi wrote:
> 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

-- 
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/