On Thu, Jun 18, 2009 at 10:55 AM, Makarius<makarius at sketis.net> wrote: > ?* The main Isabelle repository http://isabelle.in.tum.de/repos/isabelle > ? ?always needs to be in a state where > > ? ? ?isabelle makeall all > > ? ?finishes succesfully!
This last failure was due to some changes that I pushed recently. Lately I have been using "isabelle makeall all" consistently before each push. This most recent problem was due to my misunderstanding of how "isabelle makeall all" works. I managed to get into a state where I believed that all the tests had been run, when really they hadn't. Let me explain in more detail. I had noticed that when using "isabelle makeall all", if one of the build targets fails, the others will still be run. For example, even after HOL-ex fails, HOLCF will still be compiled and tested. I was very happy to see this feature, because for me, running the full test suite is an overnight process (HOL-Nominal-Examples alone takes over 4 hours) and it would be very frustrating to have an early error prevent several hours' worth of other later tests from being run. In this case, after running "makeall all" overnight, I found that HOL-ex was the only failure: CodegeneratorTest was failing because of some missing [code del] declarations. I added the [code del] declarations, and then compiled HOL-ex successfully. At this point, I was under the impression that the entire repository had undergone the appropriate tests. I pushed my changes. Of course, I now know that "makeall all" doesn't really work how I thought it did. If one test fails, it actually skips some subsequent tests, and continues with others. If it actually worked the way I expected it to, "makeall all" would be a much more useful tool for testing. - Brian
