[isabelle-dev] Community Involvement in Isabelle Development

[David Greenaway]

On 14/03/13 22:37, Makarius wrote:
> Before we run again into a noisy thread that leads nowhere: the system
> development process is run by the people doing the actual work.  This
> sounds like a trivial tautology, but is often forgotten.

What level of community involvement (i.e., external contributions) in
the Isabelle development process, if any, does the core development team
desire?

I believe there are many people in the Isabelle community willing to do
"actual work", given the opportunity. Such community members, however,
are unlikely to make significant contributions without first being
allowed to make smaller contributions.

Joachim, for instance, was willing to create a patch and write
documentation to solve a particular itch he had. The feature appeared to
have some level of community support, and I suspect he would have been
more than willing to adjust any implementation concerns, such as his
choice of syntax or the ML implementation.

When such patches fall on their face, however, it sends a message to the
community that there is little point in doing actual work, as the
chances of the work being accepted are slim.

I must confess that yesterday I knowingly sent a half-baked patch
solving the jEdit proof-output wrapping problem to the Isabelle users
mailing list. I am more than willing to do the actual work of finishing
and polishing the patch---implementing the fix for tooltips and
SideKick, refactoring the "Pretty" class to internally use units of
something other than "fractions of the width of a space", writing
in-code documentation describing what is going on, ensuring my style
matches the guide-lines, etc. What stops me is that I am not convinced
that my time will be well-spent. If changes will not be accepted into
mainline, then it is not worth me doing the actual work of converting my
half-baked patch into a proper fix.

If, however, there becomes more of a culture of community involvement in
the Isabelle development process, then I would be willing to help out.
I will submit that patch which refactors "build.scala" to pull out the
ROOT parser so other tools can also use it. I will submit that patch
which adds additional in-code documentation to "proof_context.ML" to
help out users trying to learn the internals of the system. I will
submit that patch to include helper functions to assist users trying to
interface with Isabelle at the ML level.

The patches that I initially submit will no doubt be simple, and merely
scratching my own itches. But as I submit patches and receive feedback,
hopefully I will learn. Perhaps I will start being capable of making
more significant changes. And, as time goes on, one day you might even
wake up to find a patch in your inbox that scratches one of your itches.

For such a community to form, however, it must first be fostered. It
must be allowed to focus on the problems that it is facing.
Occasionally, it must be humoured.

At this point, however, it is not clear to me if external contributions
are actively welcomed, merely tolerated, or mostly discouraged.

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.