[isabelle-dev] Bad theory import "Main"

Makarius makarius at sketis.net
Sun Apr 23 14:52:54 CEST 2017

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?


More information about the isabelle-dev mailing list