1# This file specifies the sequence of directories that the build 2# program builds. Each non-comment, non-blank line specifies a 3# directory which will be visited by the build program. Directories 4# that are not absolute are interpreted with respect to the root of 5# the HOL directory. Build is special-cased so that some directories 6# are treated differently, but the default behaviour is that in each, 7# it will call Holmake --qof. 8 9# The **KERNEL** line stands for the directory containing the sytem's 10# kernel, which may be selected as a command-line option to the build 11# command (the possibilities are src/0, src/experimental-kernel, or 12# src/logging-kernel as of 10 August 2012). 13 14# Comments can be added; all text on a line after a # symbol is 15# ignored. Similarly blank lines are ignored. If you are going to 16# edit this file, be aware that it does not record various 17# dependencies between the directories. If dir1 is earlier than dir2, 18# then dir1 can not depend on dir2, but if dir1 is later than dir2, 19# then it may or may not depend on dir2. 20 21# If a directory name is preceded by an !, then it will only be built 22# if the -selftest flag is passed to Holmake, and the object files 23# that it builds will not be transferred to the sigobj directory. If 24# there is more than one ! then the number of them indicates the level 25# of -selftest required in order to get that directory to be built at 26# all. (If -selftest appears on its own, then that's level 1. If you 27# write -selftest 2, that's level 2, which means directories with 2 !s 28# will get tested.) 29 30# If a directory name is preceded by a string inside []-brackets, then 31# that directory/target will only be considered if the string is the 32# name of the current ML implementation. Thus the line [poly]foo 33# will cause foo to be built only if the current implementation is 34# Poly/ML. (The other supported implementation at the time of writing 35# is [mosml].) 36# 37# If a directory name is preceded by a string inside ()-brackets, then 38# that directory/target will only be considered if the string is the 39# name of the current kernel. Thus the line (otknl)foo will cause foo to 40# be built only if the current kernel is otknl. (The other supported 41# kernels at the time of writing are stdknl and expk.) 42# 43# If combining these annotations, the required order is [system] then 44# (kernel) then test level. Thus [mosml]!!foo, not !![mosml]foo, and 45# [poly](otknl)!foo, not (otknl)[poly]!foo. 46# 47# Finally if a line begins with "#include" (without the quotes), then 48# the file specified after the include directive is loaded and treated 49# the same as if its contents had been inserted into the main file. 50# Those files may include other #include directives. If the file is 51# specified with a relative path, then it���s relative to HOLDIR/tools 52# (the directory containing this file). 53 54#include sequences/kernel 55#include sequences/core-theories 56#include sequences/more-theories 57#include sequences/large-theories 58 59# 60# Examples only from here on 61# 62 63#include sequences/final-examples 64