Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
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 signature: fewer warnings in IntelliJ IDEA;
6 months ago, by wenzelm
unused (see also 004b39bf06a5);
6 months ago, by wenzelm
clarified signature and modules: more explicit Build_Log.History;
6 months ago, by wenzelm
tuned: avoid recursion;
6 months ago, by wenzelm
tuned;
6 months ago, by wenzelm
avoid duplicate data;
6 months ago, by wenzelm
output more data;
6 months ago, by wenzelm
tuned whitespace;
6 months ago, by wenzelm
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
6 months ago, by wenzelm
proper ml_statistics (amending aeb511a520f4);
6 months ago, by wenzelm
unify error messages;
6 months ago, by Fabian Huch
add file information to toml parse context and error messages;
6 months ago, by Fabian Huch
add position information to toml parser and error messages;
6 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;
6 months ago, by Fabian Huch
allow re-defining keys in toml object (already checked during parse time);
6 months ago, by Fabian Huch
clarified toString for toml objects;
6 months ago, by Fabian Huch
tuned
6 months ago, by nipkow
tuned message;
7 months ago, by Fabian Huch
better invalidation for schedule cache (only on relevant changes);
7 months ago, by Fabian Huch
tuned;
7 months ago, by Fabian Huch
timing heuristic: parallelize more aggressively to utilize hosts fully;
7 months ago, by Fabian Huch
proper parallel paths for timing heuristic;
7 months ago, by Fabian Huch
scheduled build: allocate cpus more aggressively, to avoid idle threads;
7 months ago, by Fabian Huch
finalize scheduled build only on master node;
7 months ago, by Fabian Huch
finalize current sessions before generating schedule;
7 months ago, by Fabian Huch
clarified signature: more operations;
7 months ago, by Fabian Huch
NEWS
7 months ago, by desharna
merged
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
support for "cluster" table with "hosts" array, and params/options as for "host" table;
7 months ago, by wenzelm
clarified signature: more operations, allow recursive get;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned signature: more operations;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
tuned output;
7 months ago, by wenzelm
more robust: prefer strict operations;
7 months ago, by wenzelm
tuned message;
7 months ago, by wenzelm
tuned signature: more operations;
7 months ago, by wenzelm
more specific name for type class
7 months ago, by haftmann
proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
clarified modules;
7 months ago, by wenzelm
clarified signature: more operations;
7 months ago, by wenzelm
tuned comments;
7 months ago, by wenzelm
more NEWS;
7 months ago, by wenzelm
more TODO;
7 months ago, by wenzelm
prefer strict test of system options;
7 months ago, by wenzelm
some build cluster resources at TUM;
7 months ago, by wenzelm
build cluster host specifications are based on registry entries (table prefix "host");
7 months ago, by wenzelm
more robust init;
7 months ago, by wenzelm
clarified signature: more operations;
7 months ago, by wenzelm
support interpreted/typed entries via Registry.Category and Registry.Table;
7 months ago, by wenzelm
clarified signature: more operations;
7 months ago, by wenzelm
clarified output;
7 months ago, by wenzelm
support for global registry;
7 months ago, by wenzelm
clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?";
7 months ago, by wenzelm
slightly less technical formulation of very specific type class
7 months ago, by haftmann
weakened dependency
7 months ago, by haftmann
explicit type class for discrete linordered semidoms
7 months ago, by haftmann
proper dummy timing entries;
7 months ago, by Fabian Huch
use only finished sessions in timing data;
7 months ago, by Fabian Huch
tuned;
7 months ago, by Fabian Huch
performance tuning for build schedule: explicit schedule generation, without mixing heuristics;
7 months ago, by Fabian Huch
performance tuning for build schedule: faster stopping;
7 months ago, by Fabian Huch
performance tuning for timing heuristic: pre-calculate graph operations;
7 months ago, by Fabian Huch
move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values);
7 months ago, by Fabian Huch
clarified signature: emphasize mutable instance;
7 months ago, by wenzelm
clarified signature: more operations;
7 months ago, by wenzelm
support for explicit SSH hostname;
7 months ago, by wenzelm
proper local host (amending 62d7ef1da441);
7 months ago, by wenzelm
merged
7 months ago, by nipkow
added lemma
7 months ago, by nipkow
proper default for disjunction (amending 9f7a94117666);
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
more operations;
7 months ago, by wenzelm
avoid option -C: free this latter for build-related configuration;
7 months ago, by wenzelm
more direct indentation, using Symbol.spaces;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
more accurate treatment of surrounding whitespace;
7 months ago, by wenzelm
obsolete (see also f627ab8c276c);
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords;
7 months ago, by wenzelm
clarified modules;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned;
7 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);
7 months ago, by wenzelm
more tests;
7 months ago, by wenzelm
clarified exploration of history: more uniform options;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
enable multi-builds (again, see also 0c7419d3dd59);
7 months ago, by wenzelm
explore history more thoroughly;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
clarified "recent" time: days <= 0 means infinity (no constraint);
7 months ago, by wenzelm
tuned whitespace;
7 months ago, by wenzelm
proper exploration of older history: avoid premature fallback on current "rev" (see also d3d5cb2d6866, 6706d6f0afda);
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
tuned output;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
tuned message;
7 months ago, by wenzelm
proper option;
7 months ago, by wenzelm
merged
7 months ago, by wenzelm
proper SQL.string syntax, following actual SQL standard instead of historic variations before PostgreSQL 9.1;
7 months ago, by wenzelm
Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family
7 months ago, by paulson
merged
7 months ago, by wenzelm
prefer Time.scale(), following Isabelle/ML;
7 months ago, by wenzelm
proper benchmark command;
7 months ago, by Fabian Huch
merged
7 months ago, by wenzelm
proper progress (see also 45d570945fe4);
7 months ago, by wenzelm
improved build messages;
7 months ago, by Fabian Huch
clarified;
7 months ago, by Lukas Stevens
merged
7 months ago, by paulson
fixed the simplification of Suc n - 1
7 months ago, by paulson
tuned whitespace;
7 months ago, by wenzelm
tuned message;
7 months ago, by wenzelm
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
7 months ago, by wenzelm
more detailed progress for build_log_database, to see better what happens when;
7 months ago, by wenzelm
clarified signature: explicit Progress date;
7 months ago, by wenzelm
more uniform progress;
7 months ago, by wenzelm
more robust: support concurrent output;
7 months ago, by wenzelm
disable multi-builds (again): does not quite work yet;
7 months ago, by wenzelm
clarified modules;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37);
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
proper Compress.Cache;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
more parallelism via consumer thread: with mailbox limit to avoid ressource problems;
7 months ago, by wenzelm
support for mailbox limit;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
7 months ago, by wenzelm
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
7 months ago, by wenzelm
afford multiple tests on fast machines (see also edb4faf666c9 and 2a26d423d9fb);
7 months ago, by wenzelm
performance tuning: parallel and incremental update of build_log_database;
7 months ago, by wenzelm
performance tuning: more careful database access;
7 months ago, by wenzelm
clarified message;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
prefer old-style import "=>";
7 months ago, by wenzelm
merged
7 months ago, by wenzelm
redundant (see also 3069da1743bc);
7 months ago, by wenzelm
removed obsolete table (see also 6acd1a2bd146);
7 months ago, by wenzelm
more robust init_database();
7 months ago, by wenzelm
proper private_data.transaction_lock;
7 months ago, by wenzelm
clarified names;
7 months ago, by wenzelm
proper support for SSH;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned imports;
7 months ago, by wenzelm
add module for faster scheduled builds;
7 months ago, by Fabian Huch
always use host database and make protected;
7 months ago, by Fabian Huch
read relative cpu from build log;
7 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);
7 months ago, by Fabian Huch
added start date to build jobs, e.g., for build time estimation;
7 months ago, by Fabian Huch
added initial version of benchmark module, e.g., to compare performance of different hosts;
7 months ago, by Fabian Huch
generalized node infos: allow addressing of numa node segments via relative cpus;
7 months ago, by Fabian Huch
add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);
7 months ago, by Fabian Huch
added Range object to Host, e.g. to parse/unparse NUMA node ranges;
7 months ago, by Fabian Huch
defined statically known tables of Build_Log;
7 months ago, by Fabian Huch
added lemma
7 months ago, by nipkow
added lemma
7 months ago, by nipkow
added lemma
7 months ago, by nipkow
NEWS and CONTRIBUTORS;
7 months ago, by Fabian Huch
remove unused ci-extras component;
7 months ago, by Fabian Huch
use mail module in CI build;
7 months ago, by Fabian Huch
added mail module;
7 months ago, by Fabian Huch
build javamail component and add to main components;
7 months ago, by Fabian Huch
added component for javax mail;
7 months ago, by Fabian Huch
updated to vampire-4.8;
7 months ago, by wenzelm
tuned README;
7 months ago, by wenzelm
update Vampire version, following hints by Martin Desharnais;
7 months ago, by wenzelm
removed junk;
7 months ago, by wenzelm
tuned component_vampire script for Vampire 4.8 and added new flag to force version name
7 months ago, by desharna
prefer Isabelle options for CI mail settings over ci.properties;
7 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.
7 months ago, by paulson
proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);
7 months ago, by wenzelm
unused (see fe9e590ae52f);
7 months ago, by wenzelm
clarified modules;
7 months ago, by wenzelm
merged
7 months ago, by wenzelm
update documentation on simproc_setup;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
proper morphism;
7 months ago, by wenzelm
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
7 months ago, by wenzelm
more compact ML source;
7 months ago, by wenzelm
more robust read_simproc_spec: proper error positions;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
7 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
7 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
7 months ago, by wenzelm
added ML antiquotation "simproc_setup";
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
tuned signature;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
clarified syntax and order of parameters;
7 months ago, by wenzelm
clarified signature: Named_Target.setup works both for global and local theory;
7 months ago, by wenzelm
clarified signature;
7 months ago, by wenzelm
clarified signature: more concise simproc setup in ML;
7 months ago, by wenzelm
clarified signature: more concise variations on implicit theory setup;
7 months ago, by wenzelm
clarified simproc_setup (passive);
7 months ago, by wenzelm
clarified 'simproc_setup';
7 months ago, by wenzelm
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
7 months ago, by wenzelm
more standard simproc_setup in Isar;
7 months ago, by wenzelm
more standard ML setup;
7 months ago, by wenzelm
proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0
7 months ago, by desharna
added new portfolio for Vampire 4.8
7 months ago, by desharna
tuned signature, following Isabelle/Scala;
7 months ago, by wenzelm
more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;
7 months ago, by wenzelm
tuned;
7 months ago, by wenzelm
proper parallel build tasks;
7 months ago, by wenzelm
more Haskell tests on macOS;
7 months ago, by wenzelm
more NEWS;
7 months ago, by wenzelm
disable naproche component for now: to be updated before the next Isabelle release;
7 months ago, by wenzelm
updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell");
7 months ago, by wenzelm
more NEWS;
8 months ago, by wenzelm
tuned structure;
8 months ago, by wenzelm
update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;
8 months ago, by wenzelm
updated to official release of polyml-5.9.1, based on Ubuntu 18.04 LTS and macOS 11 Big Sur;
8 months ago, by wenzelm
proper options for macOS 11 Big Sur;
8 months ago, by wenzelm
support for official release of polyml-5.9.1;
8 months ago, by wenzelm
updated Linux baseline to Ubuntu 18.04;
8 months ago, by wenzelm
support for macOS 14 Sonoma (only for testing);
8 months ago, by wenzelm
more platform tests: initial support for macOS 14 Sonoma;
8 months ago, by wenzelm
updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;
8 months ago, by wenzelm
merged
8 months ago, by wenzelm
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
8 months ago, by wenzelm
clarified user errors vs. failures, e.g. java.lang.StackOverflowError;
8 months ago, by wenzelm
further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;
8 months ago, by wenzelm
proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);
8 months ago, by wenzelm
distinguish proper interrupts from Poly/ML RTS breakdown;
8 months ago, by wenzelm
tuned;
8 months ago, by wenzelm
tuned;
8 months ago, by wenzelm
proper Isabelle_Thread.try_catch;
8 months ago, by wenzelm
tuned;
8 months ago, by wenzelm
proper Exn.capture / Isabelle_Thread.try_catch;
8 months ago, by wenzelm
tuned;
8 months ago, by wenzelm
clarified signature;
8 months ago, by wenzelm
proper Exn.capture;
8 months ago, by wenzelm
more robust: avoid race condition;
8 months ago, by wenzelm
clarified name;
8 months ago, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
tip