[isabelle-dev] Community Involvement in Isabelle Development
makarius at sketis.net
Fri Mar 15 13:21:16 CET 2013
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
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
> 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
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
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.
More information about the isabelle-dev