On 05/04/13 09:32, Makarius wrote:
> On Fri, 5 Apr 2013, David Greenaway wrote:
>> What practical things could such volunteers do that you would find
>> helpful?
>
> So how about maintaining Proof General, seriously, no-nonse?
As somebody who isn't a Proof General user, nor an Emacs user, nor has
ever worked with elisp, this doesn't fall particularly well within my
skill-set, unfortunately.
> And there are other unmaintained parts, such as WWW_Find. (Note that
> several other people have worked there in the meantime, and they
> should be included in the discussion, to benefit from the experience
> gained from certain find_theorems experiements that never hit the
> repository so far.)
WWW_Find is perhaps closer to my skill set, but still not a tool I use.
Volunteers, counter-intuitively, require payment. Sometimes such payment
is a simple "thanks" on a public mailing list or a changeset being
accepted into the official repository. Other times it requires seeing an
itch that they have been facing being scratched.
If we wanted to start a discussion about replacing "WWW_Find" with
a custom server that the inbuilt "find_theorems" command could be set up
to automatically probe...:
> find_theorems "(_ :: word32) + _ < 2 ^ 32"
searched for:
"_ + _ < 2 ^ 32"
0 theorem(s) found in current session.
2 theorem(s) found from theorem server "example.com":
WordLemmaBucket.word_add_power_off: [...]
(requires import of WordLemmaBucket)
LemmaBucket.word_add_bits: [...]
(requires import of LemmaBucket)
...then we would be talking about an itch that I would be willing to
volunteer some time to scratch.
Cheers,
David
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
