Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+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.
option for benchmark session;
18 months ago, by Fabian Huch
add hosts option to run benchmark on the cluster from the command-line;
18 months ago, by Fabian Huch
only start jobs early if they are due (cf. 1966578feff8);
18 months ago, by Fabian Huch
New material from a variety of sources (including AFP)
18 months ago, by paulson
build component for cvc5-latest (ef2bc3f735df);
18 months ago, by wenzelm
merged
18 months ago, by desharna
try proof method "order" in Sledgehammer's proof reconstruction
18 months ago, by desharna
added Mirabelle action "order"
18 months ago, by desharna
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
18 months ago, by desharna
tuned proof
18 months ago, by desharna
added lemma order_reflclp_if_transp_and_asymp
18 months ago, by desharna
added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on
18 months ago, by desharna
HOL-Library: added modulo/congruence for real numbers
18 months ago, by Manuel Eberl
only print schedule if relevant;
18 months ago, by Fabian Huch
remove laziness: no need, and errors during initialization loop with close();
18 months ago, by Fabian Huch
more general definition of meromorphicity; Weierstraß factorisation theorem
18 months ago, by Manuel Eberl
always provide build_database_server option in benchmark command;
18 months ago, by Fabian Huch
always check if node is defined, e.g. for exists_next operation wit empty schedule;
18 months ago, by Fabian Huch
fixed typo
18 months ago, by blanchet
disable taskset for now: performance impact is negative;
18 months ago, by Fabian Huch
allow specifying initial schedule;
18 months ago, by Fabian Huch
clarify use of num_threads vs. max_cpus;
18 months ago, by Fabian Huch
clarified host: pre-load max threads;
18 months ago, by Fabian Huch
clarified: more operations;
18 months ago, by Fabian Huch
added alias wfp for wfP
18 months ago, by desharna
merged
18 months 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
18 months ago, by desharna
start scheduled jobs earlier, if possible;
18 months ago, by Fabian Huch
tuned proofs
18 months 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
18 months ago, by desharna
merged
18 months ago, by desharna
added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively
18 months ago, by desharna
read/write proper schedule date (amending 9da3019e1ee5);
18 months ago, by Fabian Huch
allow read/write of schedule in build (read via option, write from tool);
18 months ago, by Fabian Huch
file representation for schedule (e.g., for generating from external tool);
18 months ago, by Fabian Huch
proper median/mean time;
18 months ago, by Fabian Huch
remove schedule outdated limit: delay is sufficient;
18 months ago, by Fabian Huch
tuned whitespace;
18 months 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);
18 months ago, by Fabian Huch
tuned;
18 months ago, by Fabian Huch
remove old build before generating schedule;
18 months ago, by Fabian Huch
unused;
18 months ago, by Fabian Huch
merged
18 months 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
18 months ago, by desharna
clarified names;
18 months ago, by wenzelm
sketch & explore: TODO comments are addressed in parent commits
18 months ago, by Simon Wimmer
sketch & explore: reduce unnecessary type constraints
18 months ago, by Simon Wimmer
sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`)
18 months ago, by Simon Wimmer
sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text
18 months ago, by Simon Wimmer
change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible);
18 months ago, by Fabian Huch
unused;
18 months ago, by Fabian Huch
tuned;
18 months ago, by Fabian Huch
proper IPC for scheduled builds, following 7ae25372ab04;
18 months ago, by Fabian Huch
proper check (amending 9aef1d1535ff);
18 months ago, by Fabian Huch
more synced options (following 6e5397fcc41b);
18 months ago, by Fabian Huch
avoid [no_atp] declations shadowing propositions from sledgehammer
18 months ago, by haftmann
track start in build job results (following 9d484c5d3a63), so it can directly be written to build log database;
18 months ago, by Fabian Huch
use inherited build_start, following d9fc2cc37694;
18 months ago, by Fabian Huch
update NEWS + CONTRIBUTORS for release;
18 months ago, by wenzelm
Tuned proofs
18 months ago, by haftmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
tip