[isabelle-dev] Community Involvement in Isabelle Development

[Makarius]

On Fri, 15 Mar 2013, David Greenaway wrote:

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

The first question here is what is actually the core "development team". 
This has always fluctuated a bit over the years.  For me the hard facts 
are in the Mercurial changeset history, which I read every day, so I am 
usually informed about the state of affairs.

There has been some decline here in recent years, also due to general 
uncertainty about how things work, but I am pleased to see that the 
BNF/datatype/codatatype guys show some revival of actual hard working 
discipline, not just patching at will.


> 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.

Most of the actual work is rather boring maintenance, and sorting out 
problems from feature additions and patches from many years ago. As a rule 
of thumb, I spend myself 75% of time with things that nobody else wants to 
do, and only 25% with things than nobody else can do.

For the Isabelle2013 release, I tried to be as open-minded and welcoming 
as possible to encourage people to look through things in the critical 
phase before rollout.  Instead of all the traffic on isabelle-users and 
the tracker at bitbucket, I could have just as well done that over my 
private mail account with the very few people who actually did contribute 
here.


> 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.

That patch was conceptually wrong, and I spent quite some time explaining 
things.  This time was probably wasted on my side.



> 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.

I still did not look at these changes concretely.  Note that there has 
been an isabelle-dev thread on that issue some months ago.  As first 
exercise of "actual work" you can find that, and re-open the technical 
discussion, starting from there again.

And once more, I need to insist in proper terminology.  "Pretty" in 
Isabelle/Scala is an 'object' not a 'class' -- it imitates the structure 
Pretty from ML and is thus stateless.  This is not just nitpicking of 
superficial details.  Being sloppy on the surface indicates sloppiness in 
the depth of actual concepts.  How should I ever trust your changes like 
that?

For modules like Pretty that exist both in Isabelle/ML and Isabelle/Scala 
there is this additional challenge to keep them conceptually and 
structurally in sync over both languages.  Thus there are some 
side-conditions coming from the depths of time of Larry implementing 
Oppen.  Such things are not beyond reform, but it takes several rounds of 
looking very closely and carefully.


> 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.

This is the wrong approach.  In Isabelle we've always had a few experts 
being responsible for their specific area.  For example, when I have 
problems and questions about certain details in the code generator, I ask 
the ones who understand it, and I don't start fabricating patches myself. 
Doing so would inevitable mess up things.  The aspect that make as a 
system work are very delicate, like thin cobwebs that most people don't 
even see.

Note that "in-code documentation" is already there in most parts of 
Isabelle/Pure where I am responsible.  There is also the bulky 
"implementation" manual with partial coverage of important concepts -- 
everytime I revisit that, I am surprised how much it tells already, 
although that is not general known.  Some parts of the manual might be 
incomprehensible, but people should point that out and not start messing 
up the system due to lack of understanding.


If you want to start with some actual work, you can look at the tools that 
were contributed by some NICTA guys in the past.  E.g. find_theorems, 
find_consts, and most notably WWW_Find.  The latter has caused some 
trouble for Isabelle2013, mainly due to being unmaintained, i.e. there was 
nobody there by default to take care of it.

What is also a serious problem is the lack of Proof General maintenance. 
I am myself no longer involved there for quite some time, but it still has 
some users.  The next time when some small reform is happening in some 
corner, Proof General will break, and people start complaining.


 	Makarius