1signature Systeml = 2sig 3 4 val systeml : string list -> OS.Process.status 5 val system_ps : string -> OS.Process.status 6 val systeml_out : {outfile:string} -> string list -> OS.Process.status 7 val exec : string * string list -> 'a 8 val protect : string -> string 9 val xable_string : string -> string 10 val mk_xable : string -> OS.Process.status 11 12(* first argument to these are the name of the desired executable, the 13 second is the name of the post-initialisation script to run. *) 14 val emit_hol_script : string -> string -> string list -> OS.Process.status 15 val emit_hol_unquote_script : string -> string -> string list -> 16 OS.Process.status 17 18 val find_my_path : unit -> string 19 20 (* configuration time constants *) 21 val HOLDIR : string 22 val POLYMLLIBDIR : string 23 val POLY : string 24 val POLYC : string 25 val POLY_VERSION : int 26 val POLY_LDFLAGS : string list 27 val POLY_LDFLAGS_STATIC : string list 28 val CC : string 29 val MOSMLDIR : string 30 val OS : string 31 val DEPDIR : string 32 val GNUMAKE : string 33 val DYNLIB : bool 34 val ML_SYSNAME : string 35 val DOT_PATH : string option 36 val DEFAULT_STATE : string 37 38 val isUnix : bool 39 val pointer_eq : 'a * 'a -> bool 40 val bindstr : string -> string 41 (* emits code that tries to quietly emulate the action of the argument 42 when fed to the compiler. For MoscowML, this is the identity function 43 (and it won't be quiet). *) 44 45 (* other system-wide constants, shared between build tools and the 46 running hol *) 47 val build_log_dir : string 48 val build_log_file : string 49 val make_log_file : string 50 val build_after_reloc_envvar : string 51 52 (* canonical source of version information *) 53 val release : string 54 val version : int 55 56end 57