1structure HM_Core_Cline :> HM_Core_Cline = 2struct 3 4local 5 open FunctionalRecordUpdate 6 fun makeUpdateT z = makeUpdate22 z 7in 8fun updateT z = let 9 fun from debug do_logging fast help hmakefile holdir includes 10 interactive jobs keep_going no_action no_hmakefile no_lastmaker_check 11 no_overlay 12 no_prereqs opentheory quiet 13 quit_on_failure rebuild_deps recursive_build recursive_clean 14 verbose = 15 { 16 debug = debug, do_logging = do_logging, 17 fast = fast, help = help, hmakefile = hmakefile, holdir = holdir, 18 includes = includes, interactive = interactive, jobs = jobs, 19 keep_going = keep_going, 20 no_action = no_action, no_hmakefile = no_hmakefile, 21 no_lastmaker_check = no_lastmaker_check, no_overlay = no_overlay, 22 no_prereqs = no_prereqs, opentheory = opentheory, 23 quiet = quiet, quit_on_failure = quit_on_failure, 24 rebuild_deps = rebuild_deps, recursive_build = recursive_build, 25 recursive_clean = recursive_clean, verbose = verbose 26 } 27 fun from' verbose recursive_clean recursive_build rebuild_deps quit_on_failure 28 quiet opentheory 29 no_prereqs 30 no_overlay no_lastmaker_check no_hmakefile no_action keep_going 31 jobs interactive 32 includes holdir 33 hmakefile help fast do_logging debug = 34 { 35 debug = debug, do_logging = do_logging, 36 fast = fast, help = help, hmakefile = hmakefile, holdir = holdir, 37 includes = includes, interactive = interactive, jobs = jobs, 38 keep_going = keep_going, 39 no_action = no_action, no_hmakefile = no_hmakefile, 40 no_lastmaker_check = no_lastmaker_check, no_overlay = no_overlay, 41 no_prereqs = no_prereqs, opentheory = opentheory, 42 quiet = quiet, quit_on_failure = quit_on_failure, 43 rebuild_deps = rebuild_deps, recursive_build = recursive_build, 44 recursive_clean = recursive_clean, verbose = verbose 45 } 46 fun to f {debug, do_logging, fast, help, hmakefile, holdir, 47 includes, interactive, jobs, keep_going, no_action, no_hmakefile, 48 no_lastmaker_check, 49 no_overlay, no_prereqs, opentheory, 50 quiet, quit_on_failure, rebuild_deps, recursive_build, 51 recursive_clean, verbose} = 52 f debug do_logging fast help hmakefile holdir includes 53 interactive jobs keep_going no_action no_hmakefile no_lastmaker_check 54 no_overlay 55 no_prereqs opentheory quiet 56 quit_on_failure rebuild_deps recursive_build recursive_clean verbose 57in 58 makeUpdateT (from, from', to) 59end z 60val U = U 61val $$ = $$ 62end (* local *) 63 64fun fupd_jobs f t = updateT t (U #jobs (f (#jobs t))) $$ 65fun fupd_includes f t = updateT t (U #includes (f (#includes t))) $$ 66 67type t = { 68 debug : {ins : string list, outs : string list} option, 69 do_logging : bool, 70 fast : bool, 71 help : bool, 72 hmakefile : string option, 73 holdir : string option, 74 includes : string list, 75 interactive : bool, 76 jobs : int, 77 keep_going : bool, 78 no_action : bool, 79 no_hmakefile : bool, 80 no_lastmaker_check : bool, 81 no_overlay : bool, 82 no_prereqs : bool, 83 opentheory : string option, 84 quiet : bool, 85 quit_on_failure : bool, 86 rebuild_deps : bool, 87 recursive_build : bool, 88 recursive_clean : bool, 89 verbose : bool 90} 91 92val default_core_options : t = 93{ 94 debug = NONE, 95 do_logging = false, 96 fast = false, 97 help = false, 98 hmakefile = NONE, 99 holdir = NONE, 100 includes = [], 101 interactive = false, 102 jobs = 4, 103 keep_going = false, 104 no_action = false, 105 no_hmakefile = false, 106 no_lastmaker_check = false, 107 no_overlay = false, 108 no_prereqs = false, 109 opentheory = NONE, 110 quiet = false, 111 quit_on_failure = true, 112 rebuild_deps = false, 113 recursive_build = false, 114 recursive_clean = false, 115 verbose = false 116} 117 118type 'a cline_result = 119 { update: (string -> unit) * 'a -> 'a, 120 hmakefile : string option, 121 no_hmf : bool } 122 123fun resfn f : t cline_result = {update = f, hmakefile = NONE, no_hmf = false} 124 125open GetOpt 126val setNOHMF = 127 NoArg (fn () => {update = fn (wn,t) => updateT t (U #no_hmakefile true) $$, 128 hmakefile = NONE, no_hmf = true}) 129fun mkBoolT sel = 130 NoArg (fn () => resfn (fn (wn,t) => updateT t (U sel true) $$)) 131fun mkBoolF sel = 132 NoArg (fn () => resfn (fn (wn,t) => updateT t (U sel false) $$)) 133fun cons_includes x = 134 resfn (fn (wn,t) => updateT t (U #includes (x :: #includes t)) $$) 135fun change_jobs nstr = 136 resfn (fn (wn,t) => 137 case Int.fromString nstr of 138 NONE => (wn ("Couldn't parse "^nstr^ 139 " as a number; ignoring it"); t) 140 | SOME n => if n < 1 then 141 (wn "Ignoring non-positive job count"; t) 142 else updateT t (U #jobs n) $$) 143 144fun set_hmakefile s = 145 { update = fn (wn,t) => 146 (if isSome (#hmakefile t) then 147 wn "Multiple Holmakefile specs; ignoring earlier spec" 148 else (); 149 updateT t (U #hmakefile (SOME s)) $$), 150 hmakefile = SOME s, no_hmf = false } 151fun set_holdir s = 152 resfn (fn (wn, t) => 153 (if isSome (#holdir t) then 154 wn "Multiple holdir specs; ignoring earlier spec" 155 else (); 156 updateT t (U #holdir (SOME s)) $$)) 157fun set_openthy s = 158 resfn (fn (wn, t) => 159 (if isSome (#opentheory t) then 160 wn "Multiple opentheory specs; ignoring earlier spec" 161 else (); 162 updateT t (U #opentheory (SOME s)) $$)) 163fun addDbg sopt = 164 resfn (fn (wn, t) => 165 let 166 fun process (x as {ins,outs}) sopt = 167 case sopt of 168 NONE => SOME x 169 | SOME s => 170 if String.sub(s,0) = #"-" then 171 if size s > 1 then 172 SOME{ins=ins, 173 outs = String.extract(s,1,NONE) :: outs} 174 else (wn "Ignoring bogus -d- option"; SOME x) 175 else 176 SOME{ins = s::ins, outs = outs} 177 val newvalue = 178 case #debug t of 179 NONE => process {ins=[],outs=[]} sopt 180 | SOME x => process x sopt 181 in 182 updateT t (U #debug newvalue) $$ 183 end) 184 185val core_option_descriptions = [ 186 { help = "turn on diagnostic messages", long = ["dbg"], short = "d", 187 desc = OptArg (addDbg, "diag-cat")}, 188 { help = "fast build (replace tactics w/cheat)", long = ["fast"], short = "", 189 desc = mkBoolT #fast }, 190 { help = "show this message", long = ["help"], short = "h", 191 desc = mkBoolT #help }, 192 { help = "use different HOLDIR", long = ["holdir"], short = "", 193 desc = ReqArg (set_holdir, "directory") }, 194 { help = "use different holmakefile", long = ["holmakefile"], short = "", 195 desc = ReqArg (set_hmakefile, "file") }, 196 { help = "make session 'interactive'", long = ["interactive"], short = "i", 197 desc = mkBoolT #interactive }, 198 { help = "include directory", long = [], short = "I", 199 desc = ReqArg (cons_includes, "directory") }, 200 { help = "max number of parallel jobs", long = ["jobs"], short = "j", 201 desc = ReqArg (change_jobs, "n") }, 202 { help = "try to build all targets", long = ["keep-going"], short = "k", 203 desc = mkBoolT #keep_going }, 204 { help = "enable time logging", long = ["logging"], short = "", 205 desc = mkBoolT #do_logging }, 206 { help = "print what would be executed", long = ["no_action"], short = "n", 207 desc = mkBoolT #no_action }, 208 { help = "don't use a Holmakefile", long = ["no_hmakefile"], short = "", 209 desc = setNOHMF }, 210 { help = "don't check which Holmake was last used", long = ["nolmbc"], 211 short = "", desc = mkBoolT #no_lastmaker_check }, 212 { help = "don't use Overlay.sml file", long = ["no_overlay"], 213 short = "", desc = mkBoolT #no_overlay }, 214 { help = "don't build recursively in INCLUDES", 215 long = ["no_prereqs"], short = "", desc = mkBoolT #no_prereqs }, 216 { help = "don't quit on failure", long = ["noqof"], short = "", 217 desc = mkBoolF #quit_on_failure }, 218 { help = "use file as opentheory logging .uo", 219 long = ["ot"], short = "", desc = ReqArg (set_openthy, "file")}, 220 { help = "be quieter with output", short = "q", long = ["quiet"], 221 desc = NoArg 222 (fn () => 223 resfn (fn (wn,t) => 224 (if #verbose t then 225 wn "Quiet and verbose incompatible; \ 226 \taking verbose" 227 else () ; 228 updateT t (U #quiet true) $$))) }, 229 { help = "quit on failure", short = "", long = ["qof"], 230 desc = mkBoolT #quit_on_failure }, 231 { help = "rebuild cached dependency files", short = "", 232 long = ["rebuild_deps"], desc = mkBoolT #rebuild_deps }, 233 { help = "both --recursive-{build,clean}", short = "r", long = [], 234 desc = NoArg ( 235 fn () => resfn ( 236 fn (wn,t) => updateT t 237 (U #recursive_build true) 238 (U #recursive_clean true) $$ 239 ) 240 )}, 241 { help = "build all targets recursively", short = "", 242 long = ["recursive-build"], desc = mkBoolT #recursive_build}, 243 { help = "clean recursively", short = "", 244 long = ["recursive-clean"], desc = mkBoolT #recursive_clean}, 245 { help = "verbose output", short = "v", long = ["verbose"], 246 desc = NoArg 247 (fn () => 248 resfn (fn (wn,t) => 249 (if #quiet t then 250 wn "Quiet and verbose incompatible; \ 251 \taking verbose" 252 else (); 253 updateT t (U #verbose true) $$))) } 254] 255 256fun descr_key (d:'a GetOpt.opt_descr) = 257 str (String.sub(#short d, 0)) 258 handle Subscript => hd (#long d) handle Empty => "" 259 260fun descr_compare (d1, d2) = String.compare(descr_key d1, descr_key d2) 261 262fun sort_descriptions dl = Listsort.sort descr_compare dl 263 264 265end 266