1(* program to output iss file *)
2(* to compile this structure, cd to the tools directory, and
3     mosmlc -o make_iss.exe -I Holmake -I ..\sigobj basis2002.ui make_iss.sml
4*)
5structure make_iss = struct
6
7structure FileSys = OS.FileSys
8structure Process = OS.Process
9
10val holdir = Globals.HOLDIR
11val systeml = Systeml.systeml
12
13val sysname = Globals.release ^ " " ^ Int.toString Globals.version
14val sysname_lchyphen =
15    String.translate (fn #" " => "-" | c => str (Char.toLower c)) sysname
16val _ = print "Changing to hol directory\n"
17val _ = FileSys.chDir holdir
18
19fun normPath s = Path.toString(Path.fromString s)
20fun itstrings f [] = raise Fail "itstrings: empty list"
21  | itstrings f [x] = x
22  | itstrings f (h::t) = f h (itstrings f t);
23
24fun fullPath slist = normPath
25   (itstrings (fn chunk => fn path => Path.concat (chunk,path)) slist);
26
27fun die s = (print s; Process.exit Process.failure)
28
29val _ = FileSys.chDir holdir
30val _ = print "Removing unnecessary files: ";
31val _ = FileSys.remove (fullPath ["help", "HOL.Help"])
32    handle Interrupt => raise Interrupt | _ => ()
33val _ = print "help/HOL.Help, "
34val _ = (FileSys.chDir "help", FileSys.chDir "src-sml")
35val _ = systeml [fullPath [holdir, "bin", "Holmake"], "cleanAll"]
36val _ = print "cleanable stuff in help/src-sml\n\n"
37
38val _ = print "Compiling win-config.exe\n"
39val _ = FileSys.chDir (fullPath [holdir, "tools"])
40val _ = if Process.isSuccess
41             (systeml ["mosmlc", "-I", "Holmake", "-o", "win-config.exe",
42                       "win-config.sml"])
43        then ()
44        else (print "Compilation failed!\n"; Process.exit Process.failure)
45val _ = FileSys.chDir holdir
46
47
48val header = "\
49\; use the compile option (probably Control-F9) to compile this file\n\
50\; and create the HOL-install.exe executable in HOLDIR/Output\n\
51\[Setup]\n\
52\AppName            = HOL\n\
53\AppVerName         = HOL 4 - "^sysname^"\n\
54\AppVersion         = "^sysname^"\n\
55\AppUpdatesURL      = http://hol.sourceforge.net\n\
56\AppPublisher       = HOL Developers\n\
57\DefaultDirName     = {userdocs}\\Hol\n\
58\DefaultGroupName   = HOL\n\
59\Compression        = lzma/ultra\n\
60\SolidCompression   = true\n\
61\OutputBaseFilename = "^sysname_lchyphen^"-install\n";
62
63fun mem s [] = false | mem s (h::t) = s = h orelse mem s t
64
65fun traverse worklist acc excludes =
66  case worklist of
67    [] => acc
68  | (dir::rest) => let
69      open FileSys
70      val ds = openDir dir
71      fun alldirs filefound worklist =
72        case readDir ds of
73          NONE => (filefound, worklist)
74        | SOME f0 => let
75            val f = Path.concat(dir, f0)
76          in
77            if isDir f then
78              if not (mem f0 excludes) then
79                alldirs filefound (f::worklist)
80              else
81                alldirs filefound worklist
82            else alldirs true worklist
83          end
84      val (filefound, newworklist) = alldirs false rest
85      val _ = closeDir ds
86    in
87      traverse newworklist ((dir,filefound)::acc) excludes
88    end handle OS.SysErr(s,_) => die ("OS error: "^s)
89
90fun initial_directories excludes = let
91  open FileSys
92  val ds = openDir "."
93  fun readf filefound acc =
94    case readDir ds of
95      NONE => (filefound, acc)
96    | SOME f =>
97        if isDir f then
98          if not (mem f excludes) then
99            readf filefound (f::acc)
100          else
101            readf filefound acc
102        else readf true acc
103  val (filefound, result) = readf false []
104  val _ = closeDir ds
105in
106  (filefound, List.rev result)
107end handle OS.SysErr(s,_) => die ("OS error: "^s)
108
109fun alldirs excludes = let
110  val (filefound, ids) = initial_directories excludes
111in
112  (filefound, List.rev (traverse ids [] excludes))
113end handle OS.SysErr(s,_) => die ("OS error: "^s)
114
115fun trans #"/" = "\\" | trans x = str x
116fun dir_string dirname = String.concat ["Name: \"{app}\\",
117                                        String.translate trans dirname,
118                                        "\"\n"]
119fun file_string (dirname0, b) = let
120  val dirname = String.translate trans dirname0
121in
122  if b then
123    SOME (String.concat ["Source : \"", dirname, "\\*\"; DestDir : \"{app}\\",
124                         dirname, "\"\n"])
125  else NONE
126end
127
128val icon_section = "\
129\[Icons]\n\
130\Name : \"{group}\\HOL\" ; FileName : \"{app}\\bin\\hol.bat\" ; WorkingDir: \"{app}\"\n\
131\Name : \"{userdesktop}\\HOL\" ; FileName : \"{app}\\bin\\hol.bat\" ; WorkingDir: \"{app}\"\n"
132
133val run_section = "\
134\[Run]\n\
135\Filename: \"{app}\\tools\\win-config.exe\"; Parameters: \"\"\"{app}\"\"\"\n";
136
137val uninstall_delete_section =
138   "[UninstallDelete]\n\
139   \Type: filesandordirs; Name: \"{app}\\tools\"\n\
140   \Type: filesandordirs; Name: \"{app}\\help\"\n\
141   \Type: files; Name: \"{app}\\config-override\"\n"
142
143val _ = let
144  val (toplevelfiles, dirs) = alldirs [".HOLMK", "CVS"]
145  val outstream = TextIO.openOut "hol4.iss"
146  fun print s = TextIO.output(outstream, s)
147in
148  print header;
149  print "\n[Dirs]\n";
150  app print (map (dir_string o #1) dirs);
151  print "\n[Files]\n";
152  if toplevelfiles then print "Source : \"*\"; DestDir : \"{app}\"\n" else ();
153  app print (List.mapPartial file_string dirs);
154  print "\n";
155  print icon_section;
156  print "\n";
157  print run_section;
158  print "\n";
159  print uninstall_delete_section;
160  TextIO.closeOut outstream
161end handle OS.SysErr(s,_) => die ("OS error: "^s)
162
163val _ = print "Writing hol4.iss to HOLDIR\n\n"
164
165(* adjusting sigobj/SRCFILES *)
166val _ = let
167  val _ = print "Adjusting sigobj/SRCFILES ... "
168  val file = fullPath [holdir, "sigobj", "SRCFILES"]
169  val instrm = TextIO.openIn file
170  fun readlines acc =
171      case TextIO.inputLine instrm of
172        NONE => List.rev acc
173      | SOME s => readlines (s::acc)
174  val lines = readlines []
175  val _ = TextIO.closeIn instrm
176  fun adjustline s = String.extract(s,size holdir + 1,NONE)
177  val outstrm = TextIO.openOut file
178  val _ = app (fn s => TextIO.output(outstrm, adjustline s)) lines
179  val _ = TextIO.closeOut outstrm
180in
181  print "done\n"
182end
183
184end (* structure *)
185