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

[Apostolis Xekoukoulotakis]

Caching definitely helps but it still takes some time to typecheck the
current file.

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

On Thu, Jun 8, 2017 at 12:45 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170608/82dc8225/attachment.html>