HOL
HOL copied to clipboard
Holmake -k fails if Holdep fails
Consider the following Holmake invocation:
> Holmake -k
Working in $(HOLDIR)/examples/balanced_bst
[...]
Working in .
Holdep failed: tinyMachineScript.sml 469.66 Unescaped newline in string literal
Holmake failed with exception: HolDepFailed
Would it be possible for Holmake to ignore Holdep errors and continue working anyway when the -k flag is included?
In general, it shouldn't because the failure of the dependency analysis means that Holmake doesn't have a correct picture of what the dependency graph is, and it is this that determines what should or shouldn't be built. On the other hand, there probably are circumstances when we might be able to know when things can be done regardless...
On the third hand, failures such as these should be trivial to fix...
My naive hope was that not having "a correct picture" would simply mean that some subtree of the dependency graph (more specifically, the files, and the dependencies of the files (if not something analyzable by Holdep also depends on those files), that Holdep cannot analyze) would be skipped. If nothing depends on the files that were unanalyzable by Holdep, then things should still work. But if this is not true, or if it's a non-trivial change, then it might not be worth implementing.
I think you're right that there is a reasonable behaviour here.
I want to note that these failures are quite prevalent when resolving merge conflicts, sometimes picking the correct resolution is tricky, and a sensible thing is to build conflicting file's dependencies individually. Running Holmake depTheory.uo
breaks on git's >>>>>>>
markers anywhere in the directory and then I either need to build dependencies by hand or move files around, which is error prone.