Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
merged
23 months ago, by paulson
fixed the simplification of Suc n - 1
23 months ago, by paulson
tuned whitespace;
23 months ago, by wenzelm
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;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
proper Isabelle_Thread.try_catch;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
proper Exn.capture / Isabelle_Thread.try_catch;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
proper Exn.capture;
23 months ago, by wenzelm
more robust: avoid race condition;
23 months ago, by wenzelm
clarified name;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
clarified comments;
23 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
23 months ago, by paulson
merged
23 months ago, by paulson
New proofs also some slightly faster existing proofs
24 months ago, by paulson
updated to hugo-0.119.0;
23 months ago, by Fabian Huch
add component build tool for hugo from afp-devel;
23 months ago, by Fabian Huch
removed test failing on some platform
23 months ago, by desharna
mini2 is not active due to upgrade;
23 months ago, by wenzelm
more PLATFORMS;
23 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
24 months ago, by desharna
removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer
24 months ago, by desharna
removed unused function parameter
24 months ago, by desharna
merged
24 months ago, by paulson
A couple of new lemmas
24 months ago, 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
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
tip