isabelle: Graph

misc tuning: support "scalac -source 3.3";
2023-08-29, by wenzelm
obsolete (see b4e6b82fdb9e);
2023-08-29, by wenzelm
merged
2023-08-27, by wenzelm
update for release;
2023-08-27, by wenzelm
Added tag Isabelle2023-RC4 for changeset 12aac1489f3b
2023-08-27, by wenzelm
minimal documentation for build cluster support;
2023-08-27, by wenzelm
more robust access to local variables;
2023-08-27, by wenzelm
tuned messages: avoid duplicates;
2023-08-27, by wenzelm
removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);
2023-08-27, by wenzelm
tuned error;
2023-08-27, by wenzelm
tuned messages (again);
2023-08-26, by wenzelm
tuned: prefer explicit types;
2023-08-26, by wenzelm
support for Host.dirs;
2023-08-25, by wenzelm
tuned message: failure can happen towards the end, e.g. due to failed sessions or progress.stopped;
2023-08-25, by wenzelm
support multiple host names;
2023-08-25, by wenzelm
clarified default options: SQLite build_database is unsupported for Isabelle2023, due to lack of proper transaction_lock;
2023-08-25, by wenzelm
avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer
2023-08-25, by blanchet
tuned message;
2023-08-25, by wenzelm
tuned;
2023-08-23, by wenzelm
more accurate treatment of state vs. serial vs. db;
2023-08-23, by wenzelm
more explicit check;
2023-08-23, by wenzelm
proper numa_nodes for build_worker;
2023-08-23, by wenzelm
tuned message;
2023-08-23, by wenzelm
tuned;
2023-08-23, by wenzelm
tuned signature;
2023-08-23, by wenzelm
support hosts with shared directory (e.g. NFS);
2023-08-22, by wenzelm
tuned message: failure may stem from build_cluster init;
2023-08-22, by wenzelm
proper sync_database for receive timeout;
2023-08-22, by wenzelm
clarified source structure;
2023-08-22, by wenzelm
tuned whitespace;
2023-08-22, by wenzelm
clarified command-line tools;
2023-08-22, by wenzelm
tuned output;
2023-08-22, by wenzelm
clarified signature;
2023-08-22, by wenzelm
tuned signature;
2023-08-22, by wenzelm
tuned signature;
2023-08-22, by wenzelm
proper sequential evaluation;
2023-08-21, by wenzelm
more robust command options;
2023-08-21, by wenzelm
performance tuning: avoid redundant db access;
2023-08-21, by wenzelm
clarified signature: proper treatment of implicit state (amending d0c9d277620e);
2023-08-21, by wenzelm
performance tuning: avoid redundant db access;
2023-08-21, by wenzelm
performance tuning: avoid multiple db roundtrips;
2023-08-21, by wenzelm
clarified signature: more robust treatment of implicit state;
2023-08-21, by wenzelm
proper sync_database for Database_Progress consumer;
2023-08-21, by wenzelm
tuned message;
2023-08-21, by wenzelm
tuned;
2023-08-21, by wenzelm
tuned messages;
2023-08-21, by wenzelm
tuned signature: removed unused arguments;
2023-08-21, by wenzelm
minor performance tuning: avoid multiple db roundtrips;
2023-08-21, by wenzelm
more operations;
2023-08-21, by wenzelm
tuned;
2023-08-21, by wenzelm
limit size and complexity of bulk transactions;
2023-08-20, by wenzelm
more scalable write_entries and Export.consumer via db.execute_batch_statement;
2023-08-20, by wenzelm
clarified signature: filter batch;
2023-08-19, by wenzelm
more scalable write_messages via db.execute_batch_statement;
2023-08-19, by wenzelm
support for execute_batch: multiple statements in one round-trip;
2023-08-19, by wenzelm
more robust;
2023-08-17, by wenzelm
restrict input_messages to master build_process: avoid excessive db traffic for distributed build_workers;
2023-08-17, by wenzelm
more scalable Database_Progress via asynchronous Consumer_Thread.fork_bulk;
2023-08-17, by wenzelm
clarified main_loop: support timeout, which results in consume(Nil);
2023-08-17, by wenzelm
tuned;
2023-08-17, by wenzelm
clarified signature;
2023-08-17, by wenzelm
tuned signature;
2023-08-17, by wenzelm
tuned signature;
2023-08-16, by wenzelm
build_worker is stopped independently from master build_process;
2023-08-16, by wenzelm
clarified command arguments: optionally restrict to given theories (from theory loader);
2023-08-13, by wenzelm
tuned signature: more operations for formal theory context vs. theory loader;
2023-08-13, by wenzelm
added Isar command 'print_context_tracing';
2023-08-13, by wenzelm
avoid confusion: this is merely about "isabelle dotnet_setup", no codegen yet;
2023-08-13, by wenzelm
avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer
2023-08-25, by blanchet
merged
2023-08-25, by paulson
some refinements in Algebra and Number_Theory
2023-08-24, by paulson
provide Go component
2023-08-25, by Lars Hupel
merged
2023-08-23, by paulson
A subtle fix involving the "measurable" attribute
2023-08-22, by paulson
merged
2023-08-21, by paulson
Numerous minor tweaks and simplifications
2023-08-21, by paulson
substantial tidy-up, shortening many proofs
2023-08-12, by paulson
add Go component
2023-08-23, by Lars Hupel
backed out changeset 2a26d423d9fb: build_log_database not run yet, so this tests the same changesets again;
2023-08-13, by wenzelm
back to post-release mode -- after fork point;
2023-08-10, by wenzelm
Added tag Isabelle2023-RC3 for changeset f5fb5bb2533f
2023-08-10, by wenzelm
clarified option name (see also ff43a524aa5d);
2023-08-10, by wenzelm
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
2023-08-10, by wenzelm
more robust: atomic file-system result via tmp file;
2023-08-10, by wenzelm
removed junk (amending 8cd399b25dac);
2023-08-10, by wenzelm
more robust wrt. undefined state;
2023-08-10, by wenzelm
more informative error;
2023-08-10, by wenzelm
more robust;
2023-08-10, by wenzelm
tuned signature;
2023-08-10, by wenzelm
clarified signature: more explicit types;
2023-08-10, by wenzelm
more informative shasum: show differences explicitly;
2023-08-10, by wenzelm
tuned messages;
2023-08-10, by wenzelm
more robust ancestor_results: avoid total existence failure after build_process has crashed elsewhere;
2023-08-10, by wenzelm
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;
2023-08-10, by wenzelm
merged
2023-08-09, by nipkow
improved simp rule insert_Times_insert (following Dominique Unruh).
2023-08-09, by nipkow
afford multiple tests for arm64_32-darwin on this fast machine;
2023-08-09, by wenzelm
proper history_base for AMR64;
2023-08-09, by wenzelm
tuned
2023-08-09, by nipkow
more robust support for ARM64 platform;
2023-08-08, by wenzelm
proper support for Apple Silicon (ARM64);
2023-08-08, by wenzelm
merged
2023-08-08, by wenzelm
tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;
2023-08-08, by wenzelm
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
2023-08-08, by wenzelm
proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;
2023-08-08, by wenzelm
made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
2023-08-08, by traytel
made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
2023-08-07, by traytel
systematic testing of arm64_32-darwin;
2023-08-07, by wenzelm
more hardware details;
2023-08-07, by wenzelm
update to polyml-219e0a248f70, with more robust support for ARM64;
2023-08-06, by wenzelm
tuned generated README;
2023-08-06, by wenzelm
merged
2023-08-06, by paulson
Tidied up more messy proofs
2023-08-06, by paulson
hints on "hg bisect";
2023-08-06, by wenzelm
no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
2023-08-06, by wenzelm
Removal of ugly old proofs
2023-08-04, by paulson
merged
2023-08-03, by paulson
More cosmetic changes
2023-08-03, by paulson
Cosmetic polishing of proofs
2023-07-27, by paulson
remove debug printing
2023-08-01, by Mathias Fleury
merged
2023-07-27, by nipkow
added mbox-like latex sugar
2023-07-26, by nipkow
Added tag Isabelle2023-RC2 for changeset 53b59fa42696
2023-07-26, by wenzelm
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
2023-07-26, by wenzelm
revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);
2023-07-26, by wenzelm
output panel: don't discard already filtered messages
2023-07-26, by kleing
merged
2023-07-26, by wenzelm
tuned signature: more operations;
2023-07-26, by wenzelm
avoid excessive accumulation of garbage, for profiling of huge sessions;
2023-07-26, by wenzelm
clarified signature: systematic use of Properties.make_string;
2023-07-25, by wenzelm
tuned;
2023-07-25, by wenzelm
support for let in Alethe name bindings;
2023-07-26, by Mathias Fleury
merged
2023-07-25, by paulson
A few more cosmetic changes to proofs
2023-07-25, by paulson
merged
2023-07-17, by paulson
tidying a few proofs a bit more
2023-07-17, by paulson
partly tidied some truly horrible proofs
2023-07-17, by paulson
update for release;
2023-07-25, by wenzelm
back out 9d5e2a08ba1b, hoping the server room stays sufficiently cool;
2023-07-25, 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);
2023-07-25, by wenzelm
clarified statistics;
2023-07-25, by wenzelm
show more build history for AFP;
2023-07-24, by wenzelm
more statistics;
2023-07-24, by wenzelm
proper base_thys;
2023-07-24, by wenzelm
more thorough context tracing;
2023-07-24, by wenzelm
proper check;
2023-07-23, by wenzelm
proper symbolic hostname, as provided via Build_Cluster.Host;
2023-07-23, by wenzelm
unused;
2023-07-23, by wenzelm
clarified signature: Build_Cluster.Session.build_context;
2023-07-23, by wenzelm
clarified exception handling and return_code;
2023-07-23, by wenzelm
tuned signature: more operations;
2023-07-23, by wenzelm
more robust;
2023-07-23, by wenzelm
support for Build_Cluster.Session.init (rsync + Admin/init);
2023-07-23, by wenzelm
prefer Process_Result.RC.merge: strict treatment of interrupt;
2023-07-23, by wenzelm
clarified signature: more operations;
2023-07-23, by wenzelm
proper afp_root;
2023-07-23, by wenzelm
clarified signature: more "object-oriented" style;
2023-07-22, by wenzelm
more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process;
2023-07-22, by wenzelm
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
2023-07-22, by wenzelm
tuned signature;
2023-07-22, by wenzelm
tuned signature;
2023-07-22, by wenzelm
clarified option (see also b66b6cc1eb8c);
2023-07-22, by wenzelm
more build_cluster management: open SSH connections in parallel, but synchronously;
2023-07-21, by wenzelm
tuned signature: more options;
2023-07-21, by wenzelm
clarified signature: more operations;
2023-07-21, by wenzelm
tuned signature;
2023-07-21, by wenzelm
more accurate print vs. parse;
2023-07-21, by wenzelm
clarified signature;
2023-07-21, by wenzelm
clarified signature (again);
2023-07-21, by wenzelm
tuned output;
2023-07-21, by wenzelm
tuned output;
2023-07-21, by wenzelm
clarified modules;
2023-07-21, by wenzelm
more pro-forma support for afp_root;
2023-07-20, by wenzelm
tuned NEWS: emphasize "isabelle build" add-ons;
2023-07-20, by wenzelm
added option -A for AFP root, following "isabelle sync";
2023-07-20, by wenzelm
clarified signature: more operations;
2023-07-20, by wenzelm
tuned signature;
2023-07-20, by wenzelm
clarified file location: to be used by regular Isabelle/Scala tools;
2023-07-20, by wenzelm
update headers;
2023-07-20, by wenzelm
more pro-forma support for Build_Cluster;
2023-07-20, by wenzelm
tuned;
2023-07-20, by wenzelm
tuned;
2023-07-19, by wenzelm
clarified options;
2023-07-19, by wenzelm
clarified options;
2023-07-19, by wenzelm
proper Build_Cluster.Host.parse for parameters and system options;
2023-07-19, by wenzelm
more operations for independent "inline" options;
2023-07-19, by wenzelm
clarified options: accommodate potentially slow database connection;
2023-07-19, by wenzelm
minor performance tuning;
2023-07-19, 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);
2023-07-19, by wenzelm
proper build_options (amending 822ddccda899);
2023-07-19, by wenzelm
clarified options;
2023-07-19, by wenzelm
proforma support for remote build hosts;
2023-07-19, by wenzelm
more options for performance tuning;
2023-07-18, by wenzelm
more operations;
2023-07-18, by wenzelm
support for management of build cluster;
2023-07-18, by wenzelm
clarified modules;
2023-07-18, by wenzelm
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
2023-07-18, by wenzelm
more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh;
2023-07-18, by wenzelm
proper running limit, based on this worker process;
2023-07-18, by wenzelm
more robust: implicit locking of tables in standard order;
2023-07-18, 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;
2023-07-18, by wenzelm
removed unused "create_index": implicit index from primary_key is usually sufficient;
2023-07-18, by wenzelm
clarified "vacuum" (again, reverting 0bd366fad888);
2023-07-18, by wenzelm
clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
2023-07-18, by wenzelm
update for release;
2023-07-18, by wenzelm
merged
2023-07-17, by wenzelm
more elementary transaction implementation (despite fda3f7a158b9 and 9da65bc75610);
2023-07-17, by wenzelm
tuned signature;
2023-07-17, by wenzelm
proper check (amending 234f2ff9afe6);
2023-07-17, by wenzelm
more robust: exclude accidental nesting (synchronized block is re-entrant);
2023-07-17, by wenzelm
clarified errors;
2023-07-17, by wenzelm
removed junk (amending f8e3b228670c);
2023-07-17, by wenzelm
tuned output;
2023-07-17, by wenzelm
reuse SSH.Server connection for database server;
2023-07-17, by wenzelm
tuned source structure;
2023-07-17, by wenzelm
clarified check: uniform session_info_exists;
2023-07-17, by wenzelm
more complete check;
2023-07-17, by wenzelm
clarified signature: more specific exists_table --- avoid retrieving full list beforehand;
2023-07-17, by wenzelm
reuse database_server connection;
2023-07-17, by wenzelm
more informative trace;
2023-07-17, by wenzelm
reuse SSH.Server connection database server;
2023-07-16, by wenzelm
tuned output;
2023-07-16, by wenzelm
make double-sure that this is a transaction context, notably for LOCK TABLE;
2023-07-16, by wenzelm
more robust Java/Scala multithreading: transaction is always connection.synchronized;
2023-07-16, by wenzelm
clarified signature: proper Scala function for command-line tool;
2023-07-16, by wenzelm
tuned signature;
2023-07-16, by wenzelm
clarified signature: more operations;
2023-07-16, by wenzelm
more standard time unit;
2023-07-16, by wenzelm
clarified options;
2023-07-16, by wenzelm
tuned output;
2023-07-16, by wenzelm
global transaction_count;
2023-07-16, by wenzelm
tuned output;
2023-07-16, by wenzelm
tuned output;
2023-07-16, by wenzelm
prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job");
2023-07-16, by wenzelm
clarified isabelle.transaction_log: support time_min (in ms);
2023-07-16, by wenzelm
more operations;
2023-07-16, by wenzelm
more informative trace;
2023-07-16, by wenzelm
support trace of transaction_lock via property "isabelle.transaction_log";
2023-07-16, by wenzelm
proper db.transaction_lock instead of adhoc clone (amending 2df0f3604a67);
2023-07-16, by wenzelm
tuned;
2023-07-16, by wenzelm