[isabelle-dev] Bad theory import "Main"

[Tobias Nipkow]

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?

LOL

Tobias

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:
>> "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/Main.thy"
>> 23:23:27 *** The error(s) above occurred for theory "Main" (line 8 of
>> "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT")
>> 23:23:27 *** The error(s) above occurred in session "HOL" (line 3 of
>> "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT")
>
> 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?
>
>
> 	Makarius
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170423/bae3e62f/attachment.bin>