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
