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 what Holmake does.
regards,
Konrad.
On Wed, Jul 15, 2015 at 8:25 AM, Makarius wrote:
> 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 abstractly, but I
> want to get the resulting sequences of ML files. I've looked around
> tools/build.sml and tools/buildutils.sml a bit, and it ultimately seems to
> converge towards Holmake invocations.
>
> The latter is unclear to me. Which are typical targets, e.g. for the
> kernel or core theories? Maybe there is even some Holmake command line
> option to ask for used file dependencies of such targets?
>
>
> Makarius
>
>
> --
> Don't Limit Your Business. Reach for the Cloud.
> GigeNET's Cloud Solutions provide you with the tools and support that
> you need to offload your IT needs and focus on growing your business.
> Configured For All Businesses. Start Your Cloud Today.
> https://www.gigenetcloud.com/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Don't Limit Your Business. Reach for the Cloud.
GigeNET's Cloud Solutions provide you with the tools and support that
you need to offload your IT needs and focus on growing your business.
Configured For All Businesses. Start Your Cloud Today.
https://www.gigenetcloud.com/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
