[isabelle-dev] repos integrity
makarius at sketis.net
Fri Jun 19 14:53:12 CEST 2009
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
> 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
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
More information about the isabelle-dev