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  fun systeml_out {outfile} c =
29    system (concat_wspaces protect c ^ " > " ^ protect outfile ^ " 2>&1")
30
31  fun get_first f [] = NONE
32    | get_first f (h::t) = case f h of NONE => get_first f t
33                                     | x => x
34
35
36  fun find_my_path () = let
37    (* assumes directory hasn't been changed yet *)
38    val myname = CommandLine.name()
39    val {dir,file} = Path.splitDirFile myname
40  in
41    if dir = "" then let
42        val pathdirs = String.tokens (fn c => c = #":")
43                                     (valOf (Process.getEnv "PATH"))
44        open FileSys
45        fun checkdir d = let
46          val f = Path.concat(d,file)
47        in
48          if access(f, [A_READ, A_EXEC]) then SOME f else NONE
49        end
50      in
51        valOf (get_first checkdir pathdirs)
52      end
53    else
54      Path.mkAbsolute {path = myname, relativeTo = FileSys.getDir()}
55  end
56
57  val system_ps = Process.system
58  (* see winNT-systeml.sml for an explanation of why what is a synonym under
59     unix needs to be slightly different on Windows. *)
60
61  fun xable_string s = s
62
63  fun mk_xable file =
64    let
65      val r = systeml ["chmod", "a+x", file]
66    in
67      if Process.isSuccess r then r
68      else if FileSys.access (file,[FileSys.A_EXEC]) then
69          (* if we can execute it, then continue with a warning *)
70          (* NB: MoSML docs say FileSys.access uses real uid/gid, not effective uid/gid,
71             so this test may be bogus if we are setuid.  This is unlikely(!). *)
72          (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");
73           OS.Process.success)
74      else (print ("unable to set execute permission on "^file^".\n");
75            OS.Process.failure)
76    end
77
78
79fun normPath s = Path.toString(Path.fromString s)
80
81fun fullPath slist =
82    normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1))
83                         (hd slist) (tl slist))
84
85
86(* these values are filled in by configure.sml *)
87val HOLDIR = ""
88val MOSMLDIR = ""
89val POLYMLLIBDIR = ""
90val POLY = ""
91val POLYC = ""
92val POLY_VERSION = PolyML.Compiler.compilerVersionNumber
93val POLY_LDFLAGS = []
94val POLY_LDFLAGS_STATIC = []
95val CC = ""
96val OS = ""
97
98val DEPDIR = ""
99val GNUMAKE = ""
100val DYNLIB = ""
101val version = ""
102val ML_SYSNAME = ""
103val release = ""
104val DOT_PATH = ""
105val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"]
106
107val isUnix = true
108
109val pointer_eq = PolyML.pointerEq
110
111fun exec (x as (comm,args)) =
112    (* macos execv fails if the calling process is multi-threaded. *)
113    (* Can't lift the check out of the function body because of the value
114       restriction *)
115    if OS <> "macosx" then Posix.Process.exec x
116    else OS.Process.exit (systeml (comm::tl args))
117
118
119val build_log_dir = fullPath [HOLDIR, "tools-poly", "build-logs"]
120val build_log_file = fullPath [build_log_dir, "current-build-log"]
121val make_log_file = "current-make-log";
122val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY"
123
124fun base_interactive state scripts =
125    [POLY, "-q", "--use", fullPath [HOLDIR, "bin", "hol.ML"], state] @ scripts
126
127
128fun emit_hol_script target exe script =
129  let
130    val ostrm = TextIO.openOut target
131    fun output s = TextIO.output(ostrm, s)
132  in
133    output "#!/bin/sh\n";
134    output "# The bare HOL script\n";
135    output "# (automatically generated by HOL configuration)\n\n";
136    output (fullPath [HOLDIR, "bin", "buildheap"] ^
137            " --gcthreads=1 --repl --holstate=" ^ exe ^ " " ^
138            String.concatWith " " script ^ " \"$@\"\n");
139    TextIO.closeOut ostrm;
140    mk_xable target
141  end;
142
143  fun emit_hol_unquote_script target exe s =
144      let val ostrm = TextIO.openOut target
145          fun output s = TextIO.output(ostrm, s)
146          val qfilter = protect (fullPath [HOLDIR, "bin", "unquote"])
147          val script =
148            List.map (fn s => protect (fullPath [HOLDIR, "tools-poly", s]))
149                     s
150      in
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.concatWith " "
155                   ([qfilter, "|"] @ base_interactive exe script) ^ "\n");
156        TextIO.closeOut ostrm;
157        mk_xable target
158      end;
159end (* local *)
160
161fun bindstr mlcode =
162    "val _ = CompilerSpecific.quietbind \"" ^ String.toString mlcode ^ "\""
163
164end; (* struct *)
165