[isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks

[David Greenaway]

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.