[isabelle-dev] Bad theory import "Main"

[Makarius]

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