diff options
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 107 |
1 files changed, 46 insertions, 61 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 89760264..85aaf879 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -1,85 +1,70 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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) *) (************************************************************************) (** Global options of the system. *) +(** Command-line flags *) + val boot : bool ref -val load_init : bool ref -val batch_mode : bool ref -type compilation_mode = BuildVo | BuildVio | Vio2Vo -val compilation_mode : compilation_mode ref -val compilation_output_name : string option ref +(** Set by coqtop to tell the kernel to output to the aux file; will + be eventually removed by cleanups such as PR#1103 *) +val record_aux_file : bool ref +(* Flag set when the test-suite is called. Its only effect to display + verbose information for `Fail` *) val test_mode : bool ref -type async_proofs = APoff | APonLazy | APon -val async_proofs_mode : async_proofs ref -type cache = Force -val async_proofs_cache : cache option ref -val async_proofs_n_workers : int ref -val async_proofs_n_tacworkers : int ref -val async_proofs_private_flags : string option ref -val async_proofs_is_worker : unit -> bool -val async_proofs_is_master : unit -> bool -val async_proofs_full : bool ref -val async_proofs_never_reopen_branch : bool ref -val async_proofs_flags_for_workers : string list ref +(** Async-related flags *) val async_proofs_worker_id : string ref -type priority = Low | High -val async_proofs_worker_priority : priority ref -val string_of_priority : priority -> string -val priority_of_string : string -> priority -type tac_error_filter = [ `None | `Only of string list | `All ] -val async_proofs_tac_error_resilience : tac_error_filter ref -val async_proofs_cmd_error_resilience : bool ref -val async_proofs_delegation_threshold : float ref +val async_proofs_is_worker : unit -> bool +(** Debug flags *) val debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref val profile : bool -val print_emacs : bool ref -val coqtop_ui : bool ref - -val xml_export : bool ref - +(* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref -val ideslave_coqtop_flags : string option ref - -val time : bool ref +(* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref +(* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -val record_print : bool ref + +(* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current +type compat_version = V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string +(* Beautify command line flags, should move to printing? *) val beautify : bool ref val beautify_file : bool ref -val make_silent : bool -> unit -val is_silent : unit -> bool -val is_verbose : unit -> bool +(* Coq quiet mode. Note that normal mode is called "verbose" here, + whereas [quiet] supresses normal output such as goals in coqtop *) +val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit +(* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool @@ -90,14 +75,23 @@ val is_program_mode : unit -> bool val make_universe_polymorphism : bool -> unit val is_universe_polymorphism : unit -> bool -(** Local universe polymorphism flag. *) -val make_polymorphic_flag : bool -> unit -val use_polymorphic_flag : unit -> bool +(** Global polymorphic inductive cumulativity flag. *) +val make_polymorphic_inductive_cumulativity : bool -> unit +val is_polymorphic_inductive_cumulativity : unit -> bool val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit +(** [with_modified_ref r nf f x] Temporarily modify a reference in the + call to [f x] . Be very careful with these functions, it is very + easy to fall in the typical problem with effects: + + with_modified_ref r nf f x y != with_modified_ref r nf (f x) y + +*) +val with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b + (** Temporarily activate an option (to activate option [o] on [f x y z], use [with_option o (f x y) z]) *) val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b @@ -111,10 +105,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b (** Temporarily extends the reference to a list *) val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b -(** If [None], no limit *) -val set_print_hyps_limit : int option -> unit -val print_hyps_limit : unit -> int option - (** Options for external tools *) (** Returns string format for default browser to use from Coq or CoqIDE *) @@ -126,27 +116,17 @@ val is_standard_doc_url : string -> bool val coqlib_spec : bool ref val coqlib : string ref -(** Options for specifying where OCaml binaries reside *) -val ocamlfind_spec : bool ref -val ocamlfind : string ref -val camlp4bin_spec : bool ref -val camlp4bin : string ref - (** Level of inlining during a functor application *) val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(** Native code compilation for conversion and normalization *) -val native_compiler : bool ref +(** When producing vo objects, also compile the native-code version *) +val output_native_objects : bool ref (** Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref -val tactic_context_compat : bool ref -(** Set to [true] to trigger the compatibility bugged context matching (old - context vs. appcontext) is set. *) - val profile_ltac : bool ref val profile_ltac_cutoff : float ref @@ -154,3 +134,8 @@ val profile_ltac_cutoff : float ref val dump_bytecode : bool ref val set_dump_bytecode : bool -> unit val get_dump_bytecode : unit -> bool + +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref +val set_dump_lambda : bool -> unit +val get_dump_lambda : unit -> bool |