Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
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.
tuned;
default
tip
8 hours ago, by Fabian Huch
removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML);
6 hours ago, by wenzelm
clarified signature;
6 hours ago, by wenzelm
clarified modules: more official Sessions.notable_groups;
7 hours ago, by wenzelm
tuned
7 hours ago, by nipkow
merged
8 hours ago, by paulson
An assortment of new material, mostly due to Manuel
8 hours ago, by paulson
rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;
10 hours ago, by wenzelm
tuned signature;
11 hours ago, by wenzelm
tuned;
11 hours ago, by wenzelm
tuned signature;
12 hours ago, by wenzelm
merged
15 hours ago, by desharna
added lemma wfp_on_image and author name to theory
35 hours ago, by desharna
proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;
24 hours ago, by wenzelm
proper "isabelle go_setup" for Jenkins;
25 hours ago, by wenzelm
dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);
25 hours ago, by wenzelm
tuned message;
29 hours ago, by wenzelm
merged
29 hours ago, by wenzelm
tuned NEWS;
29 hours ago, by wenzelm
support for "all" platforms;
30 hours ago, by wenzelm
clarified signature;
30 hours ago, by wenzelm
merged
30 hours ago, by nipkow
updated time functions for Array_Braun
30 hours ago, by nipkow
merged
31 hours ago, by paulson
New material and a bit of refactoring
31 hours ago, by paulson
remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and 37f852399a32);
31 hours ago, by wenzelm
tuned;
32 hours ago, by wenzelm
more robust Markdown;
32 hours ago, by wenzelm
misc tuning;
32 hours ago, by wenzelm
run "isabelle components_build -u";
33 hours ago, by wenzelm
remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup";
33 hours ago, by wenzelm
tuned order;
33 hours ago, by wenzelm
more Setup_Tool services;
34 hours ago, by wenzelm
clarified signature;
34 hours ago, by wenzelm
proper SSH operations;
34 hours ago, by wenzelm
tuned signature: more permissive;
34 hours ago, by wenzelm
clarified signature: explicit variable is easier to find in source;
34 hours ago, by wenzelm
proper services for Setup_Tool --- avoid hardwired stuff;
34 hours ago, by wenzelm
merged
36 hours ago, by desharna
renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal
2 days ago, by desharna
more robust XML body: allow empty text, as well as arbitrary pro-forma markup (e.g. see XML.blob in Isabelle/ML);
2 days ago, by wenzelm
more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51);
2 days ago, by wenzelm
misc tuning for release;
2 days ago, by wenzelm
merged;
2 days ago, by wenzelm
NEWS for "isabelle go_setup";
2 days ago, by wenzelm
proper platform_path for Windows;
2 days ago, by wenzelm
misc tuning, following go_setup;
2 days ago, by wenzelm
dynamic setup of Go component, similar to Dotnet;
2 days ago, by wenzelm
tuned comments;
2 days ago, by wenzelm
clarified signature: more operations;
2 days ago, by wenzelm
clarified signature: explicit type Platform.Info with derived operations;
2 days ago, by wenzelm
less ambitious parallelism: avoid exhaustion of memory (64GB total);
2 days ago, by wenzelm
provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup";
2 days ago, by wenzelm
tuned;
2 days ago, by wenzelm
tuned messages;
2 days ago, by wenzelm
update to bash_process-20240326;
2 days ago, by wenzelm
build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all platform directories (e.g. for SSH upload);
2 days ago, by wenzelm
clarified meaning of platform.props: update on default;
2 days ago, by wenzelm
allow raw input in HTML (e.g., for web applications);
2 days ago, by Fabian Huch
added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on
2 days ago, by desharna
merged
2 days ago, by desharna
added lemma wf_on_iff_wf
3 days ago, by desharna
changed number of consumed assumptions of wf_on_induct and wfp_on_induct
3 days ago, by desharna
obsolete: base-line is macOS 11;
3 days ago, by wenzelm
more robust: always assume x86_64 (or its emulation on ARM);
3 days ago, by wenzelm
MLton lacks arm64-linux (see also 84f2d481d6d7);
3 days ago, by wenzelm
more ambitious test "AFP (macOS 14 Sonoma, Apple Silicon)", as replacement for AFP on lrzcloud2;
3 days ago, by wenzelm
update to stack-2.15.3, stackage-lts-22.6, ghc-9.6.4;
3 days ago, by wenzelm
tuned;
3 days ago, by wenzelm
merged
3 days ago, by wenzelm
misc updates, tuning and clarification;
3 days ago, by wenzelm
reformat source in jEdit (wrap margin 78);
3 days ago, by wenzelm
more accurate Markdown formatting, both for VSCode and Phabricator;
3 days ago, by wenzelm
just one README.md;
3 days ago, by wenzelm
tuned
3 days ago, by nipkow
merged
3 days ago, by wenzelm
more accurate platform directories: pkg/tool structure is hardwired in "go";
3 days ago, by wenzelm
support for etc/platform.props, to specify multi-platform directory structure more accurately;
3 days ago, by wenzelm
clarified signature;
4 days ago, by wenzelm
tuned;
4 days ago, by wenzelm
clarified modules;
4 days ago, by wenzelm
clarified modules;
4 days ago, by wenzelm
build Isabelle component for Go: all platforms;
4 days ago, by wenzelm
misc tuning;
4 days ago, by wenzelm
just one copy of darwin-universal.tar.gz;
4 days ago, by wenzelm
documented running time function framework by Jonas Stahl
3 days ago, by nipkow
merged
3 days ago, by desharna
redefined wf as an abbreviation for "wf_on UNIV"
5 days ago, by desharna
merged
4 days ago, by nipkow
more uniform command names
4 days ago, by nipkow
tuned parameter order
4 days ago, by nipkow
shutdown lrzcloud2;
4 days ago, by wenzelm
tuned NEWS
5 days ago, by desharna
redefined wfP as an abbreviation for "wfp_on UNIV"
7 days ago, by desharna
merged
6 days ago, by desharna
added lemma wellorder.wfp_on_less[simp]
8 days ago, by desharna
merged
7 days ago, by wenzelm
suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
7 days ago, by wenzelm
update to sumatra_pdf-3.5.2;
7 days ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
7 days ago, by wenzelm
update to jsoup-1.17.2;
7 days ago, by wenzelm
proper bib entries (amending 82aaa0d8fc3b);
7 days ago, by wenzelm
update to dotnet-8.0.203;
7 days ago, by wenzelm
enforce rebuild of Isabelle/ML;
7 days ago, by wenzelm
update to sqlite-3.45.2.0: clarified component name, following postgresql;
7 days ago, by wenzelm
activate postgresql-42.7.3;
7 days ago, by wenzelm
update to postgresql-42.7.3;
7 days ago, by wenzelm
update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64-darwin;
7 days ago, by wenzelm
isabelle update -u cite;
7 days ago, by wenzelm
raise error if benchmarking fails;
7 days ago, by Fabian Huch
option for benchmark session;
7 days ago, by Fabian Huch
add hosts option to run benchmark on the cluster from the command-line;
7 days ago, by Fabian Huch
only start jobs early if they are due (cf. 1966578feff8);
8 days ago, by Fabian Huch
New material from a variety of sources (including AFP)
7 days ago, by paulson
build component for cvc5-latest (ef2bc3f735df);
8 days ago, by wenzelm
merged
8 days ago, by desharna
try proof method "order" in Sledgehammer's proof reconstruction
8 days ago, by desharna
added Mirabelle action "order"
8 days ago, by desharna
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
8 days ago, by desharna
tuned proof
8 days ago, by desharna
added lemma order_reflclp_if_transp_and_asymp
8 days ago, by desharna
added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on
8 days ago, by desharna
HOL-Library: added modulo/congruence for real numbers
8 days ago, by Manuel Eberl
only print schedule if relevant;
8 days ago, by Fabian Huch
remove laziness: no need, and errors during initialization loop with close();
8 days ago, by Fabian Huch
more general definition of meromorphicity; Weierstraß factorisation theorem
8 days ago, by Manuel Eberl
always provide build_database_server option in benchmark command;
8 days ago, by Fabian Huch
always check if node is defined, e.g. for exists_next operation wit empty schedule;
8 days ago, by Fabian Huch
fixed typo
9 days ago, by blanchet
disable taskset for now: performance impact is negative;
9 days ago, by Fabian Huch
allow specifying initial schedule;
11 days ago, by Fabian Huch
clarify use of num_threads vs. max_cpus;
11 days ago, by Fabian Huch
clarified host: pre-load max threads;
11 days ago, by Fabian Huch
clarified: more operations;
11 days ago, by Fabian Huch
added alias wfp for wfP
11 days ago, by desharna
merged
11 days ago, by desharna
added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset
11 days ago, by desharna
start scheduled jobs earlier, if possible;
11 days ago, by Fabian Huch
tuned proofs
11 days ago, by desharna
added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal
11 days ago, by desharna
merged
11 days ago, by desharna
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
12 days ago, by desharna
read/write proper schedule date (amending 9da3019e1ee5);
12 days ago, by Fabian Huch
allow read/write of schedule in build (read via option, write from tool);
12 days ago, by Fabian Huch
file representation for schedule (e.g., for generating from external tool);
12 days ago, by Fabian Huch
proper median/mean time;
12 days ago, by Fabian Huch
remove schedule outdated limit: delay is sufficient;
12 days ago, by Fabian Huch
tuned whitespace;
12 days ago, by Fabian Huch
tie-breaking in schedule optimization to pick best schedule even when run-time is dominated by large task (e.g., session with long timeout but no data yet);
12 days ago, by Fabian Huch
tuned;
12 days ago, by Fabian Huch
remove old build before generating schedule;
12 days ago, by Fabian Huch
unused;
12 days ago, by Fabian Huch
merged
13 days ago, by desharna
added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image
13 days ago, by desharna
clarified names;
13 days ago, by wenzelm
sketch & explore: TODO comments are addressed in parent commits
2 weeks ago, by Simon Wimmer
sketch & explore: reduce unnecessary type constraints
2 weeks ago, by Simon Wimmer
sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
2 weeks ago, by Simon Wimmer
sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
2 weeks ago, by Simon Wimmer
change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
13 days ago, by Fabian Huch
unused;
2 weeks ago, by Fabian Huch
tuned;
2 weeks ago, by Fabian Huch
proper IPC for scheduled builds, following 7ae25372ab04;
2 weeks ago, by Fabian Huch
proper check (amending 9aef1d1535ff);
2 weeks ago, by Fabian Huch
more synced options (following 6e5397fcc41b);
2 weeks ago, by Fabian Huch
avoid [no_atp] declations shadowing propositions from sledgehammer
2 weeks ago, by haftmann
track start in build job results (following 9d484c5d3a63), so it can directly be written to build log database;
2 weeks ago, by Fabian Huch
use inherited build_start, following d9fc2cc37694;
2 weeks ago, by Fabian Huch
update NEWS + CONTRIBUTORS for release;
2 weeks ago, by wenzelm
Tuned proofs
2 weeks ago, by haftmann
merged
2 weeks ago, by wenzelm
revert most parts of 0e79fa88cab6: somewhat ambitious attempt to move towards "editing" builds via added/canceled workers;
2 weeks ago, by wenzelm
database performance tuning: prefer light-weight IPC over heavy-duty transactions, following bf377e10ff3b;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned whitespace;
2 weeks ago, by wenzelm
proper system option, instead of hardwired default;
2 weeks ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
2 weeks ago, by wenzelm
tuned comments;
2 weeks ago, by wenzelm
clarified build schedule host: proper module;
2 weeks ago, by Fabian Huch
remove unused dummy;
2 weeks ago, by Fabian Huch
tuned;
2 weeks ago, by Fabian Huch
use timeout as default build time predictor if no data is available;
2 weeks ago, by Fabian Huch
merged
2 weeks ago, by paulson
Restored Riemann_Mapping as an import of Complex_Analysis
2 weeks ago, by paulson
proper file headers;
2 weeks ago, by wenzelm
clarified modules;
2 weeks ago, by wenzelm
merged
2 weeks ago, by wenzelm
database performance tuning: pull changed entries only, based on recorded updates (see 98d65411bfdb);
2 weeks ago, by wenzelm
tuned signature: more operations;
2 weeks ago, by wenzelm
clarified signature: more explicit types;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
removed somewhat pointless check;
2 weeks ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
2 weeks ago, by wenzelm
merged
2 weeks ago, by paulson
Fixed a latex error in the markup
2 weeks ago, by paulson
minor performance tuning: SQL.order_by is only for demo purposes;
2 weeks ago, by wenzelm
support efficient access to state updates, based on LEFT OUTER JOIN;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
tuned: prefer if_proper expression;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
tuned: prefer if_proper expression;
2 weeks ago, by wenzelm
New material by Wenda Li and Manuel Eberl
2 weeks ago, by paulson
merged
2 weeks ago, by traytel
export BNF properties about the cardinal bound (by Jan van Brügge)
2 weeks ago, by traytel
unused (see 123f2c0995b8);
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
more robust init_built: get_build_id and start_build within the same transaction;
2 weeks ago, by wenzelm
tuned: remove redundant guard;
2 weeks ago, by wenzelm
maintain short build_id vs. build_uuid, similar to Database_Progress context/context_uuid;
2 weeks ago, by wenzelm
more operations;
2 weeks ago, by wenzelm
clarified signature: init_state vs. init_unsynchronized;
2 weeks ago, by wenzelm
more thorough "isabelle build_process -C -r -f";
2 weeks ago, by wenzelm
more operations;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
tuned signature: more uniform SQL.Data instances;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
disable write_updates from f425bbc4b2eb for now: "isabelle build_process -rf" does not quite work yet;
2 weeks ago, by wenzelm
revert part of 5969ead9f900 that does not quite work yet: only one accidental host is used;
2 weeks ago, by wenzelm
record updates within database, based on serial;
2 weeks ago, by wenzelm
proper tables (amending 4611b7b47b42);
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
clarified signature: improved data integrity;
2 weeks ago, by wenzelm
clarified modules;
2 weeks ago, by wenzelm
clarified modules;
2 weeks ago, by wenzelm
obsolete;
2 weeks ago, by wenzelm
misc tuning: prefer Build_Process.Update operations;
2 weeks ago, by wenzelm
misc tuning and clarification: prefer explicit type Build_Process.Update;
2 weeks ago, by wenzelm
misc tuning and clarification;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
clarified data representation: more uniform treatment of State.Pending vs. State.Running;
2 weeks ago, by wenzelm
tuned: drop pointless SQL.order_by (see also 5f706f7c624b);
2 weeks ago, by wenzelm
upgrade pretty_maybe_quote following 2746dfc9ceae;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
eliminate odd aliases (see also 2746dfc9ceae);
2 weeks ago, by wenzelm
tuned signature: prefer bottom-up construction;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
tuned signature;
2 weeks ago, by wenzelm
clarified signature;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
more operations for Build_Log.Meta_Info: prefer explicit types;
2 weeks ago, by wenzelm
more operations for Date and Time;
2 weeks ago, by wenzelm
more accurate patterns --- reverting unused fc3ba0a1c82f;
2 weeks ago, by wenzelm
remove unused/fragile option (amending db37cae970a6) --- universal_table requires pull_date tables;
2 weeks ago, by wenzelm
prefer explicit option "build_log_verbose";
2 weeks ago, by wenzelm
tuned whitespace;
2 weeks ago, by wenzelm
additional build_log column "session_start", with implicit upgrade of database schema;
2 weeks ago, by wenzelm
more robust build_start for master and workers (via database);
2 weeks ago, by wenzelm
more accurate progress.now(), notably for Database_Progress;
2 weeks ago, by wenzelm
update NEWS;
2 weeks ago, by wenzelm
activate E 3.0 after testing by Martin Desharnais, see also db72d9920186 and 788f11af9822;
2 weeks ago, by wenzelm
merged
2 weeks ago, by desharna
added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]
4 weeks ago, by desharna
parallelize schedule optimization;
3 weeks ago, by Fabian Huch
revised NEWS: OCaml / OPAM appears to be fine on arm64-linux, e.g. Ubuntu 22.04;
3 weeks ago, by wenzelm
update to current long-term-support version dotnet-8.0.x;
3 weeks ago, by wenzelm
merged
3 weeks ago, by wenzelm
proper release bundle_name (amending 0e7dd3eaa6e8);
3 weeks ago, by wenzelm
more multiset lemmas
3 weeks ago, by blanchet
optional cartouche syntax and proper name printing in atp Isar output
4 weeks ago, by Simon Wimmer
merged
3 weeks ago, by desharna
removed unused variable
3 weeks ago, by desharna
added virtual, greedy portfolio for E 3.0
3 weeks ago, by desharna
tuned;
3 weeks ago, by wenzelm
tuned signature;
3 weeks ago, by wenzelm
Added tag Isabelle2024-RC0 for changeset 98f009f56400
3 weeks ago, by wenzelm
updated for release;
Isabelle2024-RC0
3 weeks ago, by wenzelm
updated for release;
3 weeks ago, by wenzelm
clarified signature;
3 weeks ago, by wenzelm
misc tuning for release;
3 weeks ago, by wenzelm
tuned whitespace: avoid TABs;
3 weeks ago, by wenzelm
avoid suspicious Unicode;
3 weeks ago, by wenzelm
tuned whitespace;
3 weeks ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
3 weeks ago, by wenzelm
merged
3 weeks ago, by wenzelm
update NEWS;
3 weeks 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
3 weeks ago, by wenzelm
drop unused Task.info field;
3 weeks ago, by wenzelm
proper guard_time (amending 752806151432);
3 weeks ago, by wenzelm
proper dynamic access (amending c3f07c950116);
3 weeks ago, by wenzelm
more robust, notably for remote process (via SSH);
3 weeks ago, by wenzelm
prefer dynamic objects, following a5fda30edae2;
3 weeks ago, by wenzelm
proper dynamic access (amending 52b5c7c8e6d9);
3 weeks ago, by wenzelm
clarified signature: incorporate guard into Logger;
3 weeks ago, by wenzelm
merged
3 weeks ago, by desharna
added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp
3 weeks ago, by desharna
Moving valuable library material from Martingales into the distribution
3 weeks ago, by paulson
clarified signature;
3 weeks ago, by wenzelm
clarified module signature and state;
3 weeks ago, by wenzelm
tuned messages;
3 weeks ago, by wenzelm
omit somewhat pointless message, following b7187d4cdf68;
3 weeks ago, by wenzelm
more robust handling of uninitialized value, notably Build_Process.progress;
3 weeks ago, by wenzelm
tuned
3 weeks ago, by nipkow
partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded;
3 weeks ago, by Fabian Huch
clarified module signature and state;
3 weeks ago, by wenzelm
tuned signature: more protected operations;
3 weeks ago, by wenzelm
database performance tuning: just one synchronized_database for main loop body;
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b);
3 weeks ago, by wenzelm
more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
3 weeks ago, by wenzelm
tuned;
3 weeks ago, by wenzelm
tuned proof: avoid z3 to make it work on arm64-linux;
3 weeks ago, by wenzelm
official support for arm64-linux, despite a few missing tools;
3 weeks ago, by wenzelm
discontinue unstable z3-4.4.1 for arm64-linux from Debian (in contrast to 796ae338eb9d and 87718883c8b9);
3 weeks ago, by wenzelm
proper platform_name/platform_dir for native arm64-darwin: already published in 788f11af9822 after manual adjustment;
3 weeks ago, by wenzelm
update to scala-3.3.3;
3 weeks ago, by wenzelm
provide e-3.0.03 on all platforms, including arm64-linux and arm64-darwin --- still inactive;
3 weeks ago, by wenzelm
update NEWS, following 0d7c7fe65638;
3 weeks ago, by Fabian Huch
provide cvc5-1.1.1 for testing --- still inactive;
4 weeks ago, by wenzelm
rebuild bash_process executables on current reference platforms, including native arm64-darwin;
4 weeks ago, by wenzelm
tuned NEWS, see also c62003e05e46;
4 weeks ago, by wenzelm
update NEWS, following ea1913c953ef;
4 weeks ago, by wenzelm
tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:";
4 weeks ago, by wenzelm
more explicit NEWS (see 3648e9c88d0c);
4 weeks ago, by wenzelm
NEWS for a53287d9add3, 3e30ca77ccfe;
4 weeks ago, by wenzelm
add option for unify trace (now disabled by default as printing is excessive and rarely used);
4 weeks ago, by Fabian Huch
tuned unify trace option names;
4 weeks ago, by Fabian Huch
more scalable: avoid potentially expensive ordering of underlying key data type, e.g. in MESON.Cache of Naproche;
4 weeks ago, by wenzelm
updated to stack-2.15.1, lts-22.6, ghc-9.6.3;
4 weeks ago, by wenzelm
merged
4 weeks ago, by nipkow
tuned name
4 weeks ago, by nipkow
new simplifier trace_op for tracing simproc calls
4 weeks ago, by nipkow
merged
4 weeks 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
4 weeks ago, by paulson
support Zipperposition's skolemization in generated Isar proofs
4 weeks ago, by blanchet
improved output in simps_case_conv;
4 weeks ago, by Fabian Huch
improved output in inductive module;
4 weeks ago, by Fabian Huch
simplifier: no trace info from simprocs unless simp_debug = true.
4 weeks ago, by nipkow
deal with new-style Vampire skolemization in reconstructed Isar proofs
4 weeks ago, by blanchet
database performance tuning: prefer light-weight IPC over heavy-duty transactions;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
tuned signature: follow PostgreSQL syntax instead of JDBC API;
4 weeks ago, by wenzelm
more robust shutdown: interruptible database connection;
4 weeks ago, by wenzelm
clarified signature: more convenient send/receive operations;
4 weeks ago, by wenzelm
clarified versions for documentation;
4 weeks ago, by wenzelm
merged
4 weeks ago, by wenzelm
clarified signature: avoid hardwired values;
4 weeks ago, by wenzelm
clarified IPC via database server: receive notifications quasi-spontaneously via auxiliary thread;
4 weeks ago, by wenzelm
minor performance tuning: just 1 transaction for slices <= 1;
4 weeks ago, by wenzelm
tuned;
4 weeks ago, by wenzelm
tuned whitespace;
4 weeks ago, by wenzelm
tuned signature;
4 weeks ago, by wenzelm
clarified signature: fewer warnings in IntelliJ IDEA;
4 weeks ago, by wenzelm
removed unused database_server (amending 32ca3d1283de);
4 weeks ago, by wenzelm
timing function generation bug fix by Jonas Stahl
4 weeks ago, by nipkow
tuned signature: more types, fewer warnings in IntelliJ IDEA;
4 weeks ago, by wenzelm
new less ad hoc implementation of the 'moura' tactic for skolemization
4 weeks ago, by blanchet
more thorough Store.clean_output (amending 1fa1b32b0379);
5 weeks ago, by wenzelm
clarified signature: Build_Process tells how to clean sessions;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
minor performance tuning;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
tuned, following 7a1153c95bf9;
5 weeks ago, by wenzelm
merged
5 weeks ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
5 weeks ago, by wenzelm
proper usage;
5 weeks ago, by wenzelm
recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
more robust: make double-sure that heap digest is present;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
minor performance tuning: just one transaction for log_db without heap;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
proper store.cache.compress;
5 weeks ago, by wenzelm
tuned whitespace;
5 weeks ago, by wenzelm
clarified store_session: heap requires process_result.ok, but log_db is always stored;
5 weeks ago, by wenzelm
unused;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned names;
5 weeks ago, by wenzelm
tuned names;
5 weeks ago, by wenzelm
clarified database layout;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
more accurate types;
5 weeks ago, by wenzelm
build local log_db, with store/restore via optional database server;
5 weeks ago, by wenzelm
propagate property "isabelle.debug", notably for Java/Scala exception trace;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0);
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified names;
5 weeks ago, by wenzelm
more explicit build_cluster flag to guard open_build_database server;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
simplified specification of type class semiring_bits
5 weeks ago, by haftmann
New material about transcendental functions, polynomials, et cetera, thanks to Manuel Eberl
5 weeks ago, by paulson
merged
5 weeks ago, by paulson
A small collection of new and useful facts, including the AM-GM inequality
5 weeks ago, by paulson
remove selected occurrences of 'moura' tactic
5 weeks ago, by blanchet
added lemmas relpowp_left_unique and relpow_left_unique
5 weeks ago, by desharna
added lemmas relpowp_right_unique and relpow_right_unique
5 weeks ago, by desharna
use define_time_fun
5 weeks ago, by nipkow
time funs: +1 instead of 1+
5 weeks ago, by nipkow
minor performance tuning;
5 weeks ago, by wenzelm
clarified signature: more comprehensive operations;
5 weeks ago, by wenzelm
clarified signature: more explicit types;
5 weeks ago, by wenzelm
clarified signature: emphasize physical db files;
5 weeks ago, by wenzelm
tuned: afford untyped/unscoped update;
5 weeks ago, by wenzelm
clarified signature: avoid ill-defined type java.net.URL;
5 weeks ago, by wenzelm
unused;
5 weeks ago, by wenzelm
tuned: afford untyped/unscoped update;
5 weeks ago, by wenzelm
more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML;
5 weeks ago, by wenzelm
clarified signature: more explicit types/scopes;
5 weeks ago, by wenzelm
tuned names;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
tuned documentation;
5 weeks ago, by wenzelm
more robust: disallow empty clusters, so "isabelle build -H" really means cluster build;
5 weeks ago, by wenzelm
clarified modules: centralize default policy;
5 weeks ago, by wenzelm
more explicit types --- fewer warnings in IntelliJ IDEA;
5 weeks ago, by wenzelm
tuned: avoid shadowing of names;
5 weeks ago, by wenzelm
clarified default "isabelle build -j0 -H";
5 weeks ago, by wenzelm
tuned whitespace;
5 weeks ago, by wenzelm
clarifier worker vs. master, which may coincide for local build;
5 weeks ago, by wenzelm
clarified signature: more standard defaults;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
prefer static object, while class is required for "services";
5 weeks ago, by wenzelm
clarified signature: prefer default;
5 weeks ago, by wenzelm
merged
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
more robust: check subclasses as well;
5 weeks ago, by wenzelm
more robust;
5 weeks ago, by wenzelm
support for alternative user home, e.g. to avoid slow NFS shares;
5 weeks ago, by wenzelm
support explicit USER_HOME within SSH session;
5 weeks ago, by wenzelm
tuned;
5 weeks ago, by wenzelm
merged
5 weeks ago, by paulson
Further adjustments to the syntax for Lebesgue integration
5 weeks ago, by paulson
tuned comments;
5 weeks ago, by wenzelm
more robust: always close, despite failure;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
tuned signature;
5 weeks ago, by wenzelm
tuned comments;
5 weeks ago, by wenzelm
clarified signature;
5 weeks ago, by wenzelm
Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury
5 weeks ago, by blanchet
tuned whitespace;
6 weeks ago, by wenzelm
prefer static object, while class is required for "services" (see 47eb96592aa2);
6 weeks ago, by wenzelm
clarified directories;
6 weeks ago, by wenzelm
tuned signature;
6 weeks ago, by wenzelm
tuned: prefer explicit update operation for immutable options;
6 weeks ago, by wenzelm
tuned message;
6 weeks ago, by wenzelm
more robust type, with explicit default;
6 weeks ago, by wenzelm
tuned usage message;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
more robust defaults;
6 weeks ago, by wenzelm
merged
6 weeks ago, by desharna
added lemmas relpow_trans[trans] and relpowp_trans[trans]
6 weeks ago, by desharna
more on disjunctive addition/subtraction
6 weeks ago, by haftmann
merged
6 weeks ago, by wenzelm
prefer physical processors (see also 4b014e6c1dfe and 26a43785590b);
6 weeks ago, by wenzelm
more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
6 weeks ago, by wenzelm
more robust default;
6 weeks ago, by wenzelm
more accurate, notably on lxbroy10 and vmnipkow9;
6 weeks ago, by wenzelm
clarified num_processors: follow Poly/ML (with its inaccuracies);
6 weeks ago, by wenzelm
clarified modules, following Isabelle/ML;
6 weeks ago, by wenzelm
clarified signature;
6 weeks ago, by wenzelm
tuned comments;
6 weeks ago, by wenzelm
merged
6 weeks ago, by paulson
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
6 weeks ago, by paulson
merged
6 weeks ago, by paulson
A few lemmas brought in from AFP entries
6 weeks ago, by paulson
merged
6 weeks ago, by traytel
made destructor-view tactic more robust (by Jan van Brügge)
6 weeks ago, by traytel
performance optimization;
6 weeks ago, by Fabian Huch
clarified names;
6 weeks ago, by Fabian Huch
clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4);
6 weeks ago, by Fabian Huch
proper "linux_arm", amending 76ad72736e9e;
6 weeks ago, by wenzelm
more lemmas
6 weeks ago, by haftmann
new lemmas involving Ramsey numbers, infinite sets
6 weeks ago, by paulson
simplified class specification
6 weeks ago, by haftmann
Removal of duplicate code
7 weeks ago, by paulson
Two new theorems
7 weeks ago, by paulson
more lemmas and more correct lemma names
7 weeks ago, by haftmann
NEWS: corrected the definition of convexity of functions
7 weeks ago, by paulson
Further lemmas concerning complexity and measures
7 weeks ago, by paulson
Correct the definition of a convex function, and updated the proofs
7 weeks ago, by paulson
merged;
7 weeks ago, by wenzelm
update to windows_app-20240205, with executables for linux, linux_arm, macos;
7 weeks ago, by wenzelm
omit redundant options;
7 weeks ago, by wenzelm
tuned README;
7 weeks ago, by wenzelm
uniform build of binutils for linux, linux_arm, macos;
7 weeks ago, by wenzelm
fix reconstruction of Alethe's and_pos rule
2 months ago, by Mathias Fleury
added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult
7 weeks ago, by desharna
proper target option, following package binutils-mingw-w64-x86-64 from Debian/Ubuntu;
7 weeks ago, by wenzelm
updated windows_app based on launch4j-3.50-linux-x64, without rebuilding GNU binutils (missing COFF target pe-i386);
7 weeks ago, by wenzelm
proper sfx_archive_name;
7 weeks ago, by wenzelm
clarified options;
7 weeks ago, by wenzelm
more robust;
7 weeks ago, by wenzelm
build Isabelle windows_app component from GNU binutils and launch4j;
7 weeks ago, by wenzelm
proper windows_app/launch4j-linux_arm;
7 weeks ago, by wenzelm
merged
7 weeks ago, by paulson
A small number of new lemmas
7 weeks ago, by paulson
explicit reference to code_dt
8 weeks ago, by haftmann
made lift_bnf more robust for abstract types with 'phantom' type variables
8 weeks ago, by traytel
rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO";
8 weeks ago, by wenzelm
proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);
8 weeks ago, by wenzelm
proper bash syntax (amending 0631dfc0db07);
8 weeks ago, by wenzelm
tuned proof: avoid z3;
8 weeks ago, by wenzelm
tuned proof: avoid z3 to make it work on arm64-linux;
8 weeks ago, by wenzelm
tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;
8 weeks ago, by wenzelm
merged
8 weeks ago, by wenzelm
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
8 weeks ago, by wenzelm
strengthened class parity
8 weeks ago, by haftmann
proper accessible paths for web server;
8 weeks ago, by wenzelm
more informative message (amending b8a6b2ec85a2);
8 weeks ago, by wenzelm
merged
8 weeks ago, by wenzelm
more robust: do not affect "$ISABELLE_HOME_USER/contrib" on master node;
8 weeks ago, by wenzelm
avoid excessive ML heap on this 16GB node;
8 weeks ago, by wenzelm
more robust (amending c9774306a879);
8 weeks ago, by wenzelm
proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;
8 weeks ago, by wenzelm
clarified symbolic host name;
8 weeks ago, by wenzelm
allow remote_build on this host (server-arm), without conflicts of this "isabelle_self";
8 weeks ago, by wenzelm
more robust message;
8 weeks ago, by wenzelm
A few more new theorems taken from AFP entries
8 weeks ago, by paulson
merged
8 weeks ago, by nipkow
define_time_function: avoid unused let's
8 weeks ago, by nipkow
common type class for trivial properties on div/mod
8 weeks ago, by haftmann
more robust (amending 1600fb749c54), to support the following corner case:
8 weeks ago, by wenzelm
proper test options;
2 months ago, by wenzelm
proper history_base for linux_arm;
2 months ago, by wenzelm
updated to PostgreSQL 12 on Ubuntu 20.04;
2 months ago, by wenzelm
routine build + test for linux_arm;
2 months ago, by wenzelm
disable test on "augsburg1": machine will be dismantled;
2 months ago, by wenzelm
add approximation factors in build schedule to estimate build times more conservatively;
2 months ago, by Fabian Huch
merged
2 months ago, by paulson
Type class patch suggested by Achim Brucker, plus tidied lemma
2 months ago, by paulson
rearranged and reformulated abstract classes for bit structures and operations
2 months ago, by haftmann
Three new lemmas
2 months ago, by paulson
tuned proof: avoid z3 to make it work on arm64-linux;
2 months ago, by wenzelm
update to jdk-21.0.2;
2 months ago, by wenzelm
make build process state protected to avoid copying in subclasses (e.g. for database connections);
2 months ago, by Fabian Huch
add build_sync tag to sync certain options (e.g., build_engine) across build processes;
2 months ago, by Fabian Huch
clarified Mercurial version: presumably the last version that supports both python2 and python3;
2 months ago, by wenzelm
more robust: avoid crash on non-Linux systems;
2 months ago, by wenzelm
clarified webserver names;
2 months ago, by wenzelm
proper Apache.php_name;
2 months ago, by wenzelm
proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);
2 months ago, by wenzelm
tuned source structure;
2 months ago, by wenzelm
more robust systemd configuration;
2 months ago, by wenzelm
more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";
2 months ago, by wenzelm
tuned whitespace in generated file;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL);
2 months ago, by wenzelm
proper php-fpm configuration for nginx;
2 months ago, by wenzelm
support multiple webservers: Apache or Nginx;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
2 months ago, by wenzelm
unused;
2 months ago, by wenzelm
enforce rebuild of Isabelle/Scala + Isabelle/ML;
2 months ago, by wenzelm
updated to postgresql-42.7.1;
2 months ago, by wenzelm
updated to sqlite-jdbc-3.45.0.0, including slf4j-1.7.36;
2 months ago, by wenzelm
update to llncs-2.23;
2 months ago, by wenzelm
clarified bootstrap;
2 months ago, by wenzelm
clarified directories;
2 months ago, by wenzelm
clarified directories;
2 months ago, by wenzelm
obsolete (see also fc88b943e1b2);
2 months ago, by wenzelm
proper output, following 2cd23d587db9;
2 months ago, by wenzelm
always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c);
2 months ago, by wenzelm
clarified directories;
2 months ago, by wenzelm
more accurate Isabelle versions;
2 months ago, by wenzelm
more accurate Ubuntu versions;
2 months ago, by wenzelm
more uses of define_time_fun
2 months ago, by nipkow
translation to time functions now with canonical let.
2 months ago, by nipkow
merged
2 months ago, by paulson
A few new results (mostly brought in from other developments)
2 months ago, by paulson
merged
2 months ago, by nipkow
Added time function automation
2 months ago, by nipkow
streamlined type class specification
2 months ago, by haftmann
consolidated lemma name
2 months ago, by haftmann
support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
update links;
2 months ago, by wenzelm
follow post-maintenance updates of original Phabricator, as base-line for Phorge;
2 months ago, by wenzelm
refer to "localhost" as pro-forma domain;
2 months ago, by wenzelm
simplified specification of type class
2 months ago, by haftmann
consolidated name of lemma analogously to nat/int/word_bit_induct
2 months ago, by haftmann
more accurate syntax: 'obtain' vars are optional;
2 months ago, by wenzelm
clarified order, disregard structure of proof;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
more thorough treatment of hidden type variables within zproof;
2 months ago, by wenzelm
more uniform treatment of "hyps" within zproof;
2 months ago, by wenzelm
clarified order: follow Thm.fold_terms;
2 months ago, by wenzelm
merged
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified test: no exception yet;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned signature: more direct operations;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature: more direct operations;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
more robust: certify types uniformly (see also 62b75508eb66);
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
clarified signature: avoid redundant Term.maxidx_of_term;
2 months ago, by wenzelm
proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);
2 months ago, by wenzelm
misc tuning and clarification: prefer Same.operation;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned names;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
added and removed lemmas
2 months ago, by nipkow
proper SMTP session: set envelope sender address correctly;
2 months ago, by Fabian Huch
update javamail component with current jakarta mail APIs and eclipse angus implementation;
2 months ago, by Fabian Huch
tuned source structure;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT;
2 months ago, by wenzelm
omit syntactic of_class check, which is in conflict with sort constraints within the logic;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
minor performance tuning;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
misc tuning and clarification;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned signature: canonical argument order;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified datatype ztyp: omit special case that rarely occurs (thanks to ZClass and ZClassp);
2 months ago, by wenzelm
clarified box_proof: use sort constraints within the logic;
2 months ago, by wenzelm
more operations (see also 8368160d3c65);
2 months ago, by wenzelm
proper support for complex types, not just type variables (amending 623789141e39);
2 months ago, by wenzelm
proper instantiation for make_const_proof, notably change of types for term variables;
2 months ago, by wenzelm
tuned names;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
minor performance tuning: proper Same.operation;
2 months ago, by wenzelm
minor performance tuning: proper Same.operation;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
minor performance tuning: proper Same.operation;
2 months ago, by wenzelm
minor performance tuning: proper Same.operation;
2 months ago, by wenzelm
tuned signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
pro-forma support for ZTerm.sorts_zproof;
2 months ago, by wenzelm
tuned comments;
2 months ago, by wenzelm
tuned structure;
2 months ago, by wenzelm
minor performance tuning: proper Same.operation;
2 months ago, by wenzelm
tuned names (again);
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
clarified signature: more operations;
2 months ago, by wenzelm
tuned names;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned whitespace;
2 months ago, by wenzelm
clarified signature;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature: prefer Same.operation;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
more zproofs;
2 months ago, by wenzelm
more operations;
2 months ago, by wenzelm
clarified modules;
2 months ago, by wenzelm
minor performance tuning, following 703201dbd413;
2 months ago, by wenzelm
tuned;
2 months ago, by wenzelm
clarified signature: suppress unused fields;
3 months ago, by wenzelm
eliminate clone (amending e7796c55d840);
3 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned: avoid duplicates;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
proper Thm.transfer;
3 months ago, by wenzelm
proper Thm.trim_context;
3 months ago, by wenzelm
clarified stored data: actual thm allows to replay zproofs in a modular manner;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned signature, following Proofterm.thm_header;
3 months ago, by wenzelm
more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
proper Thm_Name.make_list for thm_definition;
3 months ago, by wenzelm
more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923);
3 months ago, by wenzelm
more robust: zproofs need to be enabled (amending 43d8385db923);
3 months ago, by wenzelm
more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
clarified signature: support update of local_theory;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
unused;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);
3 months ago, by wenzelm
minor performance tuning: shorter names;
3 months ago, by wenzelm
minor performance tuning: static vs. dynamic rules;
3 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
observe option "prune_proofs";
3 months ago, by wenzelm
clarified zproof storage: per-theory table in anticipation of session exports;
3 months ago, by wenzelm
proper thm_name for stored zproof;
3 months ago, by wenzelm
uniform treatment of lazy facts: actual proof terms are always strict;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
proper Thm.transfer;
3 months ago, by wenzelm
clarified context: avoid capture of thy2 within closure;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
more informative exceptions;
3 months ago, by wenzelm
more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy");
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more informative exception;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified ML toplevel output: avoid "??." prefix;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
omit pointless future: proof terms are built sequentially;
3 months ago, by wenzelm
omit unclear / inaccurate renaming;
3 months ago, by wenzelm
more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;
3 months ago, by wenzelm
more robust: avoid assumption about Context.certificate_theory;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more normalization;
3 months ago, by wenzelm
less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more thorough beta contraction, following Envir.norm_term;
3 months ago, by wenzelm
tuned, following Envir.norm_term;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
merged
3 months ago, by nipkow
unused lemma
3 months ago, by nipkow
restore benchmark requirement heaps properly;
3 months ago, by Fabian Huch
continue build while waiting for updated schedule;
3 months ago, by Fabian Huch
clarified signature;
3 months ago, by Fabian Huch
added start-up sequence for benchmark with requirements;
3 months ago, by Fabian Huch
use single-threaded session build as benchmark (using ZF-Constructible);
3 months ago, by Fabian Huch
separate build processes for scheduler and scheduled;
3 months ago, by Fabian Huch
add delay and limit options for when schedule is considered outdated;
3 months ago, by Fabian Huch
proper closing order;
3 months ago, by Fabian Huch
read serial for schedules (amending 2039f360);
3 months ago, by Fabian Huch
more thorough beta contraction;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more operations, following proofterm.ML;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature, following Term.subst_bounds_same;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
minor performance tuning: more concise union;
3 months ago, by wenzelm
tuned comments;
3 months ago, by wenzelm
tuned, following close_proof;
3 months ago, by wenzelm
proper treatment of proof hyps, following 8368160d3c65;
3 months ago, by wenzelm
proper treatment of proof hyps: unchangeable, like bound;
3 months ago, by wenzelm
proper Thm.transfer (required for zproofs);
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
proper beta_norm after instantiation (amending 90c5aadcc4b2);
3 months ago, by wenzelm
minor performance tuning: more direct beta_norm;
3 months ago, by wenzelm
more robust norm_proof: turn env into instantiation, based on visible statement;
3 months ago, by wenzelm
proper scope of cache (amending 61af3e917597);
3 months ago, by wenzelm
tuned comments;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
more operations: zterm ordering that follows fast_term_ord;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
more zproofs, imitating existing proofs (which are a bit rough here);
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
minor performance tuning: prefer Same.operation;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];
3 months ago, by wenzelm
misc tuning and clarification;
3 months ago, by wenzelm
minor performance tuning: prefer Symset.T;
3 months ago, by wenzelm
minor performace tuning;
3 months ago, by wenzelm
minor performance tuning: prefer Same.operation;
3 months ago, by wenzelm
tuned: more standard accumulation;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
proper ZTerm.lift_proof (amending 4a1a25bdf81d);
3 months ago, by wenzelm
filter predecessors properly (amending ee405c40db72);
3 months ago, by Fabian Huch
improve graphical clarity by omitting intra-host dependencies (following ee405c40db72);
3 months ago, by Fabian Huch
more zproofs;
3 months ago, by wenzelm
minor performance tuning: more direct abstraction level;
3 months ago, by wenzelm
more general Logic.incr_indexes_operation;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
clarified ML;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more robust: proper Proofterm.get_proofs_level with bound check;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature: fewer tuples;
3 months ago, by wenzelm
clarified signature: fewer tuples;
3 months ago, by wenzelm
clarified signature: more explicit get_proofs_level with bounds check;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
misc tuning and clarification: more standard Same.commit discipline;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
minor performance tuning: more careful treatment of empty environment;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
clarified signature: support shared cache;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned: avoid shadowing;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
tuned -- eliminate clones;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
consider schedule calculation time in estimation;
3 months ago, by Fabian Huch
compare previous build schedule with new one, to prevent regressions;
3 months ago, by Fabian Huch
clarified: build schedules may be outdated when empty, after some time, or due to build progress;
3 months ago, by Fabian Huch
store previous build jobs in graph so schedules can be used later in the build process;
3 months ago, by Fabian Huch
add serial for build schedule to avoid unnecessary db read/writes;
3 months ago, by Fabian Huch
tuned;
3 months ago, by Fabian Huch
clarified;
3 months ago, by Fabian Huch
tuned;
3 months ago, by Fabian Huch
use build database to synchronize build schedule computed on master node (e.g., such that view on cluster is consistent);
3 months ago, by Fabian Huch
add build uuid to schedule;
3 months ago, by Fabian Huch
tuned;
3 months ago, by Fabian Huch
use schedule directly instead of extra cache;
3 months ago, by Fabian Huch
added build schedule command-line wrapper;
3 months ago, by Fabian Huch
added graphical representation of build schedules;
3 months ago, by Fabian Huch
clarified build heuristics parameters;
3 months ago, by Fabian Huch
proper parallel paths: factor in elapsed time;
3 months ago, by Fabian Huch
performance tuning: cache estimates;
3 months ago, by Fabian Huch
misc tuning and clarification;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
minor performance tuning: regular Same.operation;
3 months ago, by wenzelm
clarified signature: more standard argument order;
3 months ago, by wenzelm
clarified signature: more standard argument order;
3 months ago, by wenzelm
tuned whitespace;
3 months ago, by wenzelm
tuned: more standard names;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
tuned: prefer Same.commit;
3 months ago, by wenzelm
tuned: more standard argument order;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
tuned comments;
3 months ago, by wenzelm
tuned structure;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
performance tuning: cache for ztyp_of within zterm_of;
3 months ago, by wenzelm
tuned names;
3 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
minor performance tuning;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
proper treatment of ZConstP: term represents body of closure;
3 months ago, by wenzelm
proper substitution of types within term;
3 months ago, by wenzelm
more accurate treatment of term variables after instantiation of type variables;
3 months ago, by wenzelm
tuned signature;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
check that Isar proofs contain one 'show'
3 months ago, by blanchet
include unnamed chained facts in Sledgehammer's relevance filter
3 months ago, by blanchet
merge
3 months ago, by blanchet
removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics
3 months ago, by blanchet
don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts
3 months ago, by blanchet
tuned T functions: now 0 if not recursive
3 months ago, by nipkow
minor performance tuning;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
misc tuning and clarification;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
clarified signature;
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
more ML pretty-printing;
3 months ago, by wenzelm
clarified const_proof vs. zproof_name;
3 months ago, by wenzelm
merged
3 months ago, by wenzelm
more zproofs;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
tuned;
3 months ago, by wenzelm
more operations;
3 months ago, by wenzelm
clarified modules;
3 months ago, by wenzelm
more zterm operations;
3 months ago, by wenzelm
compactified specification of type class parity
3 months ago, by haftmann
generalized
3 months ago, by haftmann
explicit annotation of lemma duplicates
3 months ago, by haftmann
merged
3 months ago, by wenzelm
clarified proof_body: cover zboxes from zproof;
3 months ago, by wenzelm
pro-forma support for optional zproof: no proper content yet;
3 months ago, by wenzelm
clarified signature: follow Term.could_unify;
3 months ago, by wenzelm
clarified bootstrap --- modules related to proofterm.ML;
3 months ago, by wenzelm
clarified path time heuristic: configurable parameters for larger search space;
3 months ago, by Fabian Huch
clarified heuristics toString;
3 months ago, by Fabian Huch
tuned;
3 months ago, by Fabian Huch
add heuristic for non-scheduled (standard) build behaviour;
3 months ago, by Fabian Huch
proper unused nodes;
3 months ago, by Fabian Huch
clarified schedule message;
3 months ago, by Fabian Huch
proper parallel paths;
3 months ago, by Fabian Huch
clarified build schedule host: more operations;
3 months ago, by Fabian Huch
clarified path heuristic;
3 months ago, by Fabian Huch
clarified graph operations in timing heuristic;
3 months ago, by Fabian Huch
merged
3 months ago, by nipkow
added and removed [simp]s
3 months ago, by nipkow
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
tip