[isabelle-dev] repos integrity

[Brian Huffman]

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