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 HAVE_BASIS2002 = false
90val POLYMLLIBDIR = ""
91val POLY = ""
92val POLYC = ""
93val POLY_VERSION = PolyML.Compiler.compilerVersionNumber
94val POLY_LDFLAGS = []
95val POLY_LDFLAGS_STATIC = []
96val CC = ""
97val OS = ""
98
99val DEPDIR = ""
100val GNUMAKE = ""
101val DYNLIB = ""
102val version = ""
103val ML_SYSNAME = ""
104val release = ""
105val DOT_PATH = ""
106val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"]
107
108val isUnix = true
109
110val pointer_eq = PolyML.pointerEq
111
112fun exec (x as (comm,args)) =
113    (* macos execv fails if the calling process is multi-threaded. *)
114    (* Can't lift the check out of the function body because of the value
115       restriction *)
116    if OS <> "macosx" then Posix.Process.exec x
117    else OS.Process.exit (systeml (comm::tl args))
118
119
120val build_log_dir = fullPath [HOLDIR, "tools-poly", "build-logs"]
121val build_log_file = fullPath [build_log_dir, "current-build-log"]
122val make_log_file = "current-make-log";
123val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY"
124
125fun base_interactive state scripts =
126    [POLY, "-q", "--use", fullPath [HOLDIR, "bin", "hol.ML"], state] @ scripts
127
128
129fun emit_hol_script target exe script =
130  let
131    val ostrm = TextIO.openOut target
132    fun output s = TextIO.output(ostrm, s)
133  in
134    output "#!/bin/sh\n";
135    output "# The bare HOL script\n";
136    output "# (automatically generated by HOL configuration)\n\n";
137    output (fullPath [HOLDIR, "bin", "buildheap"] ^
138            " --gcthreads=1 --repl --holstate=" ^ exe ^ " " ^
139            String.concatWith " " script ^ " \"$@\"\n");
140    TextIO.closeOut ostrm;
141    mk_xable target
142  end;
143
144  fun emit_hol_unquote_script target exe s =
145      let val ostrm = TextIO.openOut target
146          fun output s = TextIO.output(ostrm, s)
147          val qfilter = protect (fullPath [HOLDIR, "bin", "unquote"])
148          val script =
149            List.map (fn s => protect (fullPath [HOLDIR, "tools-poly", s]))
150                     s
151      in
152        output "#!/bin/sh\n";
153        output "# The HOL script (with quote preprocessing)\n";
154        output "# (automatically generated by HOL configuration)\n\n";
155        output (String.concatWith " "
156                   ([qfilter, "|"] @ base_interactive exe script) ^ "\n");
157        TextIO.closeOut ostrm;
158        mk_xable target
159      end;
160end (* local *)
161
162end; (* struct *)
163