1(*---------------------------------------------------------------------------
2                An ML script for building HOL
3 ---------------------------------------------------------------------------*)
4
5structure build =
6struct
7
8structure Process = OS.Process
9
10(* utilities *)
11
12(* ----------------------------------------------------------------------
13    Magic to ensure that interruptions (SIGINTs) are actually seen by the
14    linked executable as Interrupt exceptions
15   ---------------------------------------------------------------------- *)
16
17prim_val catch_interrupt : bool -> unit = 1 "sys_catch_break";
18val _ = catch_interrupt true;
19
20open buildutils
21val _ = startup_check()
22
23(* ----------------------------------------------------------------------
24    Analysing the command-line
25   ---------------------------------------------------------------------- *)
26
27val cline_record = process_cline ()
28val {cmdline,build_theory_graph,selftest_level,...} = cline_record
29val {extra={SRCDIRS},jobcount,relocbuild,debug,...} = cline_record
30
31
32open Systeml;
33
34val Holmake = let
35  fun sysl p args = Systeml.systeml (p::args)
36  val isSuccess = OS.Process.isSuccess
37in
38  buildutils.Holmake sysl isSuccess
39                     (fn () => ["-j"^Int.toString jobcount] @
40                               (if debug then ["--dbg"] else []))
41                     (fn _ => "")
42                     selftest_level
43end
44
45(* ----------------------------------------------------------------------
46   Some useful file-system utility functions
47   ---------------------------------------------------------------------- *)
48
49(* create a symbolic link - Unix only *)
50fun link b s1 s2 =
51  let open Process
52  in if SYSTEML ["ln", "-s", s1, s2] then ()
53     else die ("Unable to link file "^quote s1^" to file "^quote s2^".")
54  end
55
56fun symlink_check() =
57    if OS = "winNT" then
58      die "Sorry; symbolic linking isn't available under Windows NT"
59    else link
60val default_link = if OS = "winNT" then cp else link
61
62fun mem x [] = false
63  | mem x (y::ys) = x = y orelse mem x ys
64
65fun exns_link exns b s1 s2 =
66  if mem (OS.Path.file s1) exns then () else default_link b s1 s2
67
68(*---------------------------------------------------------------------------
69        Transport a compiled directory to another location. The
70        symlink argument says whether this is via a symbolic link,
71        or by copying. The ".uo", ".ui", ".so", ".xable" and ".sig"
72        files are transported.
73 ---------------------------------------------------------------------------*)
74
75fun upload ((src, regulardir), target, symlink) =
76    if regulardir = 0 then
77      (print ("Uploading files to "^target^"\n");
78       map_dir (transfer_file symlink target) src)
79      handle OS.SysErr(s, erropt) =>
80             die ("OS error: "^s^" - "^
81                  (case erropt of SOME s' => OS.errorMsg s'
82                                | _ => ""))
83    else if selftest_level >= regulardir then
84      print ("Self-test directory "^src^" built successfully.\n")
85    else ()
86
87(*---------------------------------------------------------------------------
88    For each element in SRCDIRS, build it, then upload it to SIGOBJ.
89    This allows us to have the build process only occur w.r.t. SIGOBJ
90    (thus requiring only a single place to look for things).
91 ---------------------------------------------------------------------------*)
92
93fun buildDir symlink s =
94    (build_dir Holmake selftest_level s; upload(s,SIGOBJ,symlink));
95
96fun build_src symlink = List.app (buildDir symlink) SRCDIRS
97
98fun upload_holmake_files symlink =
99  upload ((fullPath[HOLDIR, "tools", "Holmake"], 0), SIGOBJ, symlink)
100
101val holmake_exns = [
102  "Systeml.sig", "Systeml.ui", "Systeml.uo"
103]
104
105
106fun build_hol symlink = let
107in
108  clean_sigobj();
109  setup_logfile();
110  upload_holmake_files (exns_link holmake_exns);
111  build_src symlink
112    handle Interrupt => (finish_logging false; die "Interrupted");
113  finish_logging true;
114  make_buildstamp();
115  build_help build_theory_graph;
116  print "\nHol built successfully.\n"
117end
118
119
120(*---------------------------------------------------------------------------
121       Get rid of compiled code and dependency information.
122 ---------------------------------------------------------------------------*)
123
124val check_againstB = check_against EXECUTABLE
125val _ = check_againstB "tools/smart-configure.sml"
126val _ = check_againstB "tools/configure.sml"
127val _ = check_againstB "tools/build.sml"
128val _ = check_againstB "tools/Holmake/Systeml.sig"
129val _ = check_againstB "tools/configure-mosml.sml"
130
131val _ = let
132  val fP = fullPath
133  open OS.FileSys
134  val hmake = fP [HOLDIR,"bin",xable_string "Holmake"]
135in
136  if access(hmake, [A_READ, A_EXEC]) then
137    app_sml_files (check_against hmake)
138                  {dirname = fP [HOLDIR, "tools", "Holmake"]}
139  else
140    die ("No Holmake executable in " ^ fP [HOLDIR, "bin"])
141end
142
143
144val _ =
145    case cmdline of
146      []            => build_hol default_link
147     | _ => die "Not implemented yet"
148
149end (* struct *)
150