isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -112 +112 +1000 +3000 tip

merged
18 months ago, by paulson
Tidied up more messy proofs
18 months ago, by paulson
hints on "hg bisect";
18 months ago, by wenzelm
no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
18 months ago, by wenzelm
Removal of ugly old proofs
18 months ago, by paulson
merged
18 months ago, by paulson
More cosmetic changes
18 months ago, by paulson
Cosmetic polishing of proofs
18 months ago, by paulson
remove debug printing
18 months ago, by Mathias Fleury
merged
18 months ago, by nipkow
added mbox-like latex sugar
18 months ago, by nipkow
Added tag Isabelle2023-RC2 for changeset 53b59fa42696
18 months ago, by wenzelm
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
18 months ago, by wenzelm
revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);
18 months ago, by wenzelm
output panel: don't discard already filtered messages
18 months ago, by kleing
merged
18 months ago, by wenzelm
tuned signature: more operations;
18 months ago, by wenzelm
avoid excessive accumulation of garbage, for profiling of huge sessions;
18 months ago, by wenzelm
clarified signature: systematic use of Properties.make_string;
18 months ago, by wenzelm
tuned;
18 months ago, by wenzelm
support for let in Alethe name bindings;
18 months ago, by Mathias Fleury
merged
18 months ago, by paulson
A few more cosmetic changes to proofs
18 months ago, by paulson
merged
19 months ago, by paulson
tidying a few proofs a bit more
19 months ago, by paulson
partly tidied some truly horrible proofs
19 months ago, by paulson
update for release;
18 months ago, by wenzelm
back out 9d5e2a08ba1b, hoping the server room stays sufficiently cool;
18 months ago, by wenzelm
performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers);
18 months ago, by wenzelm
clarified statistics;
18 months ago, by wenzelm
show more build history for AFP;
18 months ago, by wenzelm
more statistics;
18 months ago, by wenzelm
proper base_thys;
18 months ago, by wenzelm
more thorough context tracing;
18 months ago, by wenzelm
proper check;
18 months ago, by wenzelm
proper symbolic hostname, as provided via Build_Cluster.Host;
18 months ago, by wenzelm
unused;
18 months ago, by wenzelm
clarified signature: Build_Cluster.Session.build_context;
18 months ago, by wenzelm
clarified exception handling and return_code;
18 months ago, by wenzelm
tuned signature: more operations;
18 months ago, by wenzelm
more robust;
18 months ago, by wenzelm
support for Build_Cluster.Session.init (rsync + Admin/init);
18 months ago, by wenzelm
prefer Process_Result.RC.merge: strict treatment of interrupt;
18 months ago, by wenzelm
clarified signature: more operations;
18 months ago, by wenzelm
proper afp_root;
18 months ago, by wenzelm
clarified signature: more "object-oriented" style;
19 months ago, by wenzelm
more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process;
19 months ago, by wenzelm
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified option (see also b66b6cc1eb8c);
19 months ago, by wenzelm
more build_cluster management: open SSH connections in parallel, but synchronously;
19 months ago, by wenzelm
tuned signature: more options;
19 months ago, by wenzelm
clarified signature: more operations;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
more accurate print vs. parse;
19 months ago, by wenzelm
clarified signature;
19 months ago, by wenzelm
clarified signature (again);
19 months ago, by wenzelm
tuned output;
19 months ago, by wenzelm
tuned output;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
more pro-forma support for afp_root;
19 months ago, by wenzelm
tuned NEWS: emphasize "isabelle build" add-ons;
19 months ago, by wenzelm
added option -A for AFP root, following "isabelle sync";
19 months ago, by wenzelm
clarified signature: more operations;
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
clarified file location: to be used by regular Isabelle/Scala tools;
19 months ago, by wenzelm
update headers;
19 months ago, by wenzelm
more pro-forma support for Build_Cluster;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
tuned;
19 months ago, by wenzelm
clarified options;
19 months ago, by wenzelm
clarified options;
19 months ago, by wenzelm
proper Build_Cluster.Host.parse for parameters and system options;
19 months ago, by wenzelm
more operations for independent "inline" options;
19 months ago, by wenzelm
clarified options: accommodate potentially slow database connection;
19 months ago, by wenzelm
minor performance tuning;
19 months ago, by wenzelm
add option "build_context" in anticipation of AFP entries that require special tricks in Isabelle/ML (NB: system component settings are unavailable in AFP);
19 months ago, by wenzelm
proper build_options (amending 822ddccda899);
19 months ago, by wenzelm
clarified options;
19 months ago, by wenzelm
proforma support for remote build hosts;
19 months ago, by wenzelm
more options for performance tuning;
19 months ago, by wenzelm
more operations;
19 months ago, by wenzelm
support for management of build cluster;
19 months ago, by wenzelm
clarified modules;
19 months ago, by wenzelm
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
19 months ago, by wenzelm
more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh;
19 months ago, by wenzelm
proper running limit, based on this worker process;
19 months ago, by wenzelm
more robust: implicit locking of tables in standard order;
19 months ago, by wenzelm
more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked;
19 months ago, by wenzelm
removed unused "create_index": implicit index from primary_key is usually sufficient;
19 months ago, by wenzelm
clarified "vacuum" (again, reverting 0bd366fad888);
19 months ago, by wenzelm
clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
19 months ago, by wenzelm
update for release;
19 months ago, by wenzelm
merged
19 months ago, by wenzelm
more elementary transaction implementation (despite fda3f7a158b9 and 9da65bc75610);
19 months ago, by wenzelm
tuned signature;
19 months ago, by wenzelm
proper check (amending 234f2ff9afe6);
19 months ago, by wenzelm
more robust: exclude accidental nesting (synchronized block is re-entrant);
19 months ago, by wenzelm
clarified errors;
19 months ago, by wenzelm
removed junk (amending f8e3b228670c);
19 months ago, by wenzelm
tuned output;
19 months ago, by wenzelm
reuse SSH.Server connection for database server;
19 months ago, by wenzelm
tuned source structure;
19 months ago, by wenzelm
clarified check: uniform session_info_exists;
19 months ago, by wenzelm
more complete check;
19 months ago, by wenzelm
clarified signature: more specific exists_table --- avoid retrieving full list beforehand;
19 months ago, by wenzelm
reuse database_server connection;
19 months ago, by wenzelm
more informative trace;
19 months ago, by wenzelm
reuse SSH.Server connection database server;
19 months ago, by wenzelm
tuned output;
19 months ago, by wenzelm
make double-sure that this is a transaction context, notably for LOCK TABLE;
19 months ago, by wenzelm