Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
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 comments;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more operations: zterm ordering that follows fast_term_ord;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more zproofs, imitating existing proofs (which are a bit rough here);
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
minor performance tuning: prefer Same.operation;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
minor performance tuning: prefer Symset.T;
13 months ago, by wenzelm
minor performace tuning;
13 months ago, by wenzelm
minor performance tuning: prefer Same.operation;
13 months ago, by wenzelm
tuned: more standard accumulation;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
proper ZTerm.lift_proof (amending 4a1a25bdf81d);
13 months ago, by wenzelm
filter predecessors properly (amending ee405c40db72);
13 months ago, by Fabian Huch
improve graphical clarity by omitting intra-host dependencies (following ee405c40db72);
13 months ago, by Fabian Huch
more zproofs;
13 months ago, by wenzelm
minor performance tuning: more direct abstraction level;
13 months ago, by wenzelm
more general Logic.incr_indexes_operation;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified ML;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more robust: proper Proofterm.get_proofs_level with bound check;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature: fewer tuples;
13 months ago, by wenzelm
clarified signature: fewer tuples;
13 months ago, by wenzelm
clarified signature: more explicit get_proofs_level with bounds check;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
misc tuning and clarification: more standard Same.commit discipline;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
minor performance tuning: more careful treatment of empty environment;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
clarified signature: support shared cache;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned: avoid shadowing;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
tuned -- eliminate clones;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
consider schedule calculation time in estimation;
13 months ago, by Fabian Huch
compare previous build schedule with new one, to prevent regressions;
13 months ago, by Fabian Huch
clarified: build schedules may be outdated when empty, after some time, or due to build progress;
13 months ago, by Fabian Huch
store previous build jobs in graph so schedules can be used later in the build process;
13 months ago, by Fabian Huch
add serial for build schedule to avoid unnecessary db read/writes;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
clarified;
13 months ago, by Fabian Huch
tuned;
13 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);
13 months ago, by Fabian Huch
add build uuid to schedule;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
use schedule directly instead of extra cache;
13 months ago, by Fabian Huch
added build schedule command-line wrapper;
13 months ago, by Fabian Huch
added graphical representation of build schedules;
13 months ago, by Fabian Huch
clarified build heuristics parameters;
13 months ago, by Fabian Huch
proper parallel paths: factor in elapsed time;
13 months ago, by Fabian Huch
performance tuning: cache estimates;
13 months ago, by Fabian Huch
misc tuning and clarification;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
minor performance tuning: regular Same.operation;
13 months ago, by wenzelm
clarified signature: more standard argument order;
13 months ago, by wenzelm
clarified signature: more standard argument order;
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
tuned: more standard names;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
tuned: prefer Same.commit;
13 months ago, by wenzelm
tuned: more standard argument order;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned comments;
13 months ago, by wenzelm
tuned structure;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
performance tuning: cache for ztyp_of within zterm_of;
13 months ago, by wenzelm
tuned names;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
minor performance tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
proper treatment of ZConstP: term represents body of closure;
13 months ago, by wenzelm
proper substitution of types within term;
13 months ago, by wenzelm
more accurate treatment of term variables after instantiation of type variables;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
check that Isar proofs contain one 'show'
13 months ago, by blanchet
include unnamed chained facts in Sledgehammer's relevance filter
13 months ago, by blanchet
merge
13 months ago, by blanchet
removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics
13 months ago, by blanchet
don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts
13 months ago, by blanchet
tuned T functions: now 0 if not recursive
13 months ago, by nipkow
minor performance tuning;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
more ML pretty-printing;
13 months ago, by wenzelm
clarified const_proof vs. zproof_name;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
more zproofs;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more operations;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
more zterm operations;
13 months ago, by wenzelm
compactified specification of type class parity
13 months ago, by haftmann
generalized
13 months ago, by haftmann
explicit annotation of lemma duplicates
13 months ago, by haftmann
merged
13 months ago, by wenzelm
clarified proof_body: cover zboxes from zproof;
13 months ago, by wenzelm
pro-forma support for optional zproof: no proper content yet;
13 months ago, by wenzelm
clarified signature: follow Term.could_unify;
13 months ago, by wenzelm
clarified bootstrap --- modules related to proofterm.ML;
13 months ago, by wenzelm
clarified path time heuristic: configurable parameters for larger search space;
13 months ago, by Fabian Huch
clarified heuristics toString;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
add heuristic for non-scheduled (standard) build behaviour;
13 months ago, by Fabian Huch
proper unused nodes;
13 months ago, by Fabian Huch
clarified schedule message;
13 months ago, by Fabian Huch
proper parallel paths;
13 months ago, by Fabian Huch
clarified build schedule host: more operations;
13 months ago, by Fabian Huch
clarified path heuristic;
13 months ago, by Fabian Huch
clarified graph operations in timing heuristic;
13 months ago, by Fabian Huch
merged
13 months ago, by nipkow
added and removed [simp]s
13 months ago, by nipkow
tight representation of types / terms / proof terms (presently unused);
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
reduce redundancy: avoid huge lists;
13 months ago, by wenzelm
more detailed profiling including "names";
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
slightly more compact heap: better sharing of persistent tuples;
13 months ago, by wenzelm
added method to generate build schedules directly;
13 months ago, by Fabian Huch
clarified load vs. apply vs. make;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
tuned heuristic;
13 months ago, by Fabian Huch
use cpu time for approximation;
13 months ago, by Fabian Huch
lower bound for approximated times;
13 months ago, by Fabian Huch
use full timing information in build schedule;
13 months ago, by Fabian Huch
consistent hosts ordering;
13 months ago, by Fabian Huch
filter hosts properly;
13 months ago, by Fabian Huch
merged
13 months ago, by wenzelm
more compact representation of theory_id -- via consecutive thread-local ids;
13 months ago, by wenzelm
misc tuning and clarification;
13 months ago, by wenzelm
more compact representation;
13 months ago, by wenzelm
more compact representation;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
more compact representation of theory_id;
13 months ago, by wenzelm
tuned signature;
13 months ago, by wenzelm
compact representation of sets of integers;
13 months ago, by wenzelm
generated build schedule explicitly (e.g., for further analysis);
13 months ago, by Fabian Huch
de-duplicated specification of class ring_bit_operations
13 months ago, by haftmann
generalized
13 months ago, by haftmann
restructured
13 months ago, by haftmann
grouped lemmas for symbolic computations
13 months ago, by haftmann
sorted out lemma duplicates
13 months ago, by haftmann
more reactive headless server, in contrast to 15656ad28691 (when "isabelle dump" was important to export AFP content);
13 months ago, by wenzelm
tuned whitespace;
13 months ago, by wenzelm
clarified signature;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified modules;
13 months ago, by wenzelm
clarified modules: Build_Log.private_data provides raw data access without transaction_lock;
13 months ago, by wenzelm
more thorough transaction_lock;
13 months ago, by wenzelm
obsolete, see also a5896fe040dd;
13 months ago, by wenzelm
removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);
13 months ago, by wenzelm
provide src/Tools/Demo as example for system component with Isabelle/Scala tool;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);
13 months ago, by wenzelm
clarified buffer_size;
13 months ago, by wenzelm
merged
13 months ago, by wenzelm
disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL-Analysis" on arm64_32-darwin (studio1);
13 months ago, by wenzelm
workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read-only text;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
prefer Unix-domain socket on Unix;
13 months ago, by wenzelm
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
clarified signature: more general make_streams;
13 months ago, by wenzelm
tuned;
13 months ago, by wenzelm
more robust exception handling (amending 8cc1ae43e12e);
13 months ago, by wenzelm
clarified signature: avoid deprecated URL constructors;
13 months ago, by wenzelm
avoid deprecated URL constructors;
13 months ago, by wenzelm
proper split;
13 months ago, by Fabian Huch
properly sort entries;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
better estimation for unknown jobs;
13 months ago, by Fabian Huch
clarified and tuned timing estimation;
13 months ago, by Fabian Huch
split actual approximation from data handling;
13 months ago, by Fabian Huch
clarified timing data vs. timing entries: full top-level data view vs. dynamic partial data;
13 months ago, by Fabian Huch
proper filter for approximations;
13 months ago, by Fabian Huch
proper inflection point check;
13 months ago, by Fabian Huch
tuned;
13 months ago, by Fabian Huch
slightly more elementary characterization of unset_bit
13 months ago, by haftmann
more direct characterization of binary bit operations
13 months ago, by haftmann
tuned;
13 months ago, by Fabian Huch
clarified timing data operations: proper estimation (instead of known points);
13 months ago, by Fabian Huch
use proper max threads (limited by available hardware) in heuristics;
13 months ago, by Fabian Huch
clarified time estimation: does not use config;
13 months ago, by Fabian Huch
handle inflection point in interpolation with monotone prefix;
13 months ago, by Fabian Huch
proper computation of sorted prefix;
13 months ago, by Fabian Huch
better build time interpolation: model with Amdahl's law where applicable;
13 months ago, by Fabian Huch
proper piecewise linear build time interpolation;
13 months ago, by Fabian Huch
properly incorporate running tasks into timing heuristic;
13 months ago, by Fabian Huch
clarified ready vs. next ready;
13 months ago, by Fabian Huch
introduced path heuristic abstraction;
13 months ago, by Fabian Huch
base abstract specification of NOT on recursive equation rather than bit projection
13 months ago, by haftmann
modernized, reordered, generalized
13 months ago, by haftmann
more correct type annotation
13 months ago, by haftmann
proper build with jdk-21 (amending 4fb5e6499da9);
13 months ago, by wenzelm
NEWS;
14 months ago, by wenzelm
update to jdk-21.0.1;
14 months ago, by wenzelm
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
14 months ago, by wenzelm
clarified modules;
14 months ago, by wenzelm
suppress duplicate entries systematically using log_name: e.g. relevant for AFP;
14 months ago, by wenzelm
clarified operation: pick current pull_date instead of previous one;
14 months ago, by wenzelm
operations AND, OR, XOR are specified by characteristic recursive equation
14 months ago, by haftmann
clarified toml keys operations;
14 months ago, by Fabian Huch
tuned;
14 months ago, by Fabian Huch
clarified toml keys: more operations;
14 months ago, by Fabian Huch
use toml key operations properly;
14 months ago, by Fabian Huch
clarified toml keys formatting vs. toString;
14 months ago, by Fabian Huch
clarified keys module;
14 months ago, by Fabian Huch
pull out toml keys module;
14 months ago, by Fabian Huch
clarified toml parser interface;
14 months ago, by Fabian Huch
prefer symbolic build_history_base_arm;
14 months ago, by wenzelm
build_history: proper support for ISABELLE_APPLE_PLATFORM64;
14 months ago, by wenzelm
clarified isabelle_hg (again, see b9d59669904a);
14 months ago, by wenzelm
clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
14 months ago, by wenzelm
clarified signature: more operations and options concerning Isabelle hg;
14 months ago, by wenzelm
performance tuning: cache graph;
14 months ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
14 months ago, by wenzelm
unused (see also 004b39bf06a5);
14 months ago, by wenzelm
clarified signature and modules: more explicit Build_Log.History;
14 months ago, by wenzelm
tuned: avoid recursion;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
avoid duplicate data;
14 months ago, by wenzelm
output more data;
14 months ago, by wenzelm
tuned whitespace;
14 months ago, by wenzelm
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
14 months ago, by wenzelm
proper ml_statistics (amending aeb511a520f4);
14 months ago, by wenzelm
unify error messages;
14 months ago, by Fabian Huch
add file information to toml parse context and error messages;
14 months ago, by Fabian Huch
add position information to toml parser and error messages;
14 months ago, by Fabian Huch
properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another;
14 months ago, by Fabian Huch
allow re-defining keys in toml object (already checked during parse time);
14 months ago, by Fabian Huch
clarified toString for toml objects;
14 months ago, by Fabian Huch
tuned
14 months ago, by nipkow
tuned message;
14 months ago, by Fabian Huch
better invalidation for schedule cache (only on relevant changes);
14 months ago, by Fabian Huch
tuned;
14 months ago, by Fabian Huch
timing heuristic: parallelize more aggressively to utilize hosts fully;
14 months ago, by Fabian Huch
proper parallel paths for timing heuristic;
14 months ago, by Fabian Huch
scheduled build: allocate cpus more aggressively, to avoid idle threads;
14 months ago, by Fabian Huch
finalize scheduled build only on master node;
14 months ago, by Fabian Huch
finalize current sessions before generating schedule;
14 months ago, by Fabian Huch
clarified signature: more operations;
14 months ago, by Fabian Huch
NEWS
14 months ago, by desharna
merged
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
support for "cluster" table with "hosts" array, and params/options as for "host" table;
14 months ago, by wenzelm
clarified signature: more operations, allow recursive get;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
tuned signature: more operations;
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
tuned output;
14 months ago, by wenzelm
more robust: prefer strict operations;
14 months ago, by wenzelm
tuned message;
14 months ago, by wenzelm
tuned signature: more operations;
14 months ago, by wenzelm
more specific name for type class
14 months ago, by haftmann
proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
clarified modules;
14 months ago, by wenzelm
clarified signature: more operations;
14 months ago, by wenzelm
tuned comments;
14 months ago, by wenzelm
more NEWS;
14 months ago, by wenzelm
more TODO;
14 months ago, by wenzelm
prefer strict test of system options;
14 months ago, by wenzelm
some build cluster resources at TUM;
14 months ago, by wenzelm
build cluster host specifications are based on registry entries (table prefix "host");
14 months ago, by wenzelm
more robust init;
14 months ago, by wenzelm
clarified signature: more operations;
14 months ago, by wenzelm
support interpreted/typed entries via Registry.Category and Registry.Table;
14 months ago, by wenzelm
clarified signature: more operations;
14 months ago, by wenzelm
clarified output;
14 months ago, by wenzelm
support for global registry;
14 months ago, by wenzelm
clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";
14 months ago, by wenzelm
slightly less technical formulation of very specific type class
14 months ago, by haftmann
weakened dependency
14 months ago, by haftmann
explicit type class for discrete linordered semidoms
14 months ago, by haftmann
proper dummy timing entries;
14 months ago, by Fabian Huch
use only finished sessions in timing data;
14 months ago, by Fabian Huch
tuned;
14 months ago, by Fabian Huch
performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
14 months ago, by Fabian Huch
performance tuning for build schedule: faster stopping;
14 months ago, by Fabian Huch
performance tuning for timing heuristic: pre-calculate graph operations;
14 months ago, by Fabian Huch
move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
14 months ago, by Fabian Huch
clarified signature: emphasize mutable instance;
14 months ago, by wenzelm
clarified signature: more operations;
14 months ago, by wenzelm
support for explicit SSH hostname;
14 months ago, by wenzelm
proper local host (amending 62d7ef1da441);
14 months ago, by wenzelm
merged
14 months ago, by nipkow
added lemma
14 months ago, by nipkow
proper default for disjunction (amending 9f7a94117666);
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
more operations;
14 months ago, by wenzelm
avoid option -C: free this latter for build-related configuration;
14 months ago, by wenzelm
more direct indentation, using Symbol.spaces;
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
more accurate treatment of surrounding whitespace;
14 months ago, by wenzelm
obsolete (see also f627ab8c276c);
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
14 months ago, by wenzelm
clarified modules;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);
14 months ago, by wenzelm
more tests;
14 months ago, by wenzelm
clarified exploration of history: more uniform options;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
enable multi-builds (again, see also 0c7419d3dd59);
14 months ago, by wenzelm
explore history more thoroughly;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
clarified "recent" time: days <= 0 means infinity (no constraint);
14 months ago, by wenzelm
tuned whitespace;
14 months ago, by wenzelm
proper exploration of older history: avoid premature fallback on current "rev" (see also d3d5cb2d6866, 6706d6f0afda);
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
tuned output;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
tuned message;
14 months ago, by wenzelm
proper option;
14 months ago, by wenzelm
merged
14 months ago, by wenzelm
proper SQL.string syntax, following actual SQL standard instead of historic variations before PostgreSQL 9.1;
14 months ago, by wenzelm
Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
14 months ago, by paulson
merged
14 months ago, by wenzelm
prefer Time.scale(), following Isabelle/ML;
14 months ago, by wenzelm
proper benchmark command;
14 months ago, by Fabian Huch
merged
14 months ago, by wenzelm
proper progress (see also 45d570945fe4);
14 months ago, by wenzelm
improved build messages;
14 months ago, by Fabian Huch
clarified;
14 months ago, by Lukas Stevens
merged
14 months ago, by paulson
fixed the simplification of Suc n - 1
14 months ago, by paulson
tuned whitespace;
14 months ago, by wenzelm
tuned message;
14 months ago, by wenzelm
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
14 months ago, by wenzelm
more detailed progress for build_log_database, to see better what happens when;
14 months ago, by wenzelm
clarified signature: explicit Progress date;
14 months ago, by wenzelm
more uniform progress;
14 months ago, by wenzelm
more robust: support concurrent output;
14 months ago, by wenzelm
disable multi-builds (again): does not quite work yet;
14 months ago, by wenzelm
clarified modules;
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
proper Compress.Cache;
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
more parallelism via consumer thread: with mailbox limit to avoid ressource problems;
14 months ago, by wenzelm
support for mailbox limit;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
14 months ago, by wenzelm
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
14 months ago, by wenzelm
afford multiple tests on fast machines (see also edb4faf666c9 and 2a26d423d9fb);
14 months ago, by wenzelm
performance tuning: parallel and incremental update of build_log_database;
14 months ago, by wenzelm
performance tuning: more careful database access;
14 months ago, by wenzelm
clarified message;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
tuned;
14 months ago, by wenzelm
prefer old-style import "=>";
14 months ago, by wenzelm
merged
14 months ago, by wenzelm
redundant (see also 3069da1743bc);
14 months ago, by wenzelm
removed obsolete table (see also 6acd1a2bd146);
14 months ago, by wenzelm
more robust init_database();
14 months ago, by wenzelm
proper private_data.transaction_lock;
14 months ago, by wenzelm
clarified names;
14 months ago, by wenzelm
proper support for SSH;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
tuned imports;
14 months ago, by wenzelm
add module for faster scheduled builds;
15 months ago, by Fabian Huch
always use host database and make protected;
15 months ago, by Fabian Huch
read relative cpu from build log;
15 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);
15 months ago, by Fabian Huch
added start date to build jobs, e.g., for build time estimation;
15 months ago, by Fabian Huch
added initial version of benchmark module, e.g., to compare performance of different hosts;
15 months ago, by Fabian Huch
generalized node infos: allow addressing of numa node segments via relative cpus;
15 months ago, by Fabian Huch
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
15 months ago, by Fabian Huch
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
15 months ago, by Fabian Huch
defined statically known tables of Build_Log;
15 months ago, by Fabian Huch
added lemma
14 months ago, by nipkow
added lemma
14 months ago, by nipkow
added lemma
14 months ago, by nipkow
NEWS and CONTRIBUTORS;
14 months ago, by Fabian Huch
remove unused ci-extras component;
14 months ago, by Fabian Huch
use mail module in CI build;
14 months ago, by Fabian Huch
added mail module;
14 months ago, by Fabian Huch
build javamail component and add to main components;
14 months ago, by Fabian Huch
added component for javax mail;
14 months ago, by Fabian Huch
updated to vampire-4.8;
14 months ago, by wenzelm
tuned README;
14 months ago, by wenzelm
update Vampire version, following hints by Martin Desharnais;
14 months ago, by wenzelm
removed junk;
14 months ago, by wenzelm
tuned component_vampire script for Vampire 4.8 and added new flag to force version name
15 months ago, by desharna
prefer Isabelle options for CI mail settings over ci.properties;
14 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.
14 months ago, by paulson
proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);
14 months ago, by wenzelm
unused (see fe9e590ae52f);
14 months ago, by wenzelm
clarified modules;
14 months ago, by wenzelm
merged
14 months ago, by wenzelm
update documentation on simproc_setup;
14 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
proper morphism;
15 months ago, by wenzelm
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
15 months ago, by wenzelm
more compact ML source;
15 months ago, by wenzelm
more robust read_simproc_spec: proper error positions;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
15 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
15 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
15 months ago, by wenzelm
added ML antiquotation "simproc_setup";
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
tuned signature;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified syntax and order of parameters;
15 months ago, by wenzelm
clarified signature: Named_Target.setup works both for global and local theory;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified signature: more concise simproc setup in ML;
15 months ago, by wenzelm
clarified signature: more concise variations on implicit theory setup;
15 months ago, by wenzelm
clarified simproc_setup (passive);
15 months ago, by wenzelm
clarified 'simproc_setup';
15 months ago, by wenzelm
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
15 months ago, by wenzelm
more standard simproc_setup in Isar;
15 months ago, by wenzelm
more standard ML setup;
15 months ago, by wenzelm
proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0
15 months ago, by desharna
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
tip