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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
