[isabelle-dev] Bad theory import "Main"

Lars Hupel hupel at in.tum.de
Mon Apr 24 15:21:05 CEST 2017


> This is still "blame game".

If you say so.

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

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.



More information about the isabelle-dev mailing list