Command sequence for installing HOL's OpenTheory packages

[binghe]

Command sequence for installing HOL's OpenTheory packages

[mn200]

Holmake "calls itself recursively" automatically: I'd try having a line like

install: $(patsubst %,../src/%/install,$(OTDIRS))

and with a definition of OTDIRS along the lines of

OTDIRS = bag integer pred_set-src/more_theories coalgebras ...

If there are dependencies between the various install targets (you say something about "the correct order" above), this can be recorded by inserting those dependencies into the Holmakefiles.

[binghe]

Thanks for your hints, but how can Holmake interpret $(patsubst %,../../%/install,$(OTDIRS)), which becomes something like /Users/binghe/ML/HOL.otknl/src/boss/install as the "install" target of the Holmakefile under /Users/binghe/ML/HOL.otknl/src/boss, instead of a literal file named install there?

When I put the toplevel "install" target into $(HOLDIR)/src/parallel_builds/core/Holmakefile with all necessary dependencies added into the "install" target of each related Holmakefile, eventually I got this message say Don't know how to build necessary target(s): /Users/binghe/ML/HOL.otknl/src/boss/install

~/ML/HOL.otknl/src/parallel_builds/core$ Holmake -j1 install
Holmake: *** Switching to execute /Users/binghe/ML/HOL.otknl/bin/Holmake
Holmake: *** (As we are in/under its HOLDIR)
Holmake: Scanned 31 directories
Holmake: Don't know how to build necessary target(s): /Users/binghe/ML/HOL.otknl/src/boss/install
Holmake failed with exception: Fail: MLton.Exit.exit(256): exit must have 0 <= status < 256
unhandled exception: Fail: MLton.Exit.exit
Top-level handler raised exception.

[mn200]

I admit that I hadn’t checked the behaviour on phony targets but I did think this should work. The workaround of having indicator files should definitely work—nice idea.