wenzelm@48367: (* :mode=isabelle-options: *) wenzelm@48367: wenzelm@49295: section "Document Preparation" wenzelm@49270: wenzelm@48795: option browser_info : bool = false wenzelm@48580: -- "generate theory browser information" wenzelm@48367: wenzelm@48795: option document : string = "" wenzelm@52746: -- "build document in given format: pdf, dvi, false" wenzelm@48805: option document_output : string = "" wenzelm@48805: -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" wenzelm@48805: option document_variants : string = "document" wenzelm@48795: -- "option alternative document variants (separated by colons)" wenzelm@48367: wenzelm@48795: option thy_output_display : bool = false wenzelm@48580: -- "indicate output as multi-line display-style material" wenzelm@48795: option thy_output_break : bool = false wenzelm@48580: -- "control line breaks in non-display material" wenzelm@48795: option thy_output_quotes : bool = false wenzelm@48580: -- "indicate if the output should be enclosed in double quotes" wenzelm@59175: option thy_output_margin : int = 76 wenzelm@59175: -- "right margin / page width for printing of display material" wenzelm@48795: option thy_output_indent : int = 0 wenzelm@48580: -- "indentation for pretty printing of display material" wenzelm@48795: option thy_output_source : bool = false wenzelm@48580: -- "print original source text rather than internal representation" wenzelm@52042: option thy_output_modes : string = "" wenzelm@52042: -- "additional print modes for document output (separated by commas)" wenzelm@49270: wenzelm@52043: wenzelm@52043: section "Prover Output" wenzelm@52043: wenzelm@52043: option show_types : bool = false wenzelm@52043: -- "show type constraints when printing terms" wenzelm@52043: option show_sorts : bool = false wenzelm@52043: -- "show sort constraints when printing types" wenzelm@52043: option show_brackets : bool = false wenzelm@52043: -- "show extra brackets when printing terms/types" wenzelm@52043: option show_question_marks : bool = true wenzelm@52043: -- "show leading question mark of schematic variables" wenzelm@52043: wenzelm@52043: option show_consts : bool = false wenzelm@52043: -- "show constants with types when printing proof state" wenzelm@52043: option show_main_goal : bool = false wenzelm@52043: -- "show main goal when printing proof state" wenzelm@52043: option goals_limit : int = 10 wenzelm@52043: -- "maximum number of subgoals to be printed" wenzelm@52043: wenzelm@52043: option names_long : bool = false wenzelm@52043: -- "show fully qualified names" wenzelm@52043: option names_short : bool = false wenzelm@52043: -- "show base names only" wenzelm@52043: option names_unique : bool = true wenzelm@52043: -- "show partially qualified names, as required for unique name resolution" wenzelm@52043: wenzelm@52043: option eta_contract : bool = true wenzelm@52043: -- "print terms in eta-contracted form" wenzelm@52043: wenzelm@49270: option print_mode : string = "" wenzelm@49270: -- "additional print modes for prover output (separated by commas)" wenzelm@49270: wenzelm@49270: wenzelm@56875: section "Parallel Processing" wenzelm@49270: wenzelm@52065: public option threads : int = 0 wenzelm@49270: -- "maximum number of worker threads for prover process (0 = hardware max.)" wenzelm@56734: option threads_trace : int = 0 wenzelm@49270: -- "level of tracing information for multithreading" wenzelm@59468: option threads_stack_limit : real = 0.25 wenzelm@59468: -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" wenzelm@62790: wenzelm@56875: public option parallel_print : bool = true wenzelm@56875: -- "parallel and asynchronous printing of results" wenzelm@65056: public option parallel_proofs : int = 1 wenzelm@49270: -- "level of parallel proof checking: 0, 1, 2" wenzelm@52714: option parallel_subproofs_threshold : real = 0.01 wenzelm@51423: -- "lower bound of timing estimate for forked nested proofs (seconds)" wenzelm@49270: wenzelm@62794: option command_timing_threshold : real = 0.01 wenzelm@62793: -- "default threshold for persistent command timing (seconds)" wenzelm@62793: wenzelm@49270: wenzelm@52490: section "Detail of Proof Checking" wenzelm@49270: wenzelm@65448: option record_proofs : int = -1 wenzelm@65448: -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" wenzelm@49270: option quick_and_dirty : bool = false wenzelm@49270: -- "if true then some tools will OMIT some proofs" wenzelm@49270: option skip_proofs : bool = false wenzelm@51553: -- "skip over proofs (implicit 'sorry')" wenzelm@49270: wenzelm@49270: wenzelm@49295: section "Global Session Parameters" wenzelm@49270: wenzelm@49270: option condition : string = "" wenzelm@49270: -- "required environment variables for subsequent theories (separated by commas)" wenzelm@49270: wenzelm@48795: option timeout : real = 0 wenzelm@48661: -- "timeout for session build job (seconds > 0)" wenzelm@48661: wenzelm@61602: option timeout_scale : real = 1.0 wenzelm@61602: -- "scale factor for session timeout" wenzelm@61602: wenzelm@51962: option process_output_limit : int = 100 wenzelm@62409: -- "build process output limit (in million characters, 0 = unlimited)" wenzelm@62409: wenzelm@62409: option process_output_tail : int = 40 wenzelm@62409: -- "build process output tail shown to user (in lines, 0 = unlimited)" wenzelm@51962: wenzelm@63827: option checkpoint : bool = false wenzelm@63827: -- "checkpoint for theories during build process (heap compression)" wenzelm@63827: wenzelm@64308: option profiling : string = "" wenzelm@64308: -- "ML profiling (possible values: time, allocations)" wenzelm@64308: wenzelm@65456: option theory_qualifier : string = "" wenzelm@65456: -- "explicit theory qualifier for special sessions (default: session name)" wenzelm@65456: wenzelm@56279: wenzelm@56279: section "ML System" wenzelm@56279: wenzelm@62711: option ML_print_depth : int = 20 wenzelm@62711: -- "ML print depth for toplevel pretty-printing" wenzelm@62711: wenzelm@56279: public option ML_exception_trace : bool = false wenzelm@56279: -- "ML exception trace for toplevel command execution" wenzelm@56265: wenzelm@62498: public option ML_exception_debugger : bool = false wenzelm@62498: -- "ML debugger exception trace for toplevel command execution" wenzelm@62498: wenzelm@60730: public option ML_debugger : bool = false wenzelm@60730: -- "ML debugger instrumentation for newly compiled code" wenzelm@60730: wenzelm@60074: public option ML_statistics : bool = true wenzelm@60843: -- "ML run-time system statistics" wenzelm@60074: wenzelm@61158: public option ML_system_64 : bool = false wenzelm@61158: -- "ML system for 64bit platform is used if possible (change requires restart)" wenzelm@61158: wenzelm@63986: public option ML_process_policy : string = "" wenzelm@63986: -- "ML process command prefix (process policy)" wenzelm@63986: wenzelm@49288: wenzelm@49295: section "Editor Reactivity" wenzelm@49288: wenzelm@52065: public option editor_load_delay : real = 0.5 wenzelm@49288: -- "delay for file load operations (new buffers etc.)" wenzelm@49288: wenzelm@52065: public option editor_input_delay : real = 0.3 wenzelm@49288: -- "delay for user input (text edits, cursor movement etc.)" wenzelm@49288: wenzelm@64524: public option editor_generated_input_delay : real = 1.0 wenzelm@64524: -- "delay for machine-generated input that may outperform user edits" wenzelm@64524: wenzelm@52065: public option editor_output_delay : real = 0.1 wenzelm@49288: -- "delay for prover output (markup, common messages etc.)" wenzelm@49288: wenzelm@62115: public option editor_prune_delay : real = 15 wenzelm@57867: -- "delay to prune history (delete old versions)" wenzelm@57867: wenzelm@65264: option editor_prune_size : int = 0 wenzelm@65264: -- "retained size of pruned history (delete old versions)" wenzelm@65264: wenzelm@52065: public option editor_update_delay : real = 0.5 wenzelm@49288: -- "delay for physical GUI updates" wenzelm@49288: wenzelm@52065: public option editor_reparse_limit : int = 10000 wenzelm@49524: -- "maximum amount of reparsed text outside perspective" wenzelm@50119: wenzelm@52065: public option editor_tracing_messages : int = 1000 wenzelm@50505: -- "initial number of tracing messages for each command transaction" wenzelm@50697: wenzelm@52065: public option editor_chart_delay : real = 3.0 wenzelm@50697: -- "delay for chart repainting" wenzelm@52702: wenzelm@52807: public option editor_continuous_checking : bool = true wenzelm@52807: -- "continuous checking of proof document (visible and required parts)" wenzelm@52807: wenzelm@61604: public option editor_output_state : bool = false wenzelm@61213: -- "implicit output of proof state" wenzelm@61213: wenzelm@52798: option editor_execution_delay : real = 0.02 wenzelm@52798: -- "delay for start of execution process after document update (seconds)" wenzelm@52798: wenzelm@57974: option editor_syslog_limit : int = 100 wenzelm@57974: -- "maximum amount of buffered syslog messages" wenzelm@57974: wenzelm@52702: wenzelm@52702: section "Miscellaneous Tools" wenzelm@52702: wenzelm@52702: public option find_theorems_limit : int = 40 wenzelm@52702: -- "limit of displayed results" wenzelm@52702: wenzelm@56613: public option find_theorems_tactic_limit : int = 5 wenzelm@52702: -- "limit of tactic search for 'solves' criterion" wenzelm@52702: wenzelm@55672: wenzelm@55672: section "Completion" wenzelm@55672: wenzelm@55672: public option completion_limit : int = 40 wenzelm@55672: -- "limit for completion within the formal context" wenzelm@64130: wenzelm@64130: wenzelm@65141: section "Spell Checker" wenzelm@65141: wenzelm@65141: public option spell_checker : bool = true wenzelm@65141: -- "enable spell-checker for prose words within document text, comments etc." wenzelm@65141: wenzelm@65141: public option spell_checker_dictionary : string = "en" wenzelm@65141: -- "spell-checker dictionary name" wenzelm@65141: wenzelm@65141: public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment" wenzelm@65141: -- "relevant markup elements for spell-checker, separated by commas" wenzelm@65141: wenzelm@65141: wenzelm@64130: section "Secure Shell" wenzelm@64130: wenzelm@64130: option ssh_config_dir : string = "~/.ssh" wenzelm@64130: -- "SSH configuration directory" wenzelm@64130: wenzelm@64130: option ssh_config_file : string = "~/.ssh/config" wenzelm@64130: -- "main SSH configuration file" wenzelm@64130: wenzelm@64130: option ssh_identity_files : string = "~/.ssh/id_dsa:~/.ssh/id_ecdsa:~/.ssh/id_rsa" wenzelm@64130: -- "possible SSH identity files (separated by colons)" wenzelm@64130: wenzelm@64130: option ssh_compression : bool = true wenzelm@64130: -- "enable SSH compression" wenzelm@64130: wenzelm@64130: option ssh_connect_timeout : real = 60 wenzelm@64130: -- "SSH connection timeout (seconds)" wenzelm@64325: wenzelm@64325: option ssh_alive_interval : real = 30 wenzelm@64325: -- "time interval to keep SSH server connection alive (seconds)" wenzelm@65595: wenzelm@65595: wenzelm@65595: section "Build Log Database" wenzelm@65595: wenzelm@65595: option build_log_database_user : string = "" wenzelm@65595: option build_log_database_password : string = "" wenzelm@65595: option build_log_database_name : string = "" wenzelm@65595: option build_log_database_host : string = "" wenzelm@65595: option build_log_database_port : int = 0 wenzelm@65595: option build_log_ssh_host : string = "" wenzelm@65595: option build_log_ssh_user : string = "" wenzelm@65595: option build_log_ssh_port : int = 0