let stdlibdir = datadir // "stdlib"
let prelude_gl_file = stdlibdir // "prelude.gl"
let prelude_sh_file = stdlibdir // "prelude.sh"
-let () =
+
+let debug_flag = ref false
+let directory = ref "."
+let input_file = ref "Goalfile"
+let includes = ref [stdlibdir]
+let add_include dir = includes := dir :: !includes
+let nr_jobs = ref 4 (* XXX use nproc *)
+let use_prelude = ref true
+
+let parse () =
if not (is_directory stdlibdir) || not (Sys.file_exists prelude_gl_file) then
failwithf "%s: cannot find the standard library directory, expected %s. If the standard library directory is in a non-standard location then set GOALS_DATADIR. If you can trying to run goals from the build directory then use ‘./run goals ...’"
- Sys.executable_name stdlibdir
-
-let input_file,
- debug_flag, directory, includes, nr_jobs, use_prelude, anon_vars, targets =
- let args = ref [] in
- let debug_flag = ref false in
- let directory = ref "." in
- let input_file = ref "Goalfile" in
- let includes = ref [stdlibdir] in
- let add_include dir = includes := dir :: !includes in
- let nr_jobs = ref 4 (* XXX use nproc *) in
- let use_prelude = ref true in
+ Sys.executable_name stdlibdir;
let argspec = [
"-C", Arg.Set_string directory,
" Print version and exit";
] in
let argspec = Arg.align argspec in
+ let args = ref [] in
let anon_fun s = args := s :: !args in
Arg.parse argspec anon_fun usage;
- let args = List.rev !args in
- let debug_flag = !debug_flag in
- let directory = !directory in
- let input_file = !input_file in
- (* Don't reverse includes - we want newer -I options to take precedence. *)
- let includes = !includes in
- let nr_jobs = !nr_jobs in
- if nr_jobs < 1 then
+ (* Check various params are sensible. *)
+ if !nr_jobs < 1 then
failwithf "%s: -j must be >= 1" Sys.executable_name;
- let use_prelude = !use_prelude in
+
+ let args = List.rev !args in
(* Get the anon var assignments and targets. *)
let anon_vars, targets =
(name, expr)
) anon_vars in
- input_file,
- debug_flag, directory, includes, nr_jobs, use_prelude, anon_vars, targets
+ anon_vars, targets
+
+let debug_flag () = !debug_flag
(* Create the debug function. *)
let debug fs =
- let display str = if debug_flag then prerr_endline str in
+ let display str = if debug_flag () then prerr_endline str in
ksprintf display fs
+
+let directory () = !directory
+let input_file () = !input_file
+
+(* Don't reverse includes - we want newer -I options to take precedence. *)
+let includes () = !includes
+
+let nr_jobs () = !nr_jobs
+let use_prelude () = !use_prelude
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
+val parse : unit -> (string * string) list * string list
+(** Parse the command line.
+ Returns two lists:
+ anon_vars = List of anonymous variable assignments.
+ targets = List of target expressions on the command line. *)
+
val stdlibdir : string
(** Get the stdlib directory. *)
val prelude_sh_file : string
(** Get the absolute path of the prelude.sh file. *)
-val input_file : string
+val input_file : unit -> string
(** Get the name of the input Goalfile. *)
val debug : ('a, unit, string, unit) format4 -> 'a
(** If debugging is enabled (-d option) then print the formatted
output. If debugging was not enabled then nothing is printed. *)
-val debug_flag : bool
+val debug_flag : unit -> bool
(** If debugging is enabled. *)
-val directory : string
+val directory : unit -> string
(** Get the name of working directory (-C option). *)
-val includes : string list
+val includes : unit -> string list
(** Get list of include directories (-I option). *)
-val nr_jobs : int
+val nr_jobs : unit -> int
(** Number of jobs (-j option). *)
-val use_prelude : bool
+val use_prelude : unit -> bool
(** True if we should load the prelude, or false if --no-prelude. *)
-
-val anon_vars : (string * string) list
-(** List of anonymous variable assignments on the command line. *)
-
-val targets : string list
-(** List of target expressions on the command line. *)
i, lines
and prepare_code env loc (code, quiet) =
- let quiet = if Cmdline.debug_flag then false else quiet in
+ let quiet = if Cmdline.debug_flag () then false else quiet in
let code = to_shell_script env loc code in
"source " ^ Filename.quote Cmdline.prelude_sh_file ^ "\n" ^
"set -e\n" ^
match returning with
| RetExpr ->
let r, b = run_code_to_string env loc code in
- if r <> 0 then (
- eprintf "*** function ‘%s’ failed with exit code %d\n" name r;
- exit 1
- );
+ if r <> 0 then
+ failwithf "function ‘%s’ failed with exit code %d" name r;
Parse.parse_expr (sprintf "function:%s" name) b
| RetString ->
let r, b = run_code_to_string env loc code in
- if r <> 0 then (
- eprintf "*** function ‘%s’ failed with exit code %d\n" name r;
- exit 1
- );
+ if r <> 0 then
+ failwithf "function ‘%s’ failed with exit code %d" name r;
Ast.EConstant (loc, Ast.CString b)
| RetStrings ->
let id = Thread.id (Thread.self ()) in
Mutex.lock lock;
incr ready;
- while not !stop && !ready <= Cmdline.nr_jobs do
+ while not !stop && !ready <= Cmdline.nr_jobs () do
(* See if there's any queue with a job which is ready to run. *)
Cmdline.debug "thread %d: checking for a runnable queue" id;
match get_runnable_queue () with
while not (all_done group); do
decr ready;
(* Start more threads if fewer than nr_jobs threads are ready. *)
- let needed = Cmdline.nr_jobs - !ready in
+ let needed = Cmdline.nr_jobs () - !ready in
if needed > 0 then
ignore (Array.init needed (Thread.create worker));
Parser.eval_substitute := Some Eval.substitute
let main () =
+ (* Handle the command line. *)
+ let anon_vars, targets = Cmdline.parse () in
+
(* Change directory (-C option). *)
- Sys.chdir Cmdline.directory;
+ Sys.chdir (Cmdline.directory ());
(* Create the initial environment, containing the system environment
* and a few other standard strings.
(* Parse the prelude. *)
let env =
- if Cmdline.use_prelude then
+ if Cmdline.use_prelude () then
Parse.parse_goalfile env Cmdline.prelude_gl_file
else env in
(* Parse the input file. *)
- let env = Parse.parse_goalfile env Cmdline.input_file in
+ let env = Parse.parse_goalfile env (Cmdline.input_file ()) in
(* Parse the command line assignments. *)
let env =
fun env (name, expr) ->
let expr = Parse.parse_expr "commandline" expr in
Ast.Env.add name expr env
- ) env Cmdline.anon_vars in
+ ) env anon_vars in
(* Parse the target expressions. *)
- let targets = List.map (Parse.parse_expr "commandline") Cmdline.targets in
+ let targets = List.map (Parse.parse_expr "commandline") targets in
(* If no target was set on the command line, use "all ()". *)
let targets =
if targets <> [] then targets
else [Ast.ECall (Ast.noloc, "all", [])] in
- if Cmdline.debug_flag then
+ if Cmdline.debug_flag () then
Ast.print_env stderr env;
(* Run the target expressions. *)
let () =
try main ()
with
- Failure msg | Sys_error msg ->
- Run.stop_all ();
- prerr_endline ("*** error: " ^ msg);
- exit 1
+ | Failure msg | Sys_error msg ->
+ Run.stop_all ();
+ prerr_endline ("*** error: " ^ msg);
+ exit 1
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
-open Lexer
open Lexing
-
open Printf
-let print_position fp lexbuf =
+open Utils
+open Lexer
+
+let string_position () lexbuf =
let pos = lexbuf.lex_curr_p in
- fprintf fp "%s:%d:%d"
- pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol)
+ sprintf "%s:%d:%d" pos.pos_fname pos.pos_lnum (pos.pos_cnum - pos.pos_bol)
let parse_file env lexbuf =
try
Ast.Env.merge env env'
with
| SyntaxError msg ->
- eprintf "%a: %s\n" print_position lexbuf msg;
- exit 1
+ failwithf "%a: %s" string_position lexbuf msg
| Parser.Error ->
- eprintf "%a: parse error\n" print_position lexbuf;
- exit 1
+ failwithf "%a: parse error" string_position lexbuf
let parse_expr lexbuf =
try Parser.expr Lexer.read lexbuf
with
| SyntaxError msg ->
- eprintf "%a: %s\n" print_position lexbuf msg;
- exit 1
+ failwithf "%a: %s" string_position lexbuf msg
| Parser.Error ->
- eprintf "%a: parse error\n" print_position lexbuf;
- exit 1
+ failwithf "%a: parse error" string_position lexbuf
(* This is used to parse the Goalfile. *)
let parse_goalfile env filename =
let path = inc // filename in
if Sys.file_exists path then path else loop incs
in
- loop Cmdline.includes
+ loop (Cmdline.includes ())
)
let do_include env loc filename optflag file =
| [] -> env
| d :: _ -> Ast.Env.add "^" d env in
let r = Eval.run_code env loc code in
- if r <> 0 then (
- eprintf "*** goal ‘%s’ failed with exit code %d\n" name r;
- exit 1
- );
+ if r <> 0 then
+ failwithf "goal ‘%s’ failed with exit code %d" name r;
(* Check all targets were updated after the code was
* run (else it's an error).
let r = Eval.run_code env loc code in
if r = 99 (* means "needs rebuild" *) then true
else if r = 0 (* means "doesn't need rebuild" *) then false
- else (
- eprintf "*** tactic ‘%s’ failed with exit code %d\n" tactic r;
- exit 1
- )
+ else
+ failwithf "tactic ‘%s’ failed with exit code %d" tactic r
(* Find the goal which matches the given tactic and start it.
* cargs is a list of parameters (all constants).