Re: [Hol-info] HOL4 build, deps etc.

2015-07-15 Thread Konrad Slind
Quick and superficial answer: A tool called Holdep computes the dependencies by a quick syntacctic analysis of the ML files in the current directory. It then the dependencies in a sub-directory called .HOLMK. Section 6.3 in the Description part of the Manual gives a detailed description of

[Hol-info] HOL4 build, deps etc.

2015-07-15 Thread Makarius
Dear HOL4 experts, I am trying to understand HOL4 build management. After some initial struggles, I have managed to make a regular build of everything via bin/build. Now I want to see which sources are used in which canonical order. The file tools/build-sequence appears to specify that