[isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support "isabelle build" Options

[Makarius]

On Fri, 17 Aug 2012, Tobias Nipkow wrote:

> Am 17/08/2012 21:51, schrieb Christian Urban:
>>
>>
>> On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote:
>> > Tjark, you have no business here.
>>
>> I assume something got here lost in translation.
>> Otherwise, we should all make reasonable effort
>> to welcome everybody on both, the isabelle-users
>> and isabelle-dev lists. After all, we like to have
>> plenty of users and plenty of developers for Isabelle;
>> not like the GDR, which had a country, but in the end
>> had no people. ;o)
>
> Thank you, Christian, spot on.

The number of users and number of developers is off-topic here.  I am not 
commenting further on this complex issue on this thread (you can open 
another if you want).


Back to the main issue:

> I had some interesting conversations at the Isabelle workshop in 
> Princeton. The tone of the isabelle mailing list is perceived as 
> amusingly agressive by outsiders. I don't find it amusing, I find it 
> aggarvating.
>
> Taking a dig at someone via a ceterum censeo in a signature is not 
> helpful, but "You have no business here" is downright rude.

This was indeed a hot outbreak on after a rather cool thread here:

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-August/003011.html
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-August/003013.html
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-August/003021.html

My unusually cool conclusion after Tjark still not quite understanding 
(even until now):

   > So I have to follow one more change to get the work done eventually.

   > This is not very productive.


> Can everybody please watch their language? I may be old fashioned, but 
> saying "Please do not ... because ..." instead of "You have no business 
> here" makes all the difference. As my grandmother, god bless her, used 
> to say: "Der Ton macht die Musik".

The tone was indeed a bit harsh at the end and on the wrong thread.  I was 
referring to Tjarks's 
http://isabelle.in.tum.de/repos/isabelle/rev/ec82c33c75f8 after I've made 
several times clear that he should not engage in the ongoing work by 
Krauss/Haftmann/Wenzel on the component business.  It is part of old 
Isabelle development wisdom that more than 2-3 people cannot work 
productively on a particular topic.

I did not know that Tjark had conversed with Florian privately before. 
This removes the main accusation on his 
http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was 
looking like he was seizing control of the draft started by Florian.

It is part of ancient Isabelle development tradition that places of 
activity by one person are not directly interfered by another one, until 
the dust has settled; and then it is often better to start some email 
thread than pushing further changes on top.  Otherwise there would be a 
constant fear of people who are starting some intiatives that they cannot 
finish quickly enough before others meddle with it.  This was also what my 
rather cool remark "The Isabelle repository is not a Wiki" was referring 
to (although German Wikipedia would not even allow such uncoordinated 
edits).


Anyway, some concluding remarks on a hot thread on a hot day:

   * The isabelle-dev mailing list was started on my initiative, and I've 
tried to motivate people over several years to redirect the discussion of 
Isabelle internals from my personal mail address to the public mailing 
list. In the last year or so this has actually started to work, so that 
sometimes there are some actual technical discussions, not just opinions. 
And people who are not directly engaged in some topic can see what is 
happening, without secret decisions happening in the back room.

   * I hope that we will all make an effort to continue making isabelle-dev 
the place where stuff really happens.

   * Mail signature lines suck, but I will use one just this time.


 	Makarius

--
Do not meddle in the affairs of wizards, for they are subtle and quick to anger.