author | wenzelm |
Fri, 07 Aug 2020 11:46:14 +0200 | |
changeset 72110 | 16fab31feadc |
parent 72103 | 7b318273a4aa |
child 72136 | 98dca728fc9c |
permissions | -rw-r--r-- |
48367 | 1 |
(* :mode=isabelle-options: *) |
2 |
||
49295 | 3 |
section "Document Preparation" |
49270 | 4 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
5 |
option browser_info : bool = false |
48580 | 6 |
-- "generate theory browser information" |
48367 | 7 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
8 |
option document : string = "" |
52746 | 9 |
-- "build document in given format: pdf, dvi, false" |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
10 |
option document_output : string = "" |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
11 |
-- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
12 |
option document_variants : string = "document" |
67137 | 13 |
-- "alternative document variants (separated by colons)" |
67138 | 14 |
option document_tags : string = "" |
15 |
-- "default command tags (separated by commas)" |
|
48367 | 16 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
17 |
option thy_output_display : bool = false |
48580 | 18 |
-- "indicate output as multi-line display-style material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
19 |
option thy_output_break : bool = false |
48580 | 20 |
-- "control line breaks in non-display material" |
70121 | 21 |
option thy_output_cartouche : bool = false |
22 |
-- "indicate if the output should be delimited as cartouche" |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
23 |
option thy_output_quotes : bool = false |
70121 | 24 |
-- "indicate if the output should be delimited via double quotes" |
59175
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
58849
diff
changeset
|
25 |
option thy_output_margin : int = 76 |
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
58849
diff
changeset
|
26 |
-- "right margin / page width for printing of display material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
27 |
option thy_output_indent : int = 0 |
48580 | 28 |
-- "indentation for pretty printing of display material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
29 |
option thy_output_source : bool = false |
48580 | 30 |
-- "print original source text rather than internal representation" |
70122
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
31 |
option thy_output_source_cartouche : bool = false |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
32 |
-- "print original source text rather than internal representation, preserve cartouches" |
52042 | 33 |
option thy_output_modes : string = "" |
34 |
-- "additional print modes for document output (separated by commas)" |
|
49270 | 35 |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
36 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
37 |
section "Prover Output" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
38 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
39 |
option show_types : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
40 |
-- "show type constraints when printing terms" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
41 |
option show_sorts : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
42 |
-- "show sort constraints when printing types" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
43 |
option show_brackets : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
44 |
-- "show extra brackets when printing terms/types" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
45 |
option show_question_marks : bool = true |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
46 |
-- "show leading question mark of schematic variables" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
47 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
48 |
option show_consts : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
49 |
-- "show constants with types when printing proof state" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
50 |
option show_main_goal : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
51 |
-- "show main goal when printing proof state" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
52 |
option goals_limit : int = 10 |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
53 |
-- "maximum number of subgoals to be printed" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
54 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
55 |
option names_long : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
56 |
-- "show fully qualified names" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
57 |
option names_short : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
58 |
-- "show base names only" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
59 |
option names_unique : bool = true |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
60 |
-- "show partially qualified names, as required for unique name resolution" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
61 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
62 |
option eta_contract : bool = true |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
63 |
-- "print terms in eta-contracted form" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
64 |
|
49270 | 65 |
option print_mode : string = "" |
66 |
-- "additional print modes for prover output (separated by commas)" |
|
67 |
||
68 |
||
56875
f6259d6fb565
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
wenzelm
parents:
56734
diff
changeset
|
69 |
section "Parallel Processing" |
49270 | 70 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
71 |
public option threads : int = 0 |
49270 | 72 |
-- "maximum number of worker threads for prover process (0 = hardware max.)" |
56734
6ca87a061740
suppress potential dangerous option (see 1baa5d19ac44);
wenzelm
parents:
56613
diff
changeset
|
73 |
option threads_trace : int = 0 |
49270 | 74 |
-- "level of tracing information for multithreading" |
59468
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59446
diff
changeset
|
75 |
option threads_stack_limit : real = 0.25 |
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59446
diff
changeset
|
76 |
-- "maximum stack size for worker threads (in giga words, 0 = unlimited)" |
62790 | 77 |
|
68130
6fb85346cb79
clarified future scheduling parameters, with support for parallel_limit;
wenzelm
parents:
67743
diff
changeset
|
78 |
public option parallel_limit : int = 0 |
6fb85346cb79
clarified future scheduling parameters, with support for parallel_limit;
wenzelm
parents:
67743
diff
changeset
|
79 |
-- "approximative limit for parallel tasks (0 = unlimited)" |
56875
f6259d6fb565
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
wenzelm
parents:
56734
diff
changeset
|
80 |
public option parallel_print : bool = true |
f6259d6fb565
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
wenzelm
parents:
56734
diff
changeset
|
81 |
-- "parallel and asynchronous printing of results" |
65056 | 82 |
public option parallel_proofs : int = 1 |
49270 | 83 |
-- "level of parallel proof checking: 0, 1, 2" |
52714 | 84 |
option parallel_subproofs_threshold : real = 0.01 |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51230
diff
changeset
|
85 |
-- "lower bound of timing estimate for forked nested proofs (seconds)" |
49270 | 86 |
|
66160 | 87 |
option command_timing_threshold : real = 0.1 |
62793
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62790
diff
changeset
|
88 |
-- "default threshold for persistent command timing (seconds)" |
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62790
diff
changeset
|
89 |
|
49270 | 90 |
|
52490 | 91 |
section "Detail of Proof Checking" |
49270 | 92 |
|
65448
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65264
diff
changeset
|
93 |
option record_proofs : int = -1 |
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65264
diff
changeset
|
94 |
-- "set level of proofterm recording: 0, 1, 2, negative means unchanged" |
49270 | 95 |
option quick_and_dirty : bool = false |
96 |
-- "if true then some tools will OMIT some proofs" |
|
97 |
option skip_proofs : bool = false |
|
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51423
diff
changeset
|
98 |
-- "skip over proofs (implicit 'sorry')" |
68661 | 99 |
option strict_facts : bool = false |
100 |
-- "force lazy facts when defined in context" |
|
49270 | 101 |
|
102 |
||
49295 | 103 |
section "Global Session Parameters" |
49270 | 104 |
|
105 |
option condition : string = "" |
|
106 |
-- "required environment variables for subsequent theories (separated by commas)" |
|
107 |
||
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
108 |
option timeout : real = 0 |
48661 | 109 |
-- "timeout for session build job (seconds > 0)" |
110 |
||
61602 | 111 |
option timeout_scale : real = 1.0 |
112 |
-- "scale factor for session timeout" |
|
113 |
||
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51960
diff
changeset
|
114 |
option process_output_limit : int = 100 |
62409
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
115 |
-- "build process output limit (in million characters, 0 = unlimited)" |
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
116 |
|
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
117 |
option process_output_tail : int = 40 |
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
118 |
-- "build process output tail shown to user (in lines, 0 = unlimited)" |
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51960
diff
changeset
|
119 |
|
64308 | 120 |
option profiling : string = "" |
121 |
-- "ML profiling (possible values: time, allocations)" |
|
122 |
||
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69755
diff
changeset
|
123 |
option system_heaps : bool = false |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69755
diff
changeset
|
124 |
-- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69755
diff
changeset
|
125 |
|
56279
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56265
diff
changeset
|
126 |
|
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56265
diff
changeset
|
127 |
section "ML System" |
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56265
diff
changeset
|
128 |
|
62711 | 129 |
option ML_print_depth : int = 20 |
130 |
-- "ML print depth for toplevel pretty-printing" |
|
131 |
||
56279
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56265
diff
changeset
|
132 |
public option ML_exception_trace : bool = false |
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56265
diff
changeset
|
133 |
-- "ML exception trace for toplevel command execution" |
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
55672
diff
changeset
|
134 |
|
62498 | 135 |
public option ML_exception_debugger : bool = false |
136 |
-- "ML debugger exception trace for toplevel command execution" |
|
137 |
||
60730 | 138 |
public option ML_debugger : bool = false |
139 |
-- "ML debugger instrumentation for newly compiled code" |
|
140 |
||
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
59468
diff
changeset
|
141 |
public option ML_statistics : bool = true |
60843 | 142 |
-- "ML run-time system statistics" |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
59468
diff
changeset
|
143 |
|
61158
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
60889
diff
changeset
|
144 |
public option ML_system_64 : bool = false |
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
60889
diff
changeset
|
145 |
-- "ML system for 64bit platform is used if possible (change requires restart)" |
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
60889
diff
changeset
|
146 |
|
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63827
diff
changeset
|
147 |
public option ML_process_policy : string = "" |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63827
diff
changeset
|
148 |
-- "ML process command prefix (process policy)" |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63827
diff
changeset
|
149 |
|
49288 | 150 |
|
71675 | 151 |
section "PIDE Build" |
152 |
||
153 |
option pide_reports : bool = true |
|
154 |
-- "report PIDE markup" |
|
155 |
||
156 |
||
69520 | 157 |
section "Editor Session" |
49288 | 158 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
159 |
public option editor_load_delay : real = 0.5 |
49288 | 160 |
-- "delay for file load operations (new buffers etc.)" |
161 |
||
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
162 |
public option editor_input_delay : real = 0.3 |
49288 | 163 |
-- "delay for user input (text edits, cursor movement etc.)" |
164 |
||
64524
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64325
diff
changeset
|
165 |
public option editor_generated_input_delay : real = 1.0 |
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64325
diff
changeset
|
166 |
-- "delay for machine-generated input that may outperform user edits" |
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64325
diff
changeset
|
167 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
168 |
public option editor_output_delay : real = 0.1 |
49288 | 169 |
-- "delay for prover output (markup, common messages etc.)" |
170 |
||
70787 | 171 |
public option editor_consolidate_delay : real = 2.0 |
66379
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
66160
diff
changeset
|
172 |
-- "delay to consolidate status of command evaluation (execution forks)" |
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
66160
diff
changeset
|
173 |
|
62115
57895801cb57
prune old versions more often, to reduce overall heap requirements;
wenzelm
parents:
61873
diff
changeset
|
174 |
public option editor_prune_delay : real = 15 |
57867
abae8aff6262
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
wenzelm
parents:
56875
diff
changeset
|
175 |
-- "delay to prune history (delete old versions)" |
abae8aff6262
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
wenzelm
parents:
56875
diff
changeset
|
176 |
|
65264
7e6ecd04b5fe
dynamic session_options for tuning parameters and initial prover options;
wenzelm
parents:
65141
diff
changeset
|
177 |
option editor_prune_size : int = 0 |
7e6ecd04b5fe
dynamic session_options for tuning parameters and initial prover options;
wenzelm
parents:
65141
diff
changeset
|
178 |
-- "retained size of pruned history (delete old versions)" |
7e6ecd04b5fe
dynamic session_options for tuning parameters and initial prover options;
wenzelm
parents:
65141
diff
changeset
|
179 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
180 |
public option editor_update_delay : real = 0.5 |
49288 | 181 |
-- "delay for physical GUI updates" |
182 |
||
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
183 |
public option editor_reparse_limit : int = 10000 |
49524
68796a77c42b
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
wenzelm
parents:
49295
diff
changeset
|
184 |
-- "maximum amount of reparsed text outside perspective" |
50119
5c370a036de7
more generous tracing_limit, with explicit system option;
wenzelm
parents:
49524
diff
changeset
|
185 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
186 |
public option editor_tracing_messages : int = 1000 |
69103
814a1ab42d70
unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
wenzelm
parents:
68661
diff
changeset
|
187 |
-- "initial number of tracing messages for each command transaction (0: unbounded)" |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50505
diff
changeset
|
188 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
189 |
public option editor_chart_delay : real = 3.0 |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50505
diff
changeset
|
190 |
-- "delay for chart repainting" |
52702 | 191 |
|
52807
b859a180936b
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
wenzelm
parents:
52798
diff
changeset
|
192 |
public option editor_continuous_checking : bool = true |
b859a180936b
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
wenzelm
parents:
52798
diff
changeset
|
193 |
-- "continuous checking of proof document (visible and required parts)" |
b859a180936b
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
wenzelm
parents:
52798
diff
changeset
|
194 |
|
61604 | 195 |
public option editor_output_state : bool = false |
61213 | 196 |
-- "implicit output of proof state" |
197 |
||
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52779
diff
changeset
|
198 |
option editor_execution_delay : real = 0.02 |
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52779
diff
changeset
|
199 |
-- "delay for start of execution process after document update (seconds)" |
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52779
diff
changeset
|
200 |
|
57974 | 201 |
option editor_syslog_limit : int = 100 |
202 |
-- "maximum amount of buffered syslog messages" |
|
203 |
||
68197 | 204 |
public option editor_presentation : bool = false |
205 |
-- "dynamic presentation while editing" |
|
68184
6c693b2700b3
support for dynamic document output while editing;
wenzelm
parents:
68154
diff
changeset
|
206 |
|
52702 | 207 |
|
69520 | 208 |
section "Headless Session" |
209 |
||
70787 | 210 |
option headless_consolidate_delay : real = 15 |
211 |
-- "delay to consolidate status of command evaluation (execution forks)" |
|
212 |
||
213 |
option headless_prune_delay : real = 60 |
|
214 |
-- "delay to prune history (delete old versions)" |
|
215 |
||
69520 | 216 |
option headless_check_delay : real = 0.5 |
217 |
-- "delay for theory status check during PIDE processing (seconds)" |
|
218 |
||
219 |
option headless_check_limit : int = 0 |
|
220 |
-- "maximum number of theory status checks (0 = unlimited)" |
|
221 |
||
222 |
option headless_nodes_status_delay : real = -1 |
|
223 |
-- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" |
|
224 |
||
225 |
option headless_watchdog_timeout : real = 600 |
|
226 |
-- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" |
|
227 |
||
228 |
option headless_commit_cleanup_delay : real = 60 |
|
229 |
-- "delay for cleanup of already imported theories (seconds, 0 = disabled)" |
|
230 |
||
70801 | 231 |
option headless_load_limit : real = 5.0 |
70800 | 232 |
-- "limit in MB for loaded theory files (0 = unlimited)" |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70634
diff
changeset
|
233 |
|
69520 | 234 |
|
52702 | 235 |
section "Miscellaneous Tools" |
236 |
||
237 |
public option find_theorems_limit : int = 40 |
|
238 |
-- "limit of displayed results" |
|
239 |
||
56613 | 240 |
public option find_theorems_tactic_limit : int = 5 |
52702 | 241 |
-- "limit of tactic search for 'solves' criterion" |
242 |
||
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
243 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
244 |
section "Completion" |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
245 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
246 |
public option completion_limit : int = 40 |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
247 |
-- "limit for completion within the formal context" |
64130 | 248 |
|
66158 | 249 |
public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" |
250 |
-- "glob patterns to ignore in file-system path completion (separated by colons)" |
|
251 |
||
64130 | 252 |
|
65141 | 253 |
section "Spell Checker" |
254 |
||
255 |
public option spell_checker : bool = true |
|
256 |
-- "enable spell-checker for prose words within document text, comments etc." |
|
257 |
||
258 |
public option spell_checker_dictionary : string = "en" |
|
259 |
-- "spell-checker dictionary name" |
|
260 |
||
69353 | 261 |
public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" |
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67273
diff
changeset
|
262 |
-- "included markup elements for spell-checker (separated by commas)" |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67273
diff
changeset
|
263 |
|
70229 | 264 |
public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" |
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67273
diff
changeset
|
265 |
-- "excluded markup elements for spell-checker (separated by commas)" |
65141 | 266 |
|
267 |
||
64130 | 268 |
section "Secure Shell" |
269 |
||
69431 | 270 |
option ssh_config_dir : string = "$HOME/.ssh" |
64130 | 271 |
-- "SSH configuration directory" |
272 |
||
69431 | 273 |
option ssh_config_file : string = "$HOME/.ssh/config" |
64130 | 274 |
-- "main SSH configuration file" |
275 |
||
69431 | 276 |
option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa" |
64130 | 277 |
-- "possible SSH identity files (separated by colons)" |
278 |
||
279 |
option ssh_compression : bool = true |
|
280 |
-- "enable SSH compression" |
|
281 |
||
282 |
option ssh_connect_timeout : real = 60 |
|
283 |
-- "SSH connection timeout (seconds)" |
|
64325 | 284 |
|
285 |
option ssh_alive_interval : real = 30 |
|
286 |
-- "time interval to keep SSH server connection alive (seconds)" |
|
65595 | 287 |
|
67273
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67194
diff
changeset
|
288 |
option ssh_alive_count_max : int = 3 |
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67194
diff
changeset
|
289 |
-- "maximum number of messages to keep SSH server connection alive" |
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67194
diff
changeset
|
290 |
|
65595 | 291 |
|
71422
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
292 |
section "Phabricator" |
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
293 |
|
72071 | 294 |
option phabricator_version_arcanist : string = "2565cc7b4d1dbce6bc7a5b3c4e72ae94be4712fe" |
71422
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
295 |
-- "repository version for arcanist" |
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
296 |
|
72071 | 297 |
option phabricator_version_phabricator : string = "324445589b5eec0377cd415036fc407295c1ba25" |
71422
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
298 |
-- "repository version for phabricator" |
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
299 |
|
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
300 |
|
68221 | 301 |
section "Theory Export" |
68154 | 302 |
|
68491
f0f83ce0badd
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
wenzelm
parents:
68381
diff
changeset
|
303 |
option export_document : bool = false |
70396 | 304 |
-- "export document sources to Isabelle/Scala" |
68491
f0f83ce0badd
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
wenzelm
parents:
68381
diff
changeset
|
305 |
|
68154 | 306 |
option export_theory : bool = false |
70396 | 307 |
-- "export theory content to Isabelle/Scala" |
308 |
||
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70801
diff
changeset
|
309 |
option export_standard_proofs : bool = false |
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70801
diff
changeset
|
310 |
-- "export standardized proof terms to Isabelle/Scala (not scalable)" |
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70801
diff
changeset
|
311 |
|
70396 | 312 |
option export_proofs : bool = false |
313 |
-- "export proof terms to Isabelle/Scala" |
|
314 |
||
315 |
option prune_proofs : bool = false |
|
316 |
-- "prune proof terms after export (do not store in Isabelle/ML)" |
|
68154 | 317 |
|
318 |
||
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
319 |
section "Theory update" |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
320 |
|
69589
e15f053a42d8
support for isabelle update -u inner_syntax_cartouches;
wenzelm
parents:
69586
diff
changeset
|
321 |
option update_inner_syntax_cartouches : bool = false |
e15f053a42d8
support for isabelle update -u inner_syntax_cartouches;
wenzelm
parents:
69586
diff
changeset
|
322 |
-- "update inner syntax (types, terms, etc.) to use cartouches" |
e15f053a42d8
support for isabelle update -u inner_syntax_cartouches;
wenzelm
parents:
69586
diff
changeset
|
323 |
|
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
324 |
option update_mixfix_cartouches : bool = false |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
325 |
-- "update mixfix templates to use cartouches instead of double quotes" |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
326 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69589
diff
changeset
|
327 |
option update_control_cartouches : bool = false |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69589
diff
changeset
|
328 |
-- "update antiquotations to use control symbol with cartouche argument" |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69589
diff
changeset
|
329 |
|
69603 | 330 |
option update_path_cartouches : bool = false |
331 |
-- "update file-system paths to use cartouches" |
|
332 |
||
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
333 |
|
68221 | 334 |
section "Build Database" |
335 |
||
336 |
option build_database_server : bool = false |
|
337 |
option build_database_user : string = "" |
|
338 |
option build_database_password : string = "" |
|
339 |
option build_database_name : string = "" |
|
340 |
option build_database_host : string = "" |
|
341 |
option build_database_port : int = 0 |
|
342 |
option build_database_ssh_host : string = "" |
|
343 |
option build_database_ssh_user : string = "" |
|
344 |
option build_database_ssh_port : int = 0 |
|
345 |
||
346 |
||
65595 | 347 |
section "Build Log Database" |
348 |
||
349 |
option build_log_database_user : string = "" |
|
350 |
option build_log_database_password : string = "" |
|
351 |
option build_log_database_name : string = "" |
|
352 |
option build_log_database_host : string = "" |
|
353 |
option build_log_database_port : int = 0 |
|
354 |
option build_log_ssh_host : string = "" |
|
355 |
option build_log_ssh_user : string = "" |
|
356 |
option build_log_ssh_port : int = 0 |
|
65782 | 357 |
option build_log_history : int = 30 -- "length of relevant history (in days)" |
67743 | 358 |
option build_log_transaction_size : int = 1 -- "number of log files for each db update" |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
359 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
360 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
361 |
section "Isabelle/Scala/ML system channel" |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
362 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
363 |
option system_channel_address : string = "" |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
364 |
option system_channel_password : string = "" |