<div>Hi all,</div><div><br></div><div>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.</div>
<div><br></div><div>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 <a href="http://bitbounties.org/agda">http://bitbounties.org/agda</a> should work.</div>
<div><br></div><div>Thanks,</div><div>Daniel</div><div><br></div><div><br></div><div>-----------------------------------------------------------------------------------------------------------------------------------</div>
<div><br></div>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.<br>
<br>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.<br>
<br>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 :)<br>
<br>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.<br>
<br>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.<br><br>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).<br>
<br><br><b>Share terms in the normalizer / compile-time evaluator</b><br><br>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.<br>
<br>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.<br>
<br>Bounty: 100 BTC<br><br><br><b>Only reload changed parts of the source in the interactive environment</b><br><br>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.<br>
<br>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.<br>
<br>Bounty: 100 BTC<br><br><br><b>Come up with a neat solution to control depth of evaluation locally</b><br><br>See <a href="http://code.google.com/p/agda/issues/detail?id=433">http://code.google.com/p/agda/issues/detail?id=433</a><br>
<br>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.<br>
<br>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. <br>
<br>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.<br>
<br>Bounty: 50 BTC<br><br>