#
2e9d720f |
|
02-Mar-2020 |
wenzelm <none@none> |
follow Phabricator update 2020 Week 6;
|
#
3998bbee |
|
08-Feb-2020 |
wenzelm <none@none> |
allow to override repository versions at runtime;
|
#
f19862f2 |
|
06-Nov-2019 |
wenzelm <none@none> |
discontinued somewhat pointless Isabelle options: setup implicitly assumes Ubuntu 18.04;
|
#
afae2a10 |
|
06-Nov-2019 |
wenzelm <none@none> |
unused;
|
#
22e08c7f |
|
05-Nov-2019 |
wenzelm <none@none> |
more phabricator setup;
|
#
c25cc344 |
|
30-Oct-2019 |
wenzelm <none@none> |
MySQL setup; tuned;
|
#
9ffe18b9 |
|
30-Oct-2019 |
wenzelm <none@none> |
Apache setup; proper "-" for URL: avoid problems with "_";
|
#
676f0439 |
|
30-Oct-2019 |
wenzelm <none@none> |
some support for Phabricator server;
|
#
d644b6b4 |
|
20-Oct-2019 |
wenzelm <none@none> |
option to export standardized proof terms (not scalable);
|
#
90e5dc55 |
|
07-Oct-2019 |
wenzelm <none@none> |
clarified option type;
|
#
85ad1590 |
|
07-Oct-2019 |
wenzelm <none@none> |
count document nodes via raw file length;
|
#
1460ffa6 |
|
07-Oct-2019 |
wenzelm <none@none> |
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
|
#
7ebe1d8f |
|
05-Oct-2019 |
wenzelm <none@none> |
clarified options -- more scalable;
|
#
e386bcbf |
|
01-Oct-2019 |
wenzelm <none@none> |
consolidate less aggressively: avoid live-lock when PIDE round-trip takes too long (e.g. in complex theory hierarchies);
|
#
cb3f0839 |
|
01-Oct-2019 |
wenzelm <none@none> |
obsolete (see 60abd1e94168);
|
#
83b18d31 |
|
30-Sep-2019 |
wenzelm <none@none> |
support headless_load_limit for more scalable load process;
|
#
be148acd |
|
29-Aug-2019 |
wenzelm <none@none> |
more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;
|
#
b32dc228 |
|
26-Aug-2019 |
wenzelm <none@none> |
added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);
|
#
7f034abf |
|
22-Jul-2019 |
wenzelm <none@none> |
support export_proofs, prune_proofs; tuned comments;
|
#
6887c3ec |
|
02-May-2019 |
wenzelm <none@none> |
clarified PIDE markup;
|
#
2bb316dd |
|
11-Apr-2019 |
wenzelm <none@none> |
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");
|
#
b079f8e2 |
|
11-Apr-2019 |
wenzelm <none@none> |
added document antiquotation option "cartouche";
|
#
6e82de52 |
|
24-Mar-2019 |
wenzelm <none@none> |
clarified spell-checking (see also 30233285270a);
|
#
9ff663fa |
|
01-Mar-2019 |
wenzelm <none@none> |
system option "system_heaps" supersedes various command-line options for "system build mode"; clarified "isabelle jedit" options -n, -s, -u;
|
#
9710dc54 |
|
30-Jan-2019 |
wenzelm <none@none> |
discontinued obsolete option "checkpoint";
|
#
e2307bf3 |
|
05-Jan-2019 |
wenzelm <none@none> |
support for isabelle update -u path_cartouches;
|
#
0ed93039 |
|
04-Jan-2019 |
wenzelm <none@none> |
support for isabelle update -u control_cartouches;
|
#
428a53f8 |
|
03-Jan-2019 |
wenzelm <none@none> |
support for isabelle update -u inner_syntax_cartouches;
|
#
cb8d2deb |
|
03-Jan-2019 |
wenzelm <none@none> |
support for "isabelle update -u mixfix_cartouches";
|
#
66e5efa7 |
|
02-Jan-2019 |
wenzelm <none@none> |
more robust system channel via options that are private to the user;
|
#
53119623 |
|
27-Dec-2018 |
wenzelm <none@none> |
clarified defaults via system options;
|
#
4d75b442 |
|
08-Dec-2018 |
wenzelm <none@none> |
clarified defaults for Windows/Cygwin hybrid;
|
#
12ad9e6c |
|
27-Nov-2018 |
wenzelm <none@none> |
adjusted to fc221fa79741;
|
#
ffbd9b6f |
|
02-Oct-2018 |
wenzelm <none@none> |
unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
|
#
ad719c25 |
|
19-Jul-2018 |
wenzelm <none@none> |
added system option "strict_facts";
|
#
c63366c9 |
|
24-Jun-2018 |
wenzelm <none@none> |
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
|
#
62ac99b4 |
|
05-Jun-2018 |
wenzelm <none@none> |
less wasteful consolidation, based on PIDE front-end state and recent changes;
|
#
43cdf945 |
|
02-Jun-2018 |
wenzelm <none@none> |
less frequent consolidation: it requires a full Document.update and Document.start_execution;
|
#
fd3ef1c4 |
|
19-May-2018 |
wenzelm <none@none> |
support for build_database_server (PostgreSQL); clarified signature;
|
#
fe6d63e7 |
|
16-May-2018 |
wenzelm <none@none> |
clarified "consolidation" vs. "presentation";
|
#
a63ae1fa |
|
14-May-2018 |
wenzelm <none@none> |
support for dynamic document output while editing;
|
#
ab35abfc |
|
11-May-2018 |
wenzelm <none@none> |
some export of foundational theory content;
|
#
76687af0 |
|
09-May-2018 |
wenzelm <none@none> |
clarified future scheduling parameters, with support for parallel_limit;
|
#
b31880a2 |
|
02-Mar-2018 |
wenzelm <none@none> |
avoid hardwired parameters; less ambitious defaults: low memory requirements;
|
#
cc907393 |
|
25-Jan-2018 |
wenzelm <none@none> |
more markup: disable spell-checker for raw latex;
|
#
de640a9a |
|
09-Jan-2018 |
wenzelm <none@none> |
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
|
#
2dbcc986 |
|
23-Dec-2017 |
wenzelm <none@none> |
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
|
#
f762827b |
|
13-Dec-2017 |
wenzelm <none@none> |
positions as postlude: avoid intrusion of odd %-forms into main tex source;
|
#
5d74bc5d |
|
12-Dec-2017 |
wenzelm <none@none> |
option document_positions;
|
#
7f1efcbe |
|
05-Dec-2017 |
wenzelm <none@none> |
system option for default command tags;
|
#
ce1172b0 |
|
05-Dec-2017 |
wenzelm <none@none> |
tuned;
|
#
7db8cd64 |
|
07-Oct-2017 |
wenzelm <none@none> |
theory qualifier is always session name (see also 31e8a86971a8);
|
#
f6ce89c5 |
|
08-Aug-2017 |
wenzelm <none@none> |
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
|
#
d8c59d88 |
|
21-Jun-2017 |
wenzelm <none@none> |
tuned granularity of parallel tasks;
|
#
bb073328 |
|
21-Jun-2017 |
wenzelm <none@none> |
clarified modules;
|
#
d3f54d7c |
|
08-May-2017 |
wenzelm <none@none> |
simplified default;
|
#
c837b93f |
|
27-Apr-2017 |
wenzelm <none@none> |
support for database connection;
|
#
a95f9676 |
|
10-Apr-2017 |
wenzelm <none@none> |
explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
|
#
e2bb69c8 |
|
09-Apr-2017 |
wenzelm <none@none> |
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
|
#
7698455d |
|
15-Mar-2017 |
wenzelm <none@none> |
dynamic session_options for tuning parameters and initial prover options;
|
#
5cafc90a |
|
07-Mar-2017 |
wenzelm <none@none> |
clarified modules;
|
#
33b957d3 |
|
26-Feb-2017 |
wenzelm <none@none> |
clarified defaults;
|
#
17963ce2 |
|
24-Nov-2016 |
wenzelm <none@none> |
explicit option editor_generated_input_delay, which is more aggressive by default;
|
#
d81eef2f |
|
20-Oct-2016 |
wenzelm <none@none> |
prevent sporadic disconnection;
|
#
b6228660 |
|
19-Oct-2016 |
wenzelm <none@none> |
added system option "profiling";
|
#
60843ef9 |
|
10-Oct-2016 |
wenzelm <none@none> |
clarified treatment of options; more uniform channels;
|
#
6b7980ab |
|
01-Oct-2016 |
wenzelm <none@none> |
options for process policy, notably for multiprocessor machines;
|
#
3e5c7a1a |
|
08-Sep-2016 |
wenzelm <none@none> |
option "checkpoint" helps to fine-tune global heap space management;
|
#
ff7c1b69 |
|
06-Apr-2016 |
wenzelm <none@none> |
simplified bootstrap: critical structures remain accessible in ML_Root context;
|
#
8ddb9298 |
|
05-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap environment;
|
#
17c2d502 |
|
04-Apr-2016 |
wenzelm <none@none> |
option ML_system_unsafe;
|
#
cdda981e |
|
01-Apr-2016 |
wenzelm <none@none> |
lower threshold -- command timing for proofs is cumulative, e.g. HOL 672 ~> 8889;
|
#
69a9fba9 |
|
01-Apr-2016 |
wenzelm <none@none> |
less bulky timing information, e.g. HOL 56913 ~> 672;
|
#
db1da230 |
|
01-Apr-2016 |
wenzelm <none@none> |
tuned whitespace;
|
#
c5b12b18 |
|
25-Mar-2016 |
wenzelm <none@none> |
avoid hardwired values;
|
#
ed14f1c4 |
|
02-Mar-2016 |
wenzelm <none@none> |
support for ML_exception_debugger;
|
#
51258694 |
|
25-Feb-2016 |
wenzelm <none@none> |
proper option process_output_tail, more generous default;
|
#
acf892df |
|
10-Jan-2016 |
wenzelm <none@none> |
prune old versions more often, to reduce overall heap requirements;
|
#
5880a83d |
|
19-Dec-2015 |
wenzelm <none@none> |
prune old document versions more frequently, for reduced heap usage;
|
#
547f3eba |
|
09-Nov-2015 |
wenzelm <none@none> |
prefer explicit State panel;
|
#
6f977afc |
|
08-Nov-2015 |
wenzelm <none@none> |
added option timeout_scale;
|
#
90cf715f |
|
07-Nov-2015 |
wenzelm <none@none> |
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
|
#
6b966add |
|
02-Nov-2015 |
wenzelm <none@none> |
clarified completion of Isabelle symbols within document source;
|
#
6d2bed40 |
|
21-Sep-2015 |
wenzelm <none@none> |
option editor_output_state;
|
#
b6eaeb24 |
|
11-Sep-2015 |
wenzelm <none@none> |
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
|
#
1825266d |
|
11-Aug-2015 |
wenzelm <none@none> |
init/exit depending on active debugger panels;
|
#
6b893214 |
|
10-Aug-2015 |
wenzelm <none@none> |
eliminated global option: breakpoints control this individually;
|
#
9c3a5e7b |
|
05-Aug-2015 |
wenzelm <none@none> |
more controls;
|
#
fc790fed |
|
05-Aug-2015 |
wenzelm <none@none> |
tuned signature;
|
#
8be10776 |
|
21-Jul-2015 |
wenzelm <none@none> |
support for ML debugger;
|
#
e3afdef6 |
|
16-Jul-2015 |
wenzelm <none@none> |
added option ML_debugger;
|
#
54744bb4 |
|
15-Apr-2015 |
wenzelm <none@none> |
GUI controls for ML_statistics, for more digestible protocol dump;
|
#
2a069601 |
|
29-Jan-2015 |
wenzelm <none@none> |
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;
|
#
415efe34 |
|
25-Jan-2015 |
wenzelm <none@none> |
discontinued obsolete option "document_graph";
|
#
8c11536a |
|
22-Dec-2014 |
wenzelm <none@none> |
system option "pretty_margin" is superseded by "thy_output_margin";
|
#
0af3db43 |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued pointless option: timing is always on (overall theory only);
|
#
f2748777 |
|
13-Aug-2014 |
wenzelm <none@none> |
added option editor_syslog_limit;
|
#
c356ddc9 |
|
05-Aug-2014 |
wenzelm <none@none> |
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
|
#
89b8a156 |
|
06-May-2014 |
wenzelm <none@none> |
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
|
#
041f51cf |
|
25-Apr-2014 |
wenzelm <none@none> |
suppress potential dangerous option (see 1baa5d19ac44);
|
#
e1e061e3 |
|
17-Apr-2014 |
wenzelm <none@none> |
tuned option name;
|
#
1d02cc6d |
|
25-Mar-2014 |
wenzelm <none@none> |
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);
|
#
14f462d6 |
|
23-Mar-2014 |
wenzelm <none@none> |
discontinued Toplevel.debug in favour of system option "exception_trace";
|
#
5c4e6b56 |
|
22-Feb-2014 |
wenzelm <none@none> |
support for completion within the formal context; tuned signature;
|
#
41e5cc9f |
|
25-Aug-2013 |
wenzelm <none@none> |
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;
|
#
9cb3c04f |
|
30-Jul-2013 |
wenzelm <none@none> |
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
|
#
fc76019e |
|
31-Jul-2013 |
wenzelm <none@none> |
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
|
#
ff57adaa |
|
30-Jul-2013 |
wenzelm <none@none> |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
#
2925ee78 |
|
29-Jul-2013 |
wenzelm <none@none> |
NEWS; tuned description;
|
#
266e9513 |
|
29-Jul-2013 |
wenzelm <none@none> |
afford higher execution priority by default: defer proofs and thus stretch parallelism over whole document;
|
#
bbdfea74 |
|
28-Jul-2013 |
wenzelm <none@none> |
support declarative editor_execution_range, instead of old-style check/cancel buttons;
|
#
ba00e852 |
|
27-Jul-2013 |
wenzelm <none@none> |
discontinued historic document formats;
|
#
3baee847 |
|
20-Jul-2013 |
wenzelm <none@none> |
option editor_execution_priority;
|
#
6427c1f7 |
|
20-Jul-2013 |
wenzelm <none@none> |
obscure options;
|
#
16006d2b |
|
19-Jul-2013 |
wenzelm <none@none> |
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
|
#
cfaf0ae1 |
|
18-Jul-2013 |
wenzelm <none@none> |
proper system options for 'find_theorems';
|
#
acac7fd8 |
|
29-Jun-2013 |
wenzelm <none@none> |
tuned;
|
#
d2193df8 |
|
29-Jun-2013 |
wenzelm <none@none> |
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;
|
#
99769c6c |
|
17-May-2013 |
wenzelm <none@none> |
explicit notion of public options, which are shown in the editor options dialog; avoid hard-wired stuff;
|
#
1e151b05 |
|
16-May-2013 |
wenzelm <none@none> |
more system options as context-sensitive config options;
|
#
38c07a40 |
|
16-May-2013 |
wenzelm <none@none> |
Thy_Output.modes as proper option;
|
#
44d2c5e9 |
|
13-May-2013 |
wenzelm <none@none> |
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
|
#
1c528634 |
|
13-May-2013 |
wenzelm <none@none> |
option "goals_limit", with more uniform description;
|
#
19282f21 |
|
27-Mar-2013 |
wenzelm <none@none> |
discontinued obsolete parallel_proofs_reuse_timing;
|
#
688e0813 |
|
27-Mar-2013 |
wenzelm <none@none> |
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
|
#
6c1c54c1 |
|
27-Mar-2013 |
wenzelm <none@none> |
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);
|
#
a51e1a99 |
|
13-Mar-2013 |
wenzelm <none@none> |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
|
#
98b408d5 |
|
20-Feb-2013 |
wenzelm <none@none> |
option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;
|
#
1c3c00bf |
|
22-Jan-2013 |
wenzelm <none@none> |
more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
|
#
e2c5ec93 |
|
03-Jan-2013 |
wenzelm <none@none> |
always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
|
#
14e8822e |
|
03-Jan-2013 |
wenzelm <none@none> |
improved Monitor_Dockable, based on ML_Statistics operations; tuned signature;
|
#
88af9b65 |
|
13-Dec-2012 |
wenzelm <none@none> |
smarter handling of tracing messages: prover process pauses and enters user dialog;
|
#
3d15fd72 |
|
10-Dec-2012 |
wenzelm <none@none> |
more generous tracing limit -- rescaled in MB;
|
#
4af3fd10 |
|
28-Nov-2012 |
wenzelm <none@none> |
some support for ML runtime statistics;
|
#
57f9e119 |
|
18-Nov-2012 |
wenzelm <none@none> |
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release); always generate sty files, as before c5d0f19ef7cb;
|
#
fcad59c7 |
|
18-Nov-2012 |
wenzelm <none@none> |
more generous tracing_limit, with explicit system option;
|
#
6e03a43d |
|
22-Sep-2012 |
wenzelm <none@none> |
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
|
#
c22e8faa |
|
11-Sep-2012 |
wenzelm <none@none> |
more precise sections;
|
#
2d6a405e |
|
11-Sep-2012 |
wenzelm <none@none> |
tuned;
|
#
81d8061a |
|
11-Sep-2012 |
wenzelm <none@none> |
more options;
|
#
c070d816 |
|
11-Sep-2012 |
wenzelm <none@none> |
some support to organize options in sections;
|
#
f4d1abc1 |
|
14-Aug-2012 |
wenzelm <none@none> |
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
|
#
883f280f |
|
14-Aug-2012 |
wenzelm <none@none> |
clarified format of etc/options: only declarations, not re-definitions;
|
#
70b8619a |
|
03-Aug-2012 |
wenzelm <none@none> |
timeout for session build job; tuned error messages;
|
#
f6658e8a |
|
01-Aug-2012 |
wenzelm <none@none> |
explicit option skip_proofs;
|
#
27d57668 |
|
28-Jul-2012 |
wenzelm <none@none> |
some description of main build options;
|
#
702d5798 |
|
26-Jul-2012 |
wenzelm <none@none> |
more build options;
|
#
c3009863 |
|
26-Jul-2012 |
wenzelm <none@none> |
more build options;
|
#
3c5a874e |
|
26-Jul-2012 |
wenzelm <none@none> |
refined "document_dump_mode": "all", "tex+sty", "tex";
|
#
974f6a58 |
|
26-Jul-2012 |
wenzelm <none@none> |
discontinued slightly odd "browser_info_remote" -- it could point to a completely different version of the Isabelle library;
|
#
8872a3f9 |
|
24-Jul-2012 |
wenzelm <none@none> |
more build options;
|
#
7bd05b6a |
|
24-Jul-2012 |
wenzelm <none@none> |
more build options;
|
#
bf04a03f |
|
23-Jul-2012 |
wenzelm <none@none> |
added "document_dump_only" (cf. negated usedir -C);
|
#
629d4a15 |
|
24-Jul-2012 |
wenzelm <none@none> |
further imitation of ISABELLE_USEDIR_OPTIONS via options;
|
#
4aea96ac |
|
24-Jul-2012 |
wenzelm <none@none> |
added "browser_info_remote" (cf. usedir -P);
|
#
64f8d919 |
|
24-Jul-2012 |
wenzelm <none@none> |
tuned options;
|
#
00b055a4 |
|
24-Jul-2012 |
wenzelm <none@none> |
timing is command line options, not system option;
|
#
c3e7a789 |
|
24-Jul-2012 |
wenzelm <none@none> |
clarified document options;
|
#
77967a15 |
|
23-Jul-2012 |
wenzelm <none@none> |
pass build options to ML; some imitation of usedir Session.init;
|
#
03f1f829 |
|
20-Jul-2012 |
wenzelm <none@none> |
require explicit initialization of options; more explicit Position operations;
|
#
c9a6e404 |
|
20-Jul-2012 |
wenzelm <none@none> |
some basic Isabelle options;
|