[Agda] Bounties for Agda features

[Daniel Peebles]

Hi all,

I posted these bounties for Agda features (effectively an attempt to
prioritize work on features that I care about) on Google+ and on Twitter,
but this seems like the best place to post them, to get the most exposure
to people who know the most about Agda.

Please let me know if you see any issues in how I've set this up. Also, if
you think you know someone who might be interested in working on any of
these, pointing them to http://bitbounties.org/agda should work.

Thanks,
Daniel


-----------------------------------------------------------------------------------------------------------------------------------

These bounties will be paid to anyone who manages to get patches for the
listed features into the Agda repository. As with any other open-source
venture, the code should be good and the project maintainers shouldn't be
burdened by your work, beyond basic merging efforts. That is, please don't
pester Ulf, Nils, or Andreas too much for help. The last thing I want to do
with the bounties is give them more work. And if you are Ulf, Nils, or
Andreas, you're still eligible for the bounties, of course! I also welcome
collaboration between people, in which case I will split the bounty as the
participants see fit.

Although you should not annoy the maintainers, I do welcome public
discussion on the mailing list about how the features below should be
implemented. It'd be horrible if you went off and implemented the most
awesome approach to the problems below, and then it turned out a maintainer
didn't like the approach, or was already implementing it differently.
Basically, the bounties should not affect your standards of code quality
and team work.

As far as standards are concerned, I leave the judgment up to the
maintainers. If they merge your code into the main repository, you get my
coins and eternal gratitude. If they don't, I hope you can work things out
so that they do :)

And if you really hate bitcoins and think they're a pyramid
scheme/scam/whatever other criticisms have been thrown at them, I'd be
willing to give you the equivalent market value (as judged by the MtGox
exchange rate) of the coins at the time of payment with Dwolla or PayPal.
I'd really prefer Dwolla though; not really a fan of PayPal.

Of course, if other people would like to add money to the pots for these
bounties or others, I'll happily post the updates here.

If you'd like to contact me about this stuff, I'm copumpkin on freenode and
twitter, or Daniel Peebles on Google+ (and most other places :P).


*Share terms in the normalizer / compile-time evaluator*

As we all know, large Agda projects quickly get bogged down by excessive
resource consumption. A lot of the bad performance can be attributed to the
almost complete lack of sharing in in-memory Agda terms, which means both a
blow-up in RAM usage by storing many identical copies of the same term, and
a blow-up in processing time computing them.

There are a couple of approaches to improving this, from what I've heard.
One is hash-consing, where you keep a global stash of all terms and
subterms and make to grab the canonical one every time you construct a new
one. This should lead to perfect sharing, but might be painful to implement
and could slow things down with all the hashing of complex structures
involved. Another approach is to implement something more closely
resembling Haskell's call-by-need evaluator.

Bounty: 100 BTC


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

Bounty: 100 BTC


*Come up with a neat solution to control depth of evaluation locally*

See http://code.google.com/p/agda/issues/detail?id=433

I see this mostly as an ease-of-use feature, but it might also help
performance. Basically, often you really don't want terms to normalize
fully in your goals or context. Some of my proofs have goals whose normal
forms are thousands (literally) of lines long, so the goal output becomes
effectively unusable.

Most of the time, I want to work at a higher level of abstraction than
individual recursively defined functions, and I've already proved simple
lemmas about them. In those cases, I don't want simple definitions to
normalize past a certain point, and want to prove things about the
higher-level expressions.

For example, when I'm writing simple proofs about the algebraic properties
of operations on the naturals, I might want my definitions to normalize,
but other times I might not. For example, (1 + x) + ((1 + y) * (1 + z))
will normalize to the horrible suc (x + suc (z + y * suc z)). If I have a
proof about the original form, it takes a lot of squinting to realize that
the normal form applies to it.

Bounty: 50 BTC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120507/51f25bfc/attachment.html