search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Agda should not have to recheck the whole file everytime #834

Open UlfNorell opened 10 years ago

UlfNorell commented 10 years ago

From guillaum...@gmail.com on April 11, 2013 21:45:42

When working at the end of a not-so-small file, every time you add a new definition you need to reload the file and the whole file is type-checked again even if nothing has changed except for the last line.

Sometimes it is useful to split the file by hand (and import the first half in the second half) in order to prevent Agda from typechecking again and again the beginning of the file which never changes.

This shouldn’t be needed, for instance a very hacky fix would be to store the md5sum of every initial segment of the file and only recheck the file starting at the point where the md5sums differ. I’m even considering writing a shell script doing that for me, but if Agda could do it by default it would be even better (also I’m not sure how I would integrate my script in emacs). I don’t see why it would be difficult but I don’t know the internals of Agda so maybe I’m wrong.

Original issue: http://code.google.com/p/agda/issues/detail?id=834

UlfNorell commented 10 years ago

From nils.anders.danielsson on April 12, 2013 03:15:57

ISTR that Wolfram Kahl started work on something like this. Wolfram, what design did you have in mind? Did you encounter any serious problems?

Status: InfoNeeded
Cc: k...@cas.mcmaster.ca

UlfNorell commented 10 years ago

From andreas....@gmail.com on April 13, 2013 04:26:04

Labels: Type-Enhancement

UlfNorell commented 10 years ago

From k...@cas.mcmaster.ca on April 13, 2013 11:46:46

The idea was to compare the parsed syntax tree from .(l)agda with the syntax tree stored in .agdai, and if they coincided, to skip re-type-checking even if the source is newer than the .agdai. (This is different from what is proposed here, since here, Agda would re-use partial modules.)

However, since the syntax highlighting was stored in the .agdai file, too, and referred to the old source positions, the highlighting in emacs was all messed up, and I didn't see a plausible way out of that. Is this now more decoupled with the new emacs interaction?

UlfNorell commented 10 years ago

From nils.anders.danielsson on April 17, 2013 02:05:14

Is this now more decoupled with the new emacs interaction?

No. However, the parse trees contain information about source locations, so I don't quite see what the problem is.

I don’t see why it would be difficult but I don’t know the internals of Agda so maybe I’m wrong.

Agda uses mutable state internally [*]. I guess one could use a pure state monad, and store a (shared) copy of the current state after each mutual block has been checked. However, I imagine that this would hurt performance.

[*] Partly for performance reasons, but also to improve sharing. However, the sharing machinery is not (yet?) good enough, and currently not activated.