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

[Andrea Vezzosi]

Yes, it's off by default, and no it does not work on top of the file.

Cheers,
Andrea

On Thu, Jun 8, 2017 at 10:38 AM, Andreas Abel <abela at chalmers.se> wrote:
> 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/