Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \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) *)(************************************************************************)
let error_wrong_arg msg = prerr_endline msg; exit 1
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 error_debug () = prerr_endline "Error: The -debug option has been removed."; prerr_endline "Use the -d option for enabling debug output."; prerr_endline "For an OCaml backtrace use -bt instead."; prerr_endline "See -help for the syntax of supported options."; exit 1
(******************************************************************************)
type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool }
type top = TopLogical of string | TopPhysical of string
type option_command = | OptionSet of string option | OptionUnset
type export_flag = Export | Import
type require_injection = { lib: string; prefix: string option; export: export_flag option; allow_failure: bool }
type injection_command = | OptionInjection of (string list * option_command) | RequireInjection of require_injection | WarnNoBytecode | WarnNoNative of string | WarnNativeDeprecated
type coqargs_logic_config = { impredicative_set : bool; indices_matter : bool; type_in_type : bool; rewrite_rules : bool; toplevel_name : top;}
type time_config = ToFeedback | ToFile of string
type coqargs_config = { logic : coqargs_logic_config; rcfile : string option; coqlib : string option; enable_VM : bool; native_compiler : native_compiler; native_output_dir : CUnix.physical_path; native_include_dirs : CUnix.physical_path list; output_directory : CUnix.physical_path option; exclude_dirs : CUnix.physical_path list; quiet : bool; time : time_config option; test_mode : bool; profile : string option; print_emacs : bool;}
type vo_path = { implicit : bool; unix_path : string; rocq_path : string;}
type coqargs_pre = { boot : bool; load_init : bool; load_rcfile : bool;
ml_includes : string list; vo_includes : vo_path list; packages : string list;
load_vernacular_list : string list; injections : injection_command list;}
type coqargs_main = | Queries of Boot.Usage.query list | Run
type coqargs_post = { memory_stat : bool;}
type t = { config : coqargs_config; pre : coqargs_pre; main : coqargs_main; post : coqargs_post;}
let default_toplevel = "Top"
let default_logic_config = { impredicative_set = false; indices_matter = false; type_in_type = false; rewrite_rules = false; toplevel_name = TopLogical default_toplevel;}
let default_config = { logic = default_logic_config; rcfile = None; coqlib = None; enable_VM = Coq_config.bytecode_compiler; native_compiler = Coq_config.native_compiler; native_output_dir = ".coq-native"; native_include_dirs = []; output_directory = None; exclude_dirs = []; quiet = false; time = None; test_mode = false; profile = None; print_emacs = false;
(* Quiet / verbosity options should be here *)}
let default_pre = { boot = false; load_init = true; load_rcfile = true; ml_includes = []; vo_includes = []; packages = []; load_vernacular_list = []; injections = [];}
let default_queries = []
let default_post = { memory_stat = false;}
let default = { config = default_config; pre = default_pre; main = Run; post = default_post;}
(******************************************************************************)(* Functional arguments *)(******************************************************************************)let add_ml_include opts s = { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }}
let add_vo_include opts unix_path rocq_path implicit = let v = { unix_path; rocq_path; implicit; } in { opts with pre = { opts.pre with vo_includes = v :: opts.pre.vo_includes }}
let add_package opts p = { opts with pre = { opts.pre with packages = p :: opts.pre.packages }}
let add_vo_require opts d ?(allow_failure=false) p export = { opts with pre = { opts.pre with injections = RequireInjection {lib=d; prefix=p; export; allow_failure} :: opts.pre.injections }}
let add_load_vernacular opts s = { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v") :: opts.pre.load_vernacular_list }}
let add_set_option opts opt_name value = { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }}
let add_set_warnings opts flags = add_set_option opts ["Warnings"] (OptionSet (Some flags))
let add_set_debug opts flags = add_set_option opts ["Debug"] (OptionSet (Some flags))
(** Options for proof general *)let set_emacs opts = let opts = add_set_option opts ["Printing";"Goal";"Tags"] (OptionSet None) in { opts with config = { opts.config with print_emacs = true }}
let set_logic f oval = { oval with config = { oval.config with logic = f oval.config.logic }}
let set_query opts q = { opts with main = match opts.main with | Run -> Queries (default_queries@[q]) | Queries queries -> Queries (queries@[q]) }
(******************************************************************************)(* Parsing helpers *)(******************************************************************************)let get_bool ~opt = function | "yes" | "on" -> true | "no" | "off" -> false | _ -> error_wrong_arg ("Error: yes/no expected after option "^opt^".")
let get_int ~opt n = try int_of_string n with Failure _ -> error_wrong_arg ("Error: integer expected after option "^opt^".")let get_int_opt ~opt n = if n = "" then None else Some (get_int ~opt n)
let get_float ~opt n = try float_of_string n with Failure _ -> error_wrong_arg ("Error: float expected after option "^opt^".")
let to_opt_key = Str.(split (regexp " +"))
let parse_option_set opt = match String.index_opt opt '=' with | None -> to_opt_key opt, None | Some eqi -> let len = String.length opt in let v = String.sub opt (eqi+1) (len - eqi - 1) in to_opt_key (String.sub opt 0 eqi), Some v
let get_bytecode_compiler_warns b = if b && not Coq_config.bytecode_compiler then [WarnNoBytecode] else []
let get_native_compiler s = (* We use two boolean flags because the four states make sense, even if only three are accessible to the user at the moment. The selection of the produced artifact(s) (`.vo`, `.coq-native`, ...) should be done by a separate flag, and the "ondemand" value removed. Once this is done, use [get_bool] here. *) let n = match s with | ("yes" | "on") -> NativeOn {ondemand=false} | "ondemand" -> NativeOn {ondemand=true} | ("no" | "off") -> NativeOff | _ -> error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler.") in if n = NativeOff then n, [] else if Coq_config.native_compiler = NativeOff then NativeOff, [WarnNativeDeprecated; WarnNoNative s] else n, [WarnNativeDeprecated]
(* Main parsing routine *)(*s Parsing of the command line *)
let parse_args ~init arglist : t * string list = let args = ref arglist in let extras = ref [] in let rec parse oval = 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 noval = begin match opt with
(* Complex options with many args *) |"-I"|"-include" -> add_ml_include oval (next()) |"-Q" -> let d = next () in let p = next () in let p = if String.equal p "Coq" then "Corelib" else p in add_vo_include oval d p false |"-R" -> let d = next () in let p = next () in let p = if String.equal p "Coq" then "Corelib" else p in (* -R Coq ... is only used by Dune in conjunction with the -boot option. The above line should be removed once we require an updated version of Dune. *) add_vo_include oval d p true | "-package" -> let p = next () in add_package oval p
(* Options with one arg *) |"-coqlib" -> { oval with config = { oval.config with coqlib = Some (next ()) }}
|"-compat" -> let arg = String.split_on_char '.' (next ()) in let rocq_name = match arg with "8" :: _ -> "Coq" | _ -> "Rocq" in (* remove the above and replace by "Rocq" once theories/Compat/Coq820.v is removed *) let xy = String.concat "" (rocq_name :: arg) in add_vo_require oval xy ~allow_failure:true (Some "Stdlib") (Some Import)
|"-exclude-dir" -> { oval with config = { oval.config with exclude_dirs = next() :: oval.config.exclude_dirs } }
|"-init-file" -> { oval with config = { oval.config with rcfile = Some (next ()); }}
|"-load-vernac-source"|"-l" -> add_load_vernacular oval (next ())
|"-mangle-names" -> let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in add_set_option oval ["Mangle"; "Names"; "Prefix"] (OptionSet(Some(next ())))
|"-profile-ltac-cutoff" -> let oval = add_set_option oval ["Ltac"; "Profiling"] (OptionSet None) in add_set_option oval ["Ltac"; "Profiling"; "Cutoff"] (OptionSet (Some (next ())))
|"-load-vernac-object"|"-require" -> add_vo_require oval (next ()) None None
|"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some Import)
|"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some Export)
|"-require-from"|"-rfrom" -> let from = next () in add_vo_require oval (next ()) (Some from) None
|"-compat-from" -> let from = next () in add_vo_require oval (next ()) ~allow_failure:true (Some from) (Some Import)
|"-require-import-from" | "-rifrom" -> let from = next () in add_vo_require oval (next ()) (Some from) (Some Import)
|"-require-export-from" | "-refrom" -> let from = next () in add_vo_require oval (next ()) (Some from) (Some Export)
|"-top" -> let topname = next () in if CString.is_empty topname then error_wrong_arg "Need a non empty toplevel module name."; { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopLogical topname }}}
|"-topfile" -> { oval with config = { oval.config with logic = { oval.config.logic with toplevel_name = TopPhysical (next()) }}}
|"-w" | "-W" -> add_set_warnings oval (next())
|"-bytecode-compiler" -> let b = get_bool ~opt (next ()) in let warn = get_bytecode_compiler_warns b in { oval with config = { oval.config with enable_VM = b }; pre = { oval.pre with injections = warn @ oval.pre.injections }}
|"-native-compiler" -> let native_compiler, warn = get_native_compiler (next ()) in { oval with config = { oval.config with native_compiler }; pre = { oval.pre with injections = warn @ oval.pre.injections }}
| "-set" -> let opt, v = parse_option_set @@ next() in add_set_option oval opt (OptionSet v)
| "-unset" -> add_set_option oval (to_opt_key @@ next ()) OptionUnset
|"-native-output-dir" -> let native_output_dir = next () in { oval with config = { oval.config with native_output_dir } }
|"-output-dir" | "-output-directory" -> let dir = next () in let dir = if Filename.is_relative dir then Filename.concat (Sys.getcwd ()) dir else dir in { oval with config = { oval.config with output_directory = Some dir } }
|"-nI" -> let include_dir = next () in { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } }
(* Options with zero arg *) |"-test-mode" -> { oval with config = { oval.config with test_mode = true } } |"-config"|"--config" -> set_query oval PrintConfig
|"-bt" -> add_set_debug oval "backtrace" (* -debug is deprecated *) |"-debug" -> error_debug () |"-d" | "-D" -> add_set_debug oval (next())
|"-diffs" -> add_set_option oval ["Diffs"] @@ OptionSet (Some (next ())) |"-emacs" -> set_emacs oval |"-impredicative-set" -> set_logic (fun o -> { o with impredicative_set = true }) oval |"-allow-sprop" -> add_set_option oval ["Allow"; "StrictProp"] (OptionSet None) |"-disallow-sprop" -> add_set_option oval ["Allow"; "StrictProp"] OptionUnset |"-allow-rewrite-rules" -> set_logic (fun o -> { o with rewrite_rules = true }) oval |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} |"-boot" -> { oval with pre = { oval.pre with boot = true }} |"-profile-ltac" -> add_set_option oval ["Ltac"; "Profiling"] (OptionSet None) |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} |"-quiet"|"-silent" -> add_set_warnings { oval with config = { oval.config with quiet = true } } "-all" |"-time" -> { oval with config = { oval.config with time = Some ToFeedback }} |"-time-file" -> { oval with config = { oval.config with time = Some (ToFile (next())) }} | "-profile" -> { oval with config = { oval.config with profile = Some (next()) } } |"-type-in-type" -> set_logic (fun o -> { o with type_in_type = true }) oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some Import) |"-where" -> set_query oval PrintWhere |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval PrintHelp |"-v"|"--version" -> set_query oval PrintVersion |"-print-version"|"--print-version" -> set_query oval PrintMachineReadableVersion
(* Unknown option *) | s -> extras := s :: !extras; oval end in parse noval in parse init
(* These lists are accumulated in reverse order by the parser. This helper converts both from and to that representation. *)let reverse_accumulators opts = { opts with pre = { opts.pre with ml_includes = List.rev opts.pre.ml_includes ; vo_includes = List.rev opts.pre.vo_includes ; load_vernacular_list = List.rev opts.pre.load_vernacular_list ; injections = List.rev opts.pre.injections } }
let parse_args ~init args = let init = reverse_accumulators init in let opts, extra = parse_args ~init args in reverse_accumulators opts, extra
(******************************************************************************)(* Startup LoadPath and Modules *)(******************************************************************************)
(* prelude_data == From Corelib Require Import Prelude. *)let prelude_data = RequireInjection { lib = "Prelude"; prefix = Some "Corelib"; export = Some Import; allow_failure = false }
let injection_commands opts = if opts.pre.load_init then prelude_data :: opts.pre.injections else opts.pre.injections