[Agda] Bounties for Agda features

[Nils Anders Danielsson]

On 2012-05-07 19:06, Daniel Peebles wrote:
> *Only reload changed parts of the source in the interactive environment*
> 
> I'd prefer this to be implemented generally, as I think the
> interaction machinery is trying to move away from strict
> emacs-specific behavior. Basically, C-c C-l currently always reloads
> the entire file when you run it, even if you've only changed a tiny
> piece of it.
> 
> I can think of two approaches to this, but I don't really care how
> it's done as long as it works. One approach is to parse and then run
> some sort of a clever diff on the parse tree before typechecking. The
> other is to run a textual diff and do something similar. The latter
> approach would likely work at the declaration level. Given the weird
> non-local behavior of constraints (I think this has decreased now, but
> back in the day you could write a really specific proof about a
> function and leave the function to be inferred by the constraints
> solver), determining how much would change given an AST-level change
> might be tricky.

We've had something like this for a while now (--caching). I think
Andrea Vezzosi was the main implementor of this feature.

> Bounty: 100 BTC

:)

-- 
/NAD