isabelle: Graph

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
14 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;
14 months ago, by wenzelm
proper morphism;
14 months ago, by wenzelm
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
14 months ago, by wenzelm
more compact ML source;
14 months ago, by wenzelm
more robust read_simproc_spec: proper error positions;
14 months ago, by wenzelm
tuned signature;
14 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
14 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
14 months ago, by wenzelm
more standard simproc_setup using ML antiquotation;
14 months ago, by wenzelm
added ML antiquotation "simproc_setup";
14 months ago, by wenzelm
clarified signature;
14 months ago, by wenzelm
clarified signature;
14 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
14 months ago, by desharna
added new portfolio for Vampire 4.8
15 months ago, by desharna
tuned signature, following Isabelle/Scala;
15 months ago, by wenzelm
more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
proper parallel build tasks;
15 months ago, by wenzelm
more Haskell tests on macOS;
15 months ago, by wenzelm
more NEWS;
15 months ago, by wenzelm
disable naproche component for now: to be updated before the next Isabelle release;
15 months ago, by wenzelm
updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell");
15 months ago, by wenzelm
more NEWS;
15 months ago, by wenzelm
tuned structure;
15 months ago, by wenzelm
update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;
15 months ago, by wenzelm
updated to official release of polyml-5.9.1, based on Ubuntu 18.04 LTS and macOS 11 Big Sur;
15 months ago, by wenzelm
proper options for macOS 11 Big Sur;
15 months ago, by wenzelm
support for official release of polyml-5.9.1;
15 months ago, by wenzelm
updated Linux baseline to Ubuntu 18.04;
15 months ago, by wenzelm
support for macOS 14 Sonoma (only for testing);
15 months ago, by wenzelm
more platform tests: initial support for macOS 14 Sonoma;
15 months ago, by wenzelm
updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;
15 months ago, by wenzelm
merged
15 months ago, by wenzelm
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
15 months ago, by wenzelm
clarified user errors vs. failures, e.g. java.lang.StackOverflowError;
15 months ago, by wenzelm
further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;
15 months ago, by wenzelm
proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);
15 months ago, by wenzelm
distinguish proper interrupts from Poly/ML RTS breakdown;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
proper Isabelle_Thread.try_catch;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
proper Exn.capture / Isabelle_Thread.try_catch;
15 months ago, by wenzelm
tuned;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
proper Exn.capture;
15 months ago, by wenzelm
more robust: avoid race condition;
15 months ago, by wenzelm
clarified name;
15 months ago, by wenzelm
clarified signature;
15 months ago, by wenzelm
clarified comments;
15 months ago, by wenzelm
Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts
15 months ago, by paulson
atin now an abbreviation for atin_within, which has been moved to Abstract_Limits
15 months ago, by paulson
merged
15 months ago, by paulson
New proofs also some slightly faster existing proofs
15 months ago, by paulson
updated to hugo-0.119.0;
15 months ago, by Fabian Huch
add component build tool for hugo from afp-devel;
15 months ago, by Fabian Huch
removed test failing on some platform
15 months ago, by desharna
mini2 is not active due to upgrade;
15 months ago, by wenzelm
more PLATFORMS;
15 months ago, by wenzelm
update documentation on Isabelle/ML exceptions;
15 months ago, by wenzelm
misc tuning;
15 months ago, by wenzelm
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
15 months ago, by wenzelm
proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b);
15 months ago, by wenzelm
proper Scala version, e.g. for IntelliJ IDEA;
15 months ago, by wenzelm
NEWS
15 months ago, by desharna
used standard Time.compare in Sledgehammer's preplay
15 months ago, by desharna
moved variable bindings to tighter scope
15 months ago, by desharna
removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer
15 months ago, by desharna
removed unused function parameter
15 months ago, by desharna
merged
15 months ago, by paulson
A couple of new lemmas
15 months ago, by paulson
merged
15 months ago, by wenzelm
more NEWS;
15 months ago, by wenzelm
explicitly reject 'handle' with catch-all patterns;
15 months ago, by wenzelm
avoid accidental 'handle' of interrupts;
15 months ago, by wenzelm