[isabelle-dev] repos integrity

[Brian Huffman]

On Thu, Jun 18, 2009 at 2:56 PM, Makarius<makarius at sketis.net> wrote:
> "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.

A quick Google search found the following bit of documentation about gnu make:

http://www.gnu.org/software/automake/manual/make/Errors.html

"When an error happens that make has not been told to ignore, it
implies that the current target cannot be correctly remade, and
neither can any other that depends on it either directly or
indirectly. No further commands will be executed for these targets,
since their preconditions have not been achieved.

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

"The usual behavior assumes that your purpose is to get the specified
targets up to date; once make learns that this is impossible, it might
as well report the failure immediately. The `-k' option says that the
real purpose is to test as many of the changes made in the program as
possible, perhaps to find several independent problems so that you can
correct them all before the next attempt to compile."

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?

- Brian