1(*---------------------------------------------------------------------------
2                An ML script for building HOL
3 ---------------------------------------------------------------------------*)
4
5structure build =
6struct
7
8open buildutils
9datatype phase = Initial | Bare | Full
10
11(* utilities *)
12
13  fun main () = let
14
15    val _ = startup_check()
16    val phase = ref Initial
17
18
19    open buildutils
20
21(* ----------------------------------------------------------------------
22    Analysing the command-line
23   ---------------------------------------------------------------------- *)
24
25val cline_record = process_cline ()
26val {cmdline,build_theory_graph,selftest_level,...} = cline_record
27val {debug,jobcount,relocbuild,extra={SRCDIRS,...},...} = cline_record
28val {multithread,...} = cline_record
29
30open Systeml;
31
32fun phase_extras () =
33  case !phase of
34    Initial => ["--poly_not_hol"]
35  | Bare => ["--holstate", fullPath [HOLDIR, "bin", "hol.state0"]]
36  | Full => []
37
38fun aug_systeml proc args = let
39  open Posix.Process
40  val env' =
41      "SELFTESTLEVEL="^Int.toString selftest_level :: Posix.ProcEnv.environ()
42in
43  case fork() of
44    NONE => (exece(proc,proc::args,env')
45             handle _ => die ("Exece of "^proc^" failed"))
46  | SOME cpid => let
47      val (_, result) = waitpid(W_CHILD cpid, [])
48    in
49      result
50    end
51end
52
53
54val Holmake = let
55  fun isSuccess Posix.Process.W_EXITED = true
56    | isSuccess _ = false
57  fun analysis hmstatus = let
58    open Posix.Process
59  in
60    case hmstatus of
61      W_EXITSTATUS w8 => "exited with code "^Word8.toString w8
62    | W_EXITED => "exited normally???"
63    | W_SIGNALED sg => "with signal " ^
64                       SysWord.toString (Posix.Signal.toWord sg)
65    | W_STOPPED sg => "stopped with signal " ^
66                      SysWord.toString (Posix.Signal.toWord sg)
67  end
68in
69  buildutils.Holmake aug_systeml isSuccess
70                     (fn () => ("-j"^Int.toString jobcount) ::
71                               ((if relocbuild then ["--relocbuild"] else []) @
72                                (if debug then ["--dbg"] else []) @
73                                (case multithread of
74                                     NONE => []
75                                   | SOME i => ["--mt="^Int.toString i]) @
76                                phase_extras()))
77                     analysis selftest_level
78end
79
80(* create a symbolic link - Unix only *)
81fun link b s1 s2 =
82    Posix.FileSys.symlink {new = s2, old = s1}
83    handle OS.SysErr (s, _) =>
84           die ("Unable to link old file "^quote s1^" to new file "
85                ^quote s2^": "^s)
86
87fun symlink_check() =
88    if OS = "winNT" then
89      die "Sorry; symbolic linking isn't available under Windows NT"
90    else link
91val default_link = if OS = "winNT" then cp else link
92
93(*---------------------------------------------------------------------------
94        Transport a compiled directory to another location. The
95        symlink argument says whether this is via a symbolic link,
96        or by copying. The ".uo", ".ui", ".so", ".xable" and ".sig"
97        files are transported.
98 ---------------------------------------------------------------------------*)
99
100fun upload ((src, regulardir), target, symlink) =
101    if regulardir = 0 then
102      (print ("Uploading files to "^target^"\n");
103       map_dir (transfer_file symlink target) src)
104      handle OS.SysErr(s, erropt) =>
105             die ("OS error: "^s^" - "^
106                  (case erropt of SOME s' => OS.errorMsg s'
107                                | _ => ""))
108    else if selftest_level >= regulardir then
109      print ("Self-test directory "^src^" built successfully.\n")
110    else ()
111
112(*---------------------------------------------------------------------------
113    For each element in SRCDIRS, build it, then upload it to SIGOBJ.
114    This allows us to have the build process only occur w.r.t. SIGOBJ
115    (thus requiring only a single place to look for things).
116 ---------------------------------------------------------------------------*)
117
118fun buildDir symlink s =
119  if #1 s = fullPath [HOLDIR, "bin/hol.bare"] then phase := Bare
120  else if #1 s = fullPath [HOLDIR, "bin/hol"] then phase := Full
121  else
122    (build_dir Holmake selftest_level s; upload(s,SIGOBJ,symlink))
123
124fun build_src symlink = List.app (buildDir symlink) SRCDIRS
125
126fun build_hol symlink = let
127in
128  clean_sigobj();
129  setup_logfile();
130  build_src symlink
131    handle SML90.Interrupt => (finish_logging false; die "Interrupted");
132  finish_logging true;
133  make_buildstamp();
134  build_help build_theory_graph;
135  print "\nHol built successfully.\n"
136end
137
138
139(*---------------------------------------------------------------------------
140       Get rid of compiled code and dependency information.
141 ---------------------------------------------------------------------------*)
142
143val check_againstB = check_against EXECUTABLE
144val _ = check_againstB "tools-poly/smart-configure.sml"
145val _ = check_againstB "tools-poly/configure.sml"
146val _ = check_againstB "tools-poly/build.sml"
147val _ = check_againstB "tools/Holmake/Systeml.sig"
148
149val _ = let
150  val fP = fullPath
151  open OS.FileSys
152  val hmake = fP [HOLDIR,"bin",xable_string "Holmake"]
153in
154  if access(hmake, [A_READ, A_EXEC]) then
155    (app_sml_files (check_against hmake)
156                   {dirname = fP [HOLDIR, "tools-poly", "Holmake"]};
157     app_sml_files (check_against hmake)
158                   {dirname = fP [HOLDIR, "tools", "Holmake"]})
159  else
160    die ("No Holmake executable in " ^ fP [HOLDIR, "bin"])
161end
162
163
164
165
166
167in
168    case cmdline of
169      []            => build_hol default_link
170    | _ => die "Multi-dir build not implemented yet"
171
172  end
173end (* struct *)
174