63 -- "additional print modes for prover output (separated by commas)" |
63 -- "additional print modes for prover output (separated by commas)" |
64 |
64 |
65 |
65 |
66 section "Parallel Checking" |
66 section "Parallel Checking" |
67 |
67 |
68 option threads : int = 0 |
68 public option threads : int = 0 |
69 -- "maximum number of worker threads for prover process (0 = hardware max.)" |
69 -- "maximum number of worker threads for prover process (0 = hardware max.)" |
70 option threads_trace : int = 0 |
70 public option threads_trace : int = 0 |
71 -- "level of tracing information for multithreading" |
71 -- "level of tracing information for multithreading" |
72 option parallel_proofs : int = 2 |
72 public option parallel_proofs : int = 2 |
73 -- "level of parallel proof checking: 0, 1, 2" |
73 -- "level of parallel proof checking: 0, 1, 2" |
74 option parallel_subproofs_saturation : int = 100 |
74 public option parallel_subproofs_saturation : int = 100 |
75 -- "upper bound for forks of nested proofs (multiplied by worker threads)" |
75 -- "upper bound for forks of nested proofs (multiplied by worker threads)" |
76 option parallel_subproofs_threshold : real = 0.01 |
76 public option parallel_subproofs_threshold : real = 0.01 |
77 -- "lower bound of timing estimate for forked nested proofs (seconds)" |
77 -- "lower bound of timing estimate for forked nested proofs (seconds)" |
78 |
78 |
79 |
79 |
80 section "Detail of Proof Recording" |
80 section "Detail of Proof Recording" |
81 |
81 |
102 -- "build process output limit in million characters (0 = unlimited)" |
102 -- "build process output limit in million characters (0 = unlimited)" |
103 |
103 |
104 |
104 |
105 section "Editor Reactivity" |
105 section "Editor Reactivity" |
106 |
106 |
107 option editor_skip_proofs : bool = false |
107 public option editor_skip_proofs : bool = false |
108 -- "skip over proofs (implicit 'sorry')" |
108 -- "skip over proofs (implicit 'sorry')" |
109 |
109 |
110 option editor_load_delay : real = 0.5 |
110 public option editor_load_delay : real = 0.5 |
111 -- "delay for file load operations (new buffers etc.)" |
111 -- "delay for file load operations (new buffers etc.)" |
112 |
112 |
113 option editor_input_delay : real = 0.3 |
113 public option editor_input_delay : real = 0.3 |
114 -- "delay for user input (text edits, cursor movement etc.)" |
114 -- "delay for user input (text edits, cursor movement etc.)" |
115 |
115 |
116 option editor_output_delay : real = 0.1 |
116 public option editor_output_delay : real = 0.1 |
117 -- "delay for prover output (markup, common messages etc.)" |
117 -- "delay for prover output (markup, common messages etc.)" |
118 |
118 |
119 option editor_update_delay : real = 0.5 |
119 public option editor_update_delay : real = 0.5 |
120 -- "delay for physical GUI updates" |
120 -- "delay for physical GUI updates" |
121 |
121 |
122 option editor_reparse_limit : int = 10000 |
122 public option editor_reparse_limit : int = 10000 |
123 -- "maximum amount of reparsed text outside perspective" |
123 -- "maximum amount of reparsed text outside perspective" |
124 |
124 |
125 option editor_tracing_messages : int = 1000 |
125 public option editor_tracing_messages : int = 1000 |
126 -- "initial number of tracing messages for each command transaction" |
126 -- "initial number of tracing messages for each command transaction" |
127 |
127 |
128 option editor_chart_delay : real = 3.0 |
128 public option editor_chart_delay : real = 3.0 |
129 -- "delay for chart repainting" |
129 -- "delay for chart repainting" |