<div dir="ltr"><div>Caching definitely helps but it still takes some time to typecheck the current file.<br><br></div><div>From now on, my workflow will be to have a separate text file where I introduce new functions. When I finish with them, I will put them to the original file.<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jun 8, 2017 at 12:45 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes, it's off by default, and no it does not work on top of the file.<br>
<br>
Cheers,<br>
Andrea<br>
<div class="HOEnZb"><div class="h5"><br>
On Thu, Jun 8, 2017 at 10:38 AM, Andreas Abel <<a href="mailto:abela@chalmers.se">abela@chalmers.se</a>> wrote:<br>
> So it is off by default?<br>
><br>
> Does {-# OPTIONS --caching #-} work on top of the file?<br>
><br>
><br>
> On 08.06.2017 10:37, Andrea Vezzosi wrote:<br>
>><br>
>> Yeah, it's worth a try at least, you only need to put --caching as one<br>
>> of the arguments for agda.<br>
>><br>
>> On Thu, Jun 8, 2017 at 10:28 AM, Andreas Abel <<a href="mailto:abela@chalmers.se">abela@chalmers.se</a>> wrote:<br>
>>><br>
>>> We are a bit short of emacs-lisp programmers, but if you implement<br>
>>> something, we are happy to receive a pull request.<br>
>>><br>
>>> What makes Agda slow here is that the file is reloaded after each case<br>
>>> split.  Ideally, the caching feature of Agda should speed things up in<br>
>>> case<br>
>>> you only work at the end of the file (not on holes somewhere in the<br>
>>> middle<br>
>>> where lots of definitions come after that).<br>
>>><br>
>>> @Andrea: is it reasonable to expect that the caching feature eliminates<br>
>>> the<br>
>>> 10s of seconds that Apostolis describes?<br>
>>><br>
>>> Best,<br>
>>> Andreas<br>
>>><br>
>>> On 07.06.2017 10:52, Apostolis Xekoukoulotakis wrote:<br>
>>>><br>
>>>><br>
>>>> Let us say that we have a big agda file and we have a function at the<br>
>>>> bottom that has holes.<br>
>>>> Whenever we case split , it takes tens of seconds to do it.<br>
>>>><br>
>>>> Since all the previous functions are complete, one could simply create a<br>
>>>> new file with the new function and work there. The type checking will be<br>
>>>> instantaneous.<br>
>>>><br>
>>>> But this method is very tedious. An emacs command that copies the<br>
>>>> function<br>
>>>> to another file and performs the typechecking there would be much<br>
>>>> appreciated.<br>
>>>><br>
>>>> It needs to grab all the imports. It also needs to find the beginning<br>
>>>> and<br>
>>>> ending of a function.<br>
>>>> We could use "empty" lines as the boundaries.<br>
>>>><br>
>>>> If there is code after that function, it is commented out.<br>
>>>><br>
>>>> This seems like an easy solution to me.<br>
>>>><br>
>>>><br>
>>>> ______________________________<wbr>_________________<br>
>>>> Agda mailing list<br>
>>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
>>>><br>
>>><br>
>>><br>
>>> --<br>
>>> Andreas Abel  <><      Du bist der geliebte Mensch.<br>
>>><br>
>>> Department of Computer Science and Engineering<br>
>>> Chalmers and Gothenburg University, Sweden<br>
>>><br>
>>> <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
>>> <a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~<wbr>abela/</a><br>
>>> ______________________________<wbr>_________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
> --<br>
> Andreas Abel  <><      Du bist der geliebte Mensch.<br>
><br>
> Department of Computer Science and Engineering<br>
> Chalmers and Gothenburg University, Sweden<br>
><br>
> <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
> <a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~<wbr>abela/</a><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>