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