HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Holmake -k fails if Holdep fails

Open AndreasLoow opened this issue 6 years ago • 4 comments

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?

AndreasLoow avatar Jun 25 '18 11:06 AndreasLoow

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

mn200 avatar Jun 27 '18 09:06 mn200

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.

AndreasLoow avatar Jun 27 '18 11:06 AndreasLoow

I think you're right that there is a reasonable behaviour here.

mn200 avatar Jun 27 '18 12:06 mn200

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.

formrre avatar Jan 07 '20 14:01 formrre