1structure Systeml :> Systeml = struct
2
3(* This is the UNIX implementation of the Systeml functionality.  It is the
4   very first thing compiled by the HOL build process so it absolutely
5   can not depend on any other HOL source code. *)
6
7structure Path =  OS.Path
8structure Process = OS.Process
9structure FileSys = OS.FileSys
10
11local
12  open Process
13  fun concat_wspaces munge strl = String.concatWith " " (map munge strl)
14in
15
16  val unix_meta_chars = [#"'", #"\"", #"|", #" ", #">", #"\t", #"\n", #"<",
17                         #"\\", #"#"]
18  fun is_meta c = List.exists (fn y => c = y) unix_meta_chars
19  fun is_meta_string(s,i) = if i >= size s then false
20                            else if is_meta (String.sub(s,i)) then true
21                            else is_meta_string(s, i + 1)
22  fun unix_trans c = if is_meta c then "\\" ^ str c else str c
23
24  fun protect s = if is_meta_string(s,0) then String.translate unix_trans s
25                  else s
26
27  val systeml = system o concat_wspaces protect
28
29  fun systeml_out {outfile} c =
30    system (concat_wspaces protect c ^ " > " ^ protect outfile ^ " 2>&1")
31
32  val system_ps = Process.system
33  (* see winNT-systeml.sml for an explanation of why what is a synonym under
34     unix needs to be slightly different on Windows. *)
35
36  (* would like to be using Posix.Process.exec, but this seems flakey on
37     various machines (and is entirely unavailable on Moscow ML) *)
38  fun exec (comm, args) = OS.Process.exit (systeml (comm::tl args))
39
40  fun get_first f [] = NONE
41    | get_first f (h::t) = case f h of NONE => get_first f t
42                                     | x => x
43
44
45  fun find_my_path () = let
46    (* assumes directory hasn't been changed yet *)
47    val myname = CommandLine.name()
48    val {dir,file} = Path.splitDirFile myname
49  in
50    if dir = "" then let
51        val pathdirs = String.tokens (fn c => c = #":")
52                                     (valOf (Process.getEnv "PATH"))
53        open FileSys
54        fun checkdir d = let
55          val f = Path.concat(d,file)
56        in
57          if access(f, [A_READ, A_EXEC]) then SOME f else NONE
58        end
59      in
60        valOf (get_first checkdir pathdirs)
61      end
62    else
63      Path.mkAbsolute {path = myname,relativeTo = FileSys.getDir()}
64  end
65
66  fun xable_string s = s
67
68  fun mk_xable file =
69    let
70      val r = systeml ["chmod", "a+x", file]
71    in
72      if Process.isSuccess r then r
73      else if FileSys.access (file,[FileSys.A_EXEC]) then
74          (* if we can execute it, then continue with a warning *)
75          (* NB: MoSML docs say FileSys.access uses real uid/gid, not effective uid/gid,
76             so this test may be bogus if we are setuid.  This is unlikely(!). *)
77          (print ("Non-fatal warning: couldn't set world execute permission on "^file^",\n  but continuing anyway since at least the current user has execute permission.\n");
78           OS.Process.success)
79      else (print ("unable to set execute permission on "^file^".\n");
80            OS.Process.failure)
81    end
82
83
84fun normPath s = Path.toString(Path.fromString s)
85
86fun fullPath slist =
87    normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1))
88                         (hd slist) (tl slist))
89
90
91(* these values are filled in by configure.sml *)
92val HOLDIR = ""
93val MOSMLDIR = ""
94val OS = ""
95val POLY = ""
96val POLYC = ""
97val POLY_VERSION = 0
98val POLYMLLIBDIR = ""
99val POLY_LDFLAGS = []
100val POLY_LDFLAGS_STATIC = []
101val CC = ""
102
103val DEPDIR = ""
104val GNUMAKE = ""
105val DYNLIB = ""
106val version = ""
107val ML_SYSNAME = ""
108val release = ""
109val DOT_PATH = ""
110val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"]
111
112val isUnix = true
113local val cast : 'a -> int = Obj.magic
114in
115  fun pointer_eq (x:'a, y:'a) = (cast x = cast y)
116end
117
118val build_log_dir = fullPath [HOLDIR, "tools", "build-logs"]
119val build_log_file = fullPath [build_log_dir, "current-build-log"]
120val make_log_file = "current-make-log"
121val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY"
122
123
124fun emit_hol_script target qend _ = let
125  val ostrm = TextIO.openOut target
126  fun output s = TextIO.output(ostrm, s)
127  val sigobj = protect (fullPath [HOLDIR, "sigobj"])
128  val std_prelude = protect (fullPath [HOLDIR, "std.prelude"])
129  val mosml = protect (fullPath [MOSMLDIR, "mosml"])
130in
131  output "#!/bin/sh\n";
132  output "# The bare HOL script\n";
133  output "# (automatically generated by HOL configuration)\n\n";
134  output (String.concat[mosml," -quietdec -P full -I ", sigobj, " ",
135                        std_prelude, " $* ", protect qend, "\n"]);
136  TextIO.closeOut ostrm;
137  mk_xable target
138end
139
140
141fun emit_hol_unquote_script target qend _ = let
142  val ostrm = TextIO.openOut target
143  fun output s = TextIO.output(ostrm, s)
144  val qfilter = protect (fullPath [HOLDIR, "bin", "unquote"])
145  val sigobj = protect (fullPath [HOLDIR, "sigobj"])
146  val std_prelude = protect (fullPath [HOLDIR, "std.prelude"])
147  val mosml = protect (fullPath [MOSMLDIR, "mosml"])
148  val qinit =
149      protect (fullPath [HOLDIR, "tools", "unquote-init.sml"])
150in
151  output "#!/bin/sh\n";
152  output "# The HOL script (with quote preprocessing)\n";
153  output "# (automatically generated by HOL configuration)\n\n";
154  output  (String.concat [qfilter, " | ", mosml," -quietdec -P full -I ",
155                          sigobj, " ", std_prelude, " ", qinit,
156                          " $* ", protect qend, "\n"]);
157  TextIO.closeOut ostrm;
158  mk_xable target
159end
160end (* local *)
161
162fun bindstr s = s
163
164end; (* struct *)
165