[isabelle-dev] repos integrity

[Makarius]

On Thu, 18 Jun 2009, Brian Huffman wrote:

> "Normally make gives up immediately in this circumstance, returning a
> nonzero status. However, if the `-k' or `--keep-going' flag is
> specified, make continues to consider the other prerequisites of the
> pending targets, remaking them if necessary, before it gives up and
> returns nonzero status. For example, after an error in compiling one
> object file, `make -k' will continue compiling other object files even
> though it already knows that linking them will be impossible.

I did not know about this option yet, maybe it is relatively new (i.e. 
less than 20 years old).  It certainly looks promising in the remaining 
(short) time, where we still have IsaMakefiles in the first place. (There 
are many more problems caused by make, and it should be eliminated pretty 
soon.)


> It looks like "isabelle makeall all -k" will do exactly what I want. 
> Maybe the "makeall" script should be changed to use this option by 
> default?

Then we would start hardwiring special behaviour into isabelle make and 
makeall, but these are merely meant to pass through everything to the 
basic make on the particular platform (whatever that might be exactly). 
This very "ignorance" of isabelle make/makeall now allows to invoke that 
-k option in the first place.

BTW, you can always roll your own isabelle tools and put them into a place 
that is reachable via the ISABELLE_TOOLS setting (which is a colon 
separated list of directories, and can be configure in your 
~/.isabelle/etc/settings).


 	Makarius