isabelle: Graph

more accurate progress.now(), notably for Database_Progress;
10 months ago, by wenzelm
update NEWS;
10 months ago, by wenzelm
activate E 3.0 after testing by Martin Desharnais, see also db72d9920186 and 788f11af9822;
10 months ago, by wenzelm
merged
10 months ago, by desharna
added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]
10 months ago, by desharna
parallelize schedule optimization;
10 months ago, by Fabian Huch
revised NEWS: OCaml / OPAM appears to be fine on arm64-linux, e.g. Ubuntu 22.04;
10 months ago, by wenzelm
update to current long-term-support version dotnet-8.0.x;
10 months ago, by wenzelm
merged
10 months ago, by wenzelm
proper release bundle_name (amending 0e7dd3eaa6e8);
10 months ago, by wenzelm
more multiset lemmas
10 months ago, by blanchet
optional cartouche syntax and proper name printing in atp Isar output
10 months ago, by Simon Wimmer
merged
10 months ago, by desharna
removed unused variable
10 months ago, by desharna
added virtual, greedy portfolio for E 3.0
10 months ago, by desharna
tuned;
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
Added tag Isabelle2024-RC0 for changeset 98f009f56400
10 months ago, by wenzelm
updated for release;
10 months ago, by wenzelm
updated for release;
10 months ago, by wenzelm
clarified signature;
10 months ago, by wenzelm
misc tuning for release;
10 months ago, by wenzelm
tuned whitespace: avoid TABs;
10 months ago, by wenzelm
avoid suspicious Unicode;
10 months ago, by wenzelm
tuned whitespace;
10 months ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
10 months ago, by wenzelm
merged
10 months ago, by wenzelm
update NEWS;
10 months ago, by wenzelm
update cygwin near 3.5.1-1, also see https://cygwin.com/pipermail/cygwin-announce/2024-February/011524.html and https://cygwin.com/pipermail/cygwin-announce/2024-February/011611.html
10 months ago, by wenzelm
drop unused Task.info field;
10 months ago, by wenzelm
proper guard_time (amending 752806151432);
10 months ago, by wenzelm
proper dynamic access (amending c3f07c950116);
10 months ago, by wenzelm
more robust, notably for remote process (via SSH);
10 months ago, by wenzelm
prefer dynamic objects, following a5fda30edae2;
10 months ago, by wenzelm
proper dynamic access (amending 52b5c7c8e6d9);
10 months ago, by wenzelm
clarified signature: incorporate guard into Logger;
10 months ago, by wenzelm
merged
10 months ago, by desharna
added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp
10 months ago, by desharna
Moving valuable library material from Martingales into the distribution
10 months ago, by paulson
clarified signature;
10 months ago, by wenzelm
clarified module signature and state;
10 months ago, by wenzelm
tuned messages;
10 months ago, by wenzelm
omit somewhat pointless message, following b7187d4cdf68;
10 months ago, by wenzelm
more robust handling of uninitialized value, notably Build_Process.progress;
10 months ago, by wenzelm
tuned
10 months ago, by nipkow
partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded;
10 months ago, by Fabian Huch
clarified module signature and state;
10 months ago, by wenzelm
tuned signature: more protected operations;
10 months ago, by wenzelm
database performance tuning: just one synchronized_database for main loop body;
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b);
10 months ago, by wenzelm
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
10 months ago, by wenzelm
tuned;
10 months ago, by wenzelm
tuned proof: avoid z3 to make it work on arm64-linux;
10 months ago, by wenzelm
official support for arm64-linux, despite a few missing tools;
10 months ago, by wenzelm
discontinue unstable z3-4.4.1 for arm64-linux from Debian (in contrast to 796ae338eb9d and 87718883c8b9);
10 months ago, by wenzelm
proper platform_name/platform_dir for native arm64-darwin: already published in 788f11af9822 after manual adjustment;
10 months ago, by wenzelm
update to scala-3.3.3;
10 months ago, by wenzelm
provide e-3.0.03 on all platforms, including arm64-linux and arm64-darwin --- still inactive;
10 months ago, by wenzelm
update NEWS, following 0d7c7fe65638;
10 months ago, by Fabian Huch
provide cvc5-1.1.1 for testing --- still inactive;
10 months ago, by wenzelm
rebuild bash_process executables on current reference platforms, including native arm64-darwin;
10 months ago, by wenzelm
tuned NEWS, see also c62003e05e46;
10 months ago, by wenzelm
update NEWS, following ea1913c953ef;
10 months ago, by wenzelm
tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:";
10 months ago, by wenzelm
more explicit NEWS (see 3648e9c88d0c);
10 months ago, by wenzelm
NEWS for a53287d9add3, 3e30ca77ccfe;
10 months ago, by wenzelm
add option for unify trace (now disabled by default as printing is excessive and rarely used);
10 months ago, by Fabian Huch
tuned unify trace option names;
10 months ago, by Fabian Huch
more scalable: avoid potentially expensive ordering of underlying key data type, e.g. in MESON.Cache of Naproche;
10 months ago, by wenzelm
updated to stack-2.15.1, lts-22.6, ghc-9.6.3;
10 months ago, by wenzelm
merged
10 months ago, by nipkow
tuned name
10 months ago, by nipkow
new simplifier trace_op for tracing simproc calls
10 months ago, by nipkow
merged
10 months ago, by paulson
Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers
10 months ago, by paulson
support Zipperposition's skolemization in generated Isar proofs
10 months ago, by blanchet
improved output in simps_case_conv;
10 months ago, by Fabian Huch
improved output in inductive module;
10 months ago, by Fabian Huch
simplifier: no trace info from simprocs unless simp_debug = true.
10 months ago, by nipkow
deal with new-style Vampire skolemization in reconstructed Isar proofs
10 months ago, by blanchet
database performance tuning: prefer light-weight IPC over heavy-duty transactions;
10 months ago, by wenzelm
tuned signature;
10 months ago, by wenzelm
tuned signature: follow PostgreSQL syntax instead of JDBC API;
10 months ago, by wenzelm
more robust shutdown: interruptible database connection;
10 months ago, by wenzelm
clarified signature: more convenient send/receive operations;
10 months ago, by wenzelm
clarified versions for documentation;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
clarified signature: avoid hardwired values;
11 months ago, by wenzelm
clarified IPC via database server: receive notifications quasi-spontaneously via auxiliary thread;
11 months ago, by wenzelm
minor performance tuning: just 1 transaction for slices <= 1;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned whitespace;
11 months ago, by wenzelm
tuned signature;
11 months ago, by wenzelm
clarified signature: fewer warnings in IntelliJ IDEA;
11 months ago, by wenzelm
removed unused database_server (amending 32ca3d1283de);
11 months ago, by wenzelm
timing function generation bug fix by Jonas Stahl
11 months ago, by nipkow
tuned signature: more types, fewer warnings in IntelliJ IDEA;
11 months ago, by wenzelm
new less ad hoc implementation of the 'moura' tactic for skolemization
11 months ago, by blanchet
more thorough Store.clean_output (amending 1fa1b32b0379);
11 months ago, by wenzelm
clarified signature: Build_Process tells how to clean sessions;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
minor performance tuning;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned signature;
11 months ago, by wenzelm
tuned, following 7a1153c95bf9;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
11 months ago, by wenzelm
proper usage;
11 months ago, by wenzelm
recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
more robust: make double-sure that heap digest is present;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
minor performance tuning: just one transaction for log_db without heap;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
proper store.cache.compress;
11 months ago, by wenzelm
tuned whitespace;
11 months ago, by wenzelm
clarified store_session: heap requires process_result.ok, but log_db is always stored;
11 months ago, by wenzelm
unused;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned names;
11 months ago, by wenzelm
tuned names;
11 months ago, by wenzelm
clarified database layout;
11 months ago, by wenzelm
tuned signature;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
more accurate types;
11 months ago, by wenzelm
build local log_db, with store/restore via optional database server;
11 months ago, by wenzelm
propagate property "isabelle.debug", notably for Java/Scala exception trace;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0);
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
clarified names;
11 months ago, by wenzelm
more explicit build_cluster flag to guard open_build_database server;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
simplified specification of type class semiring_bits
11 months ago, by haftmann
New material about transcendental functions, polynomials, et cetera, thanks to Manuel Eberl
11 months ago, by paulson
merged
11 months ago, by paulson
A small collection of new and useful facts, including the AM-GM inequality
11 months ago, by paulson
remove selected occurrences of 'moura' tactic
11 months ago, by blanchet
added lemmas relpowp_left_unique and relpow_left_unique
11 months ago, by desharna
added lemmas relpowp_right_unique and relpow_right_unique
11 months ago, by desharna
use define_time_fun
11 months ago, by nipkow
time funs: +1 instead of 1+
11 months ago, by nipkow
minor performance tuning;
11 months ago, by wenzelm
clarified signature: more comprehensive operations;
11 months ago, by wenzelm
clarified signature: more explicit types;
11 months ago, by wenzelm
clarified signature: emphasize physical db files;
11 months ago, by wenzelm
tuned: afford untyped/unscoped update;
11 months ago, by wenzelm
clarified signature: avoid ill-defined type java.net.URL;
11 months ago, by wenzelm
unused;
11 months ago, by wenzelm
tuned: afford untyped/unscoped update;
11 months ago, by wenzelm
more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML;
11 months ago, by wenzelm
clarified signature: more explicit types/scopes;
11 months ago, by wenzelm
tuned names;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
tuned documentation;
11 months ago, by wenzelm
more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;
11 months ago, by wenzelm
clarified modules: centralize default policy;
11 months ago, by wenzelm
more explicit types --- fewer warnings in IntelliJ IDEA;
11 months ago, by wenzelm
tuned: avoid shadowing of names;
11 months ago, by wenzelm
clarified default "isabelle build -j0 -H";
11 months ago, by wenzelm
tuned whitespace;
11 months ago, by wenzelm
clarifier worker vs. master, which may coincide for local build;
11 months ago, by wenzelm
clarified signature: more standard defaults;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
prefer static object, while class is required for "services";
11 months ago, by wenzelm
clarified signature: prefer default;
11 months ago, by wenzelm
merged
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
more robust: check subclasses as well;
11 months ago, by wenzelm
more robust;
11 months ago, by wenzelm
support for alternative user home, e.g. to avoid slow NFS shares;
11 months ago, by wenzelm
support explicit USER_HOME within SSH session;
11 months ago, by wenzelm
tuned;
11 months ago, by wenzelm
merged
11 months ago, by paulson
Further adjustments to the syntax for Lebesgue integration
11 months ago, by paulson
tuned comments;
11 months ago, by wenzelm
more robust: always close, despite failure;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned signature;
11 months ago, by wenzelm
tuned comments;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury
11 months ago, by blanchet
tuned whitespace;
11 months ago, by wenzelm
prefer static object, while class is required for "services" (see 47eb96592aa2);
11 months ago, by wenzelm
clarified directories;
11 months ago, by wenzelm
tuned signature;
11 months ago, by wenzelm
tuned: prefer explicit update operation for immutable options;
11 months ago, by wenzelm
tuned message;
11 months ago, by wenzelm
more robust type, with explicit default;
11 months ago, by wenzelm
tuned usage message;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
more robust defaults;
11 months ago, by wenzelm
merged
11 months ago, by desharna
added lemmas relpow_trans[trans] and relpowp_trans[trans]
11 months ago, by desharna
more on disjunctive addition/subtraction
11 months ago, by haftmann
merged
11 months ago, by wenzelm
prefer physical processors (see also 4b014e6c1dfe and 26a43785590b);
11 months ago, by wenzelm
more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
11 months ago, by wenzelm
more robust default;
11 months ago, by wenzelm
more accurate, notably on lxbroy10 and vmnipkow9;
11 months ago, by wenzelm
clarified num_processors: follow Poly/ML (with its inaccuracies);
11 months ago, by wenzelm
clarified modules, following Isabelle/ML;
11 months ago, by wenzelm
clarified signature;
11 months ago, by wenzelm
tuned comments;
11 months ago, by wenzelm
merged
11 months ago, by paulson
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
11 months ago, by paulson
merged
11 months ago, by paulson
A few lemmas brought in from AFP entries
11 months ago, by paulson
merged
11 months ago, by traytel
made destructor-view tactic more robust (by Jan van Brügge)
11 months ago, by traytel
performance optimization;
11 months ago, by Fabian Huch
clarified names;
11 months ago, by Fabian Huch
clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4);
11 months ago, by Fabian Huch
proper "linux_arm", amending 76ad72736e9e;
11 months ago, by wenzelm
more lemmas
11 months ago, by haftmann
new lemmas involving Ramsey numbers, infinite sets
11 months ago, by paulson
simplified class specification
11 months ago, by haftmann
Removal of duplicate code
11 months ago, by paulson