[isabelle-dev] repos integrity

[Makarius]

On Thu, 18 Jun 2009, Brian Huffman wrote:

> 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.

"isabelle makeall TARGETS" merely runs "isabelle make TARGET" in every 
"logic directory" -- this is a very ancient arrangement.  This means it 
stops after the first failure in each directory, but tries the other 
directories afterwards.  Since HOL and HOLCF are different "logics" in 
that sense, you get the above effect of continued HOLCF testing after some 
HOL session failed.


> 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.

This reminds me of the very old days of Isabelle development, when the 
makeall all was taking 8 hours on our fastest machine.

Are you running this on your old laptop?  Even on a very cheap iMac it now 
takes only 1-2 hours total.  Since you have an official account at TUM, 
you should be able to use macbroy20 .. 29 (which are SuSE Linux boxes). 
Hint: rsync your hg working directory before doing actual commits.


> 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.

Ever since Dec 1996, the Isabelle make system remembers the state of 
succesful sessions (via the log files).  So you merely need to iterate 
"isabelle makeall all" until a fixed point is reached.


> 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.

It is a bit more useful than expected, but still in dire need of 
renovation.  If you are fluent in Python, you can produce a more 
systematic test suite based on Mercurial, associating test reports with 
changeset ids on a persistent store that is incrementally refined by a 
semi-automatic process.  Moreover, the same could be done for AFP in 
relation to the main Isabelle repository, so that the changeset that has 
introduced a failure in AFP is automatically determined.


 	Makarius