[isabelle-dev] Bad theory import "Main"
nipkow at in.tum.de
Sun Apr 23 15:54:49 CEST 2017
The Isabelle regression test system shows up a mistake in a commit of yours and
you ask what its purpose is? And tell us your rarely look there?
On 23/04/2017 14:52, Makarius wrote:
> On 23/04/17 08:39, Tobias Nipkow wrote:
>> The Isabelle regression test system shows similar behaviour:
>> 23:23:27 *** No such file:
>> 23:23:27 *** The error(s) above occurred for theory "Main" (line 8 of
>> 23:23:27 *** The error(s) above occurred in session "HOL" (line 3 of
> I did not see this, because Jenkins is not "The Isabelle regression test
> system" and I am rarely looking what happens there -- I do look
> sometimes after significant changes of Isabelle/Scala, because I have no
> intention to destroy such experiments on purpose.
> Concerning the status of Jenkins wrt. isabelle-dev (not isabelle-group
> at TUM), we are still lacking a proper discussion of its purpose and
> general approach. When I started to ask some critical questions last
> year, I did not get any answers and was merely blamed for that.
> If there is anybody *outside* the TUM group, who uses the Jenkins setup
> regularly, it would be interesting to discuss some basic things. What is
> good about it? What is bad about it?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev