[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks
david.greenaway at nicta.com.au
Fri Apr 5 01:04:47 CEST 2013
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
> 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
> 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"
"_ + _ < 2 ^ 32"
0 theorem(s) found in current session.
2 theorem(s) found from theorem server "example.com":
(requires import of WordLemmaBucket)
(requires import of LemmaBucket)
...then we would be talking about an itch that I would be willing to
volunteer some time to scratch.
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.
More information about the isabelle-dev