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@67137: -- "alternative document variants (separated by colons)" wenzelm@67138: option document_tags : string = "" wenzelm@67138: -- "default command tags (separated by commas)" 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@68130: public option parallel_limit : int = 0 wenzelm@68130: -- "approximative limit for parallel tasks (0 = unlimited)" 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@66160: option command_timing_threshold : real = 0.1 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@68661: option strict_facts : bool = false wenzelm@68661: -- "force lazy facts when defined in context" 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@64308: option profiling : string = "" wenzelm@64308: -- "ML profiling (possible values: time, allocations)" wenzelm@64308: wenzelm@69854: option system_heaps : bool = false wenzelm@69854: -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" wenzelm@69854: 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@69520: section "Editor Session" 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@68381: public option editor_consolidate_delay : real = 2.0 wenzelm@66379: -- "delay to consolidate status of command evaluation (execution forks)" wenzelm@66379: 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@69103: -- "initial number of tracing messages for each command transaction (0: unbounded)" 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@68197: public option editor_presentation : bool = false wenzelm@68197: -- "dynamic presentation while editing" wenzelm@68184: wenzelm@52702: wenzelm@69520: section "Headless Session" wenzelm@69520: wenzelm@69520: option headless_check_delay : real = 0.5 wenzelm@69520: -- "delay for theory status check during PIDE processing (seconds)" wenzelm@69520: wenzelm@69520: option headless_check_limit : int = 0 wenzelm@69520: -- "maximum number of theory status checks (0 = unlimited)" wenzelm@69520: wenzelm@69520: option headless_nodes_status_delay : real = -1 wenzelm@69520: -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" wenzelm@69520: wenzelm@69520: option headless_watchdog_timeout : real = 600 wenzelm@69520: -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" wenzelm@69520: wenzelm@69520: option headless_commit_cleanup_delay : real = 60 wenzelm@69520: -- "delay for cleanup of already imported theories (seconds, 0 = disabled)" wenzelm@69520: wenzelm@69520: 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@66158: public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" wenzelm@66158: -- "glob patterns to ignore in file-system path completion (separated by colons)" wenzelm@66158: 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@69353: public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" wenzelm@67395: -- "included markup elements for spell-checker (separated by commas)" wenzelm@67395: wenzelm@69968: public option spell_checker_exclude : string = "antiquoted,raw_text" wenzelm@67395: -- "excluded markup elements for spell-checker (separated by commas)" wenzelm@65141: wenzelm@65141: wenzelm@64130: section "Secure Shell" wenzelm@64130: wenzelm@69431: option ssh_config_dir : string = "$HOME/.ssh" wenzelm@64130: -- "SSH configuration directory" wenzelm@64130: wenzelm@69431: option ssh_config_file : string = "$HOME/.ssh/config" wenzelm@64130: -- "main SSH configuration file" wenzelm@64130: wenzelm@69431: option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.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@67273: option ssh_alive_count_max : int = 3 wenzelm@67273: -- "maximum number of messages to keep SSH server connection alive" wenzelm@67273: wenzelm@65595: wenzelm@68221: section "Theory Export" wenzelm@68154: wenzelm@68491: option export_document : bool = false wenzelm@68491: wenzelm@68154: option export_theory : bool = false wenzelm@68154: wenzelm@68154: wenzelm@69586: section "Theory update" wenzelm@69586: wenzelm@69589: option update_inner_syntax_cartouches : bool = false wenzelm@69589: -- "update inner syntax (types, terms, etc.) to use cartouches" wenzelm@69589: wenzelm@69586: option update_mixfix_cartouches : bool = false wenzelm@69586: -- "update mixfix templates to use cartouches instead of double quotes" wenzelm@69586: wenzelm@69592: option update_control_cartouches : bool = false wenzelm@69592: -- "update antiquotations to use control symbol with cartouche argument" wenzelm@69592: wenzelm@69603: option update_path_cartouches : bool = false wenzelm@69603: -- "update file-system paths to use cartouches" wenzelm@69603: wenzelm@69586: wenzelm@68221: section "Build Database" wenzelm@68221: wenzelm@68221: option build_database_server : bool = false wenzelm@68221: option build_database_user : string = "" wenzelm@68221: option build_database_password : string = "" wenzelm@68221: option build_database_name : string = "" wenzelm@68221: option build_database_host : string = "" wenzelm@68221: option build_database_port : int = 0 wenzelm@68221: option build_database_ssh_host : string = "" wenzelm@68221: option build_database_ssh_user : string = "" wenzelm@68221: option build_database_ssh_port : int = 0 wenzelm@68221: wenzelm@68221: 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 wenzelm@65782: option build_log_history : int = 30 -- "length of relevant history (in days)" wenzelm@67743: option build_log_transaction_size : int = 1 -- "number of log files for each db update" wenzelm@69572: wenzelm@69572: wenzelm@69572: section "Isabelle/Scala/ML system channel" wenzelm@69572: wenzelm@69572: option system_channel_address : string = "" wenzelm@69572: option system_channel_password : string = ""