Command sequence for installing HOL's OpenTheory packages

[binghe]

Before building HOL with --otknl, the opentheory command must be available and initialized (shell command: opentheory init), and the OT package "base-1.221" [1] must be already installed (shell command: opentheory update; opentheory install base).

[1] https://opentheory.gilith.com/?pkg=base-1.221

After the build completed (it takes a long time, say 10+ hours, with at leat 32GB memory (-j1), better 64GB (-j2)), the built OT packages must be installed locally (and possibly can be uploaded to OT repository, without any authentication!) so that other user code can be correctly exported. These packages must be installed in a correct order. Various Holmakefile has been modified with an install target which calls the actual opentheory install command with correct arguments, while the following toplevel command sequence gives their location and order:

install:
	cd $(HOLDIR)/src/boss;                       Holmake -j1 install
	cd $(HOLDIR)/src/res_quan/src;               Holmake -j1 install
	cd $(HOLDIR)/src/quotient/src;               Holmake -j1 install
	cd $(HOLDIR)/src/sort;                       Holmake -j1 install
	cd $(HOLDIR)/src/string;                     Holmake -j1 install
	cd $(HOLDIR)/src/n-bit;                      Holmake -j1 install
	cd $(HOLDIR)/src/ring/src;                   Holmake -j1 install
	cd $(HOLDIR)/src/integer;                    Holmake -j1 install
	cd $(HOLDIR)/src/pred_set/src/more_theories; Holmake -j1 install
	cd $(HOLDIR)/src/real;                       Holmake -j1 install
	cd $(HOLDIR)/src/real/analysis;              Holmake -j1 install
	cd $(HOLDIR)/src/probability;                Holmake -j1 install
	cd $(HOLDIR)/src/bag;                        Holmake -j1 install
	cd $(HOLDIR)/src/finite_maps;                Holmake -j1 install
	cd $(HOLDIR)/src/coalgebras;                 Holmake -j1 install
	cd $(HOLDIR)/src/floating-point;             Holmake -j1 install
	cd $(HOLDIR)/src/monad/more_monads;          Holmake -j1 install

The problem is that, I don't know where to put the above Makefile fragment into HOL code base. And I know it's not a good style to call Holmake command in a nested way. Anyway, I hope, by calling bin/build --otknl --install (or something similar) after the build, the above commands (or something equivalent) can be executed in the same order. Can this be implemented (by HOL maintainer), or I can have some hints on how to do it?

--Chun

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