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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to