isabelle: Graph

tuned message;
23 months ago, by wenzelm
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
23 months ago, by wenzelm
more detailed progress for build_log_database, to see better what happens when;
23 months ago, by wenzelm
clarified signature: explicit Progress date;
23 months ago, by wenzelm
more uniform progress;
23 months ago, by wenzelm
more robust: support concurrent output;
23 months ago, by wenzelm
disable multi-builds (again): does not quite work yet;
23 months ago, by wenzelm
clarified modules;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
proper Compress.Cache;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
more parallelism via consumer thread: with mailbox limit to avoid ressource problems;
23 months ago, by wenzelm
support for mailbox limit;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
23 months ago, by wenzelm
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
23 months ago, by wenzelm
afford multiple tests on fast machines (see also edb4faf666c9 and 2a26d423d9fb);
23 months ago, by wenzelm
performance tuning: parallel and incremental update of build_log_database;
23 months ago, by wenzelm
performance tuning: more careful database access;
23 months ago, by wenzelm
clarified message;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
prefer old-style import "=>";
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
redundant (see also 3069da1743bc);
23 months ago, by wenzelm
removed obsolete table (see also 6acd1a2bd146);
23 months ago, by wenzelm
more robust init_database();
23 months ago, by wenzelm
proper private_data.transaction_lock;
23 months ago, by wenzelm
clarified names;
23 months ago, by wenzelm
proper support for SSH;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
tuned imports;
23 months ago, by wenzelm
add module for faster scheduled builds;
23 months ago, by Fabian Huch
always use host database and make protected;
23 months ago, by Fabian Huch
read relative cpu from build log;
23 months ago, by Fabian Huch
prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);
23 months ago, by Fabian Huch
added start date to build jobs, e.g., for build time estimation;
23 months ago, by Fabian Huch
added initial version of benchmark module, e.g., to compare performance of different hosts;
23 months ago, by Fabian Huch
generalized node infos: allow addressing of numa node segments via relative cpus;
23 months ago, by Fabian Huch
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
23 months ago, by Fabian Huch
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
23 months ago, by Fabian Huch
defined statically known tables of Build_Log;
23 months ago, by Fabian Huch
added lemma
23 months ago, by nipkow
added lemma
23 months ago, by nipkow
added lemma
23 months ago, by nipkow
NEWS and CONTRIBUTORS;
23 months ago, by Fabian Huch
remove unused ci-extras component;
23 months ago, by Fabian Huch
use mail module in CI build;
23 months ago, by Fabian Huch
added mail module;
23 months ago, by Fabian Huch
build javamail component and add to main components;
23 months ago, by Fabian Huch
added component for javax mail;
23 months ago, by Fabian Huch
updated to vampire-4.8;
23 months ago, by wenzelm
tuned README;
23 months ago, by wenzelm
update Vampire version, following hints by Martin Desharnais;
23 months ago, by wenzelm
removed junk;
23 months ago, by wenzelm
tuned component_vampire script for Vampire 4.8 and added new flag to force version name
23 months ago, by desharna
prefer Isabelle options for CI mail settings over ci.properties;
23 months ago, by Fabian Huch
Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal.
23 months ago, by paulson
proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);
23 months ago, by wenzelm
unused (see fe9e590ae52f);
23 months ago, by wenzelm
clarified modules;
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
update documentation on simproc_setup;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
proper morphism;
23 months ago, by wenzelm
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
23 months ago, by wenzelm
more compact ML source;
23 months ago, by wenzelm
more robust read_simproc_spec: proper error positions;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
23 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
23 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
23 months ago, by wenzelm
added ML antiquotation "simproc_setup";
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified syntax and order of parameters;
23 months ago, by wenzelm
clarified signature: Named_Target.setup works both for global and local theory;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified signature: more concise simproc setup in ML;
23 months ago, by wenzelm
clarified signature: more concise variations on implicit theory setup;
23 months ago, by wenzelm
clarified simproc_setup (passive);
23 months ago, by wenzelm
clarified 'simproc_setup';
23 months ago, by wenzelm
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
23 months ago, by wenzelm
more standard simproc_setup in Isar;
23 months ago, by wenzelm
more standard ML setup;
23 months ago, by wenzelm
proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0
23 months ago, by desharna
added new portfolio for Vampire 4.8
23 months ago, by desharna
tuned signature, following Isabelle/Scala;
23 months ago, by wenzelm
more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
proper parallel build tasks;
23 months ago, by wenzelm
more Haskell tests on macOS;
23 months ago, by wenzelm
more NEWS;
23 months ago, by wenzelm
disable naproche component for now: to be updated before the next Isabelle release;
23 months ago, by wenzelm
updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell");
23 months ago, by wenzelm
more NEWS;
23 months ago, by wenzelm
tuned structure;
23 months ago, by wenzelm
update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;
23 months ago, by wenzelm
updated to official release of polyml-5.9.1, based on Ubuntu 18.04 LTS and macOS 11 Big Sur;
23 months ago, by wenzelm
proper options for macOS 11 Big Sur;
23 months ago, by wenzelm
support for official release of polyml-5.9.1;
23 months ago, by wenzelm
updated Linux baseline to Ubuntu 18.04;
23 months ago, by wenzelm
support for macOS 14 Sonoma (only for testing);
23 months ago, by wenzelm
more platform tests: initial support for macOS 14 Sonoma;
23 months ago, by wenzelm
updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
23 months ago, by wenzelm
clarified user errors vs. failures, e.g. java.lang.StackOverflowError;
23 months ago, by wenzelm
further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;
23 months ago, by wenzelm
proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);
23 months ago, by wenzelm
distinguish proper interrupts from Poly/ML RTS breakdown;
23 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
proper Isabelle_Thread.try_catch;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
proper Exn.capture / Isabelle_Thread.try_catch;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
proper Exn.capture;
24 months ago, by wenzelm
more robust: avoid race condition;
24 months ago, by wenzelm
clarified name;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified comments;
24 months ago, by wenzelm
Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts
23 months ago, by paulson
atin now an abbreviation for atin_within, which has been moved to Abstract_Limits
24 months ago, by paulson
merged
24 months ago, by paulson
New proofs also some slightly faster existing proofs
24 months ago, by paulson
updated to hugo-0.119.0;
24 months ago, by Fabian Huch
add component build tool for hugo from afp-devel;
24 months ago, by Fabian Huch
removed test failing on some platform
24 months ago, by desharna
mini2 is not active due to upgrade;
24 months ago, by wenzelm
more PLATFORMS;
24 months ago, by wenzelm
update documentation on Isabelle/ML exceptions;
24 months ago, by wenzelm
misc tuning;
24 months ago, by wenzelm
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
24 months ago, by wenzelm
proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b);
24 months ago, by wenzelm
proper Scala version, e.g. for IntelliJ IDEA;
24 months ago, by wenzelm
NEWS
24 months ago, by desharna
used standard Time.compare in Sledgehammer's preplay
24 months ago, by desharna
moved variable bindings to tighter scope
2023-09-29, by desharna
removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer
2023-09-29, by desharna
removed unused function parameter
2023-09-29, by desharna
merged
2023-09-29, by paulson
A couple of new lemmas
2023-09-29, by paulson
merged
2023-09-29, by wenzelm
more NEWS;
2023-09-29, by wenzelm
explicitly reject 'handle' with catch-all patterns;
2023-09-28, by wenzelm
avoid accidental 'handle' of interrupts;
2023-09-28, by wenzelm
tuned: prefer try-catch/finally over low-level 'handle';
2023-09-28, by wenzelm
clarified treatment of exceptions: avoid catch-all handlers;
2023-09-28, by wenzelm
clarified output vs. error: presence of error messages means error (see also cb7264721c91);
2023-09-28, by wenzelm
tuned;
2023-09-26, by wenzelm
more robust management of resources, using Thread_Attributes.uninterruptible;
2023-09-26, by wenzelm
tuned;
2023-09-26, by wenzelm
clarified signature;
2023-09-26, by wenzelm
more robust management of resources, using Thread_Attributes.uninterruptible;
2023-09-26, by wenzelm
tuned;
2023-09-26, by wenzelm
tuned;
2023-09-26, by wenzelm
tuned signature;
2023-09-26, by wenzelm
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
2023-09-26, by wenzelm
clarified signature;
2023-09-25, by wenzelm
clarified modules;
2023-09-25, by wenzelm
unused;
2023-09-25, by wenzelm
clarified order of modules: early access to interrupt management of Isabelle_Threads;
2023-09-25, by wenzelm
tuned: prefer antiquotation for try-catch;
2023-09-25, by wenzelm
tuned: prefer antiquotation for try-catch;
2023-09-25, by wenzelm
tuned: prefer antiquotation for try-finally;
2023-09-25, by wenzelm
omit pointless capture/release (see also 469a375212c1);
2023-09-25, by wenzelm
omit pointless capture/release (see also 26774ccb1c74);
2023-09-25, by wenzelm
clarified signature: avoid association with potentially dangerous Exn.capture;
2023-09-25, by wenzelm
more robust: catch/finally part is uninterruptible;
2023-09-25, by wenzelm
more position information, e.g. for warning about fn-pattern;
2023-09-25, by wenzelm
unused;
2023-09-25, by wenzelm
more general ML_Antiquotation.special_form;
2023-09-25, by wenzelm
Importing or moving a few more useful theorems
2023-09-27, by paulson
merged
2023-09-25, by paulson
A few new theorems
2023-09-25, by paulson
avoid legacy binding errors in Sledgehammer Isar proofs
2023-09-25, by blanchet
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
2023-09-25, by blanchet
added argo
2023-09-25, by blanchet
allow (~) syntax in TPTP proofs for unapplied negation
2023-09-25, by blanchet
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
2023-09-25, by blanchet
use same associativity as Isabelle when parsing HOL proofs
2023-09-25, by blanchet
improved Sledgehammer's HOL proof parser w.r.t. negation
2023-09-25, by blanchet
clarified signature;
2023-09-24, by wenzelm
clarified signature;
2023-09-24, by wenzelm
clarified signature;
2023-09-24, by wenzelm
minor performance tuning;
2023-09-24, by wenzelm
merged
2023-09-23, by paulson
A few new or simplified proofs
2023-09-23, by paulson
tuned: more standard order;
2023-09-22, by wenzelm
clarified signature;
2023-09-22, by wenzelm
proper fontenc for cartouches (amending d052d61da398);
2023-09-22, by wenzelm
clarified modules;
2023-09-21, by wenzelm
clarified signature;
2023-09-21, by wenzelm
clarified modules;
2023-09-21, by wenzelm
tuned;
2023-09-21, by wenzelm
more robust: prefer linear data flow;
2023-09-21, by wenzelm
added first proof reconstruction test for Sledgehammer
2023-09-20, by desharna
tuned;
2023-09-19, by wenzelm
clarified signature;
2023-09-19, by wenzelm
clarified signature (again): follow Isabelle/Java/Scala;
2023-09-19, by wenzelm
tuned (following 69c6d3e87660);
2023-09-19, by wenzelm
tuned --- avoid pointless indirection (see also a2df9de46060);
2023-09-19, by wenzelm
(pointlessly) get rid of some simp calls within "proof"
2023-09-17, by paulson
reduced prominence of lemma names
2023-09-16, by haftmann
new formulation of an auxiliary lemma
2023-09-16, by haftmann
A few more inclusion-exclusion theorems from HOL Light
2023-09-15, by paulson
Corrected type calculation.
2023-09-14, by haftmann
some hints on managed installations
2023-09-13, by haftmann
prefer cartouches over quotes for clarity of resulting document
2023-09-13, by haftmann
A little reorganisation
2023-09-12, by paulson
post-release updates;
2023-09-11, by wenzelm
merged
2023-09-11, by wenzelm
Added tag Isabelle2023 for changeset b5f3d1051b13
2023-09-11, by wenzelm
tuned; Isabelle2023
2023-09-11, by wenzelm
misc tuning;
2023-09-11, by wenzelm
documentation for the "Document" panel in Isabelle/jEdit;
2023-09-10, by wenzelm
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
2023-09-09, by paulson
merged
2023-09-09, by paulson
merged
2023-08-26, by paulson
tidying up old apply-style proofs
2023-08-26, by paulson
allow higher-order unification of open terms (reviewed by Larry Paulson)
2023-09-07, by Kevin Kappelmann
merged
2023-09-06, by wenzelm
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
2023-09-06, by wenzelm
add ML_system_pp for type Isabelle_Thread.T;
2023-09-06, by wenzelm
more explicit type Isabelle_Thread.T;
2023-09-06, by wenzelm
discontinue somewhat pointless thread tracing/debugging: without PIDE command context, messages are not shown, and Exn.trace hardly works anyway (see also de20fccf6509 and 447972249785);
2023-09-04, by wenzelm
tuned whitespace;
2023-09-04, by wenzelm
tuned Sledgehammer messages
2023-09-05, by blanchet
respect timeout better
2023-09-05, by blanchet
merged
2023-09-03, by wenzelm
Added tag Isabelle2023-RC5 for changeset ffa417b5c913
2023-09-03, by wenzelm
tuned;
2023-09-03, by wenzelm
tuned messages;
2023-09-03, by wenzelm