diff options
Diffstat (limited to 'toplevel/coqcargs.ml')
| -rw-r--r-- | toplevel/coqcargs.ml | 174 |
1 files changed, 174 insertions, 0 deletions
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml new file mode 100644 index 0000000000..7445619d26 --- /dev/null +++ b/toplevel/coqcargs.ml @@ -0,0 +1,174 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type compilation_mode = BuildVo | BuildVio | Vio2Vo + +type t = + { compilation_mode : compilation_mode + + ; compile_list: (string * bool) list (* bool is verbosity *) + ; compilation_output_name : string option + + ; vio_checking : bool + ; vio_tasks : (int list * string) list + ; vio_files : string list + ; vio_files_j : int + + ; echo : bool + + ; outputstate : string option; + } + +let default = + { compilation_mode = BuildVo + + ; compile_list = [] + ; compilation_output_name = None + + ; vio_checking = false + ; vio_tasks = [] + ; vio_files = [] + ; vio_files_j = 0 + + ; echo = false + + ; outputstate = None + } + +let depr opt = + Feedback.msg_warning Pp.(seq[str "Option "; str opt; str " is a noop and deprecated"]) + +(* XXX Remove this duplication with Coqargs *) +let fatal_error exn = + Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn); + let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in + exit exit_code + +let error_missing_arg s = + prerr_endline ("Error: extra argument expected after option "^s); + prerr_endline "See -help for the syntax of supported options"; + exit 1 + +let add_compile ?echo copts s = + (* make the file name explicit; needed not to break up Coq loadpath stuff. *) + let echo = Option.default copts.echo echo in + let s = + let open Filename in + if is_implicit s + then concat current_dir_name s + else s + in + { copts with compile_list = (s,echo) :: copts.compile_list } + +let add_vio_task opts f = + { opts with vio_tasks = f :: opts.vio_tasks } + +let add_vio_file opts f = + { opts with vio_files = f :: opts.vio_files } + +let set_vio_checking_j opts opt j = + try { opts with vio_files_j = int_of_string j } + with Failure _ -> + prerr_endline ("The first argument of " ^ opt ^ " must the number"); + prerr_endline "of concurrent workers to be used (a positive integer)."; + prerr_endline "Makefiles generated by coq_makefile should be called"; + prerr_endline "setting the J variable like in 'make vio2vo J=3'"; + exit 1 + +let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) + +let is_not_dash_option = function + | Some f when String.length f > 0 && f.[0] <> '-' -> true + | _ -> false + +let rec add_vio_args peek next oval = + if is_not_dash_option (peek ()) then + let oval = add_vio_file oval (next ()) in + add_vio_args peek next oval + else oval + +let warn_deprecated_outputstate = + CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" + (fun () -> + Pp.strbrk "The outputstate option is deprecated and discouraged.") + +let set_outputstate opts s = + warn_deprecated_outputstate (); + { opts with outputstate = Some s } + +let parse arglist : t = + let echo = ref false in + let args = ref arglist in + let extras = ref [] in + let rec parse (oval : t) = match !args with + | [] -> + (oval, List.rev !extras) + | opt :: rem -> + args := rem; + let next () = match !args with + | x::rem -> args := rem; x + | [] -> error_missing_arg opt + in + let peek_next () = match !args with + | x::_ -> Some x + | [] -> None + in + let noval : t = begin match opt with + (* Deprecated options *) + | "-opt" + | "-byte" as opt -> + depr opt; + oval + | "-image" as opt -> + depr opt; + let _ = next () in + oval + (* Verbose == echo mode *) + | "-verbose" -> + echo := true; + oval + (* Output filename *) + | "-o" -> + { oval with compilation_output_name = Some (next ()) } + | "-quick" -> + { oval with compilation_mode = BuildVio } + | "-check-vio-tasks" -> + let tno = get_task_list (next ()) in + let tfile = next () in + add_vio_task oval (tno,tfile) + + | "-schedule-vio-checking" -> + let oval = { oval with vio_checking = true } in + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + | "-schedule-vio2vo" -> + let oval = set_vio_checking_j oval opt (next ()) in + let oval = add_vio_file oval (next ()) in + add_vio_args peek_next next oval + + | "-vio2vo" -> + let oval = add_compile ~echo:false oval (next ()) in + { oval with compilation_mode = Vio2Vo } + + | "-outputstate" -> + set_outputstate oval (next ()) + + | s -> + extras := s :: !extras; + oval + end in + parse noval + in + try + let opts, extra = parse default in + List.fold_left add_compile opts extra + with any -> fatal_error any |