[isabelle-dev] Bad theory import "Main"

Makarius makarius at sketis.net
Mon Apr 24 15:39:02 CEST 2017

On 24/04/17 15:21, Lars Hupel wrote:
>> I actually offered an open dialog about it last December, and you
>> rejected that.
> Because the offer consisted merely of rehashing things we already talked
> about in person. To be completely frank, I'm tired of repeating myself
> and others endlessly.

I actually wanted to resolve all the open questions that remained in the
Jenkins project. Open problems that are still open need to be
"rehashed", even this is tiresome.

> For the record, the lxcisa0 host is the result of a compromise that both
> Jenkins and what you asked for (a publicly-accessible beefy machine)
> should be accommodated for. I wouldn't call that rejection.

So far, I did not even know that the ssh access was now "official". I
thought it was just privately for me, to do some basic hardware tests.

It shows that in "blame game" mode it is hard to communicate in a plain
and simple way.


More information about the isabelle-dev mailing list