Page MenuHomeIsabelle/Phabricator
Feed All Stories

Jan 7 2021

makarius added a comment to T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon).

Also missing: arm64-linux, arm64-darwin (relavant for native JDK on macOS).

Jan 7 2021, 1:18 PM · provers, isabelle-release
makarius closed T30: Component and Isabelle/ML setup for Zipperposition as Resolved.

See Isabelle/162b71f7e554 and Isabelle/11de287ed481.

Jan 7 2021, 1:17 PM · provers
florian.haftmann committed rISABELLEdc62ecc7e59a: dropped junk.
dropped junk
Jan 7 2021, 10:23 AM
makarius committed rISABELLE131ab1a941dd: try GTK 3: some visual dropouts, but more stable e.g. in Sidekick "isabelle….
try GTK 3: some visual dropouts, but more stable e.g. in Sidekick "isabelle…
Jan 7 2021, 12:04 AM

Jan 6 2021

makarius committed rISABELLE9db6072eb711: proper purge for arm64-darwin;.
proper purge for arm64-darwin;
Jan 6 2021, 6:24 PM
makarius committed rISABELLEbf573ed376ef: detect arm64-darwin more reliably: uname could be in x86_64 mode, e.g. within….
detect arm64-darwin more reliably: uname could be in x86_64 mode, e.g. within…
Jan 6 2021, 6:24 PM
makarius committed rISABELLE99b77188d4f7: discontinued somethat pointless sharing: too complicated;.
discontinued somethat pointless sharing: too complicated;
Jan 6 2021, 6:24 PM
makarius committed rISABELLEaf54129abd9e: updated jdk-15.0.1+9, including arm64-darwin;.
updated jdk-15.0.1+9, including arm64-darwin;
Jan 6 2021, 6:24 PM
makarius committed rISABELLE198fe1e7ed32: less verbose;.
less verbose;
Jan 6 2021, 6:23 PM
makarius committed rISABELLE178c9d04e08c: more robust sharing, despite minimal impact on archive size;.
more robust sharing, despite minimal impact on archive size;
Jan 6 2021, 6:23 PM
makarius committed rISABELLE4f1df8d3707b: obsolete, thanks to zulu-jdk directory layout;.
obsolete, thanks to zulu-jdk directory layout;
Jan 6 2021, 6:23 PM
makarius committed rISABELLEb595bcdf5bf3: proper LSMinimumSystemVersion for zulu-jdk-15;.
proper LSMinimumSystemVersion for zulu-jdk-15;
Jan 6 2021, 6:23 PM
makarius committed rISABELLE4a117b57e622: clarified Info.plist;.
clarified Info.plist;
Jan 6 2021, 6:23 PM
makarius committed rISABELLEe67d659d7a41: more direct ISABELLE_JDK_HOME, thanks to zulu-jdk directory layout;.
more direct ISABELLE_JDK_HOME, thanks to zulu-jdk directory layout;
Jan 6 2021, 6:23 PM
makarius committed rISABELLE120ffea2c244: prefer OpenJDK from Azul: supports more versions and platforms;.
prefer OpenJDK from Azul: supports more versions and platforms;
Jan 6 2021, 6:23 PM
makarius committed rISABELLEb34d24153a47: sort lines;.
sort lines;
Jan 6 2021, 6:23 PM
makarius committed rISABELLE824815ec52aa: more NEWS;.
more NEWS;
Jan 6 2021, 6:23 PM
makarius committed rISABELLE66d775f7a6e8: tuned;.
tuned;
Jan 6 2021, 6:23 PM
makarius committed rISABELLE75bd49ba9c28: recovered file-type icons from macos_app;.
recovered file-type icons from macos_app;
Jan 6 2021, 6:23 PM

Jan 5 2021

makarius committed rISABELLEd44552bf310f: clarified application init;.
clarified application init;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE893310d6d76d: recovered bundle icons (not application) from macos_app;.
recovered bundle icons (not application) from macos_app;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEa1d4c9f5207a: more robust;.
more robust;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEe8b8e9a6330f: proper app directory setup, without macos_app component;.
proper app directory setup, without macos_app component;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE7460f92d63fc: prefer official Java 9 operations;.
prefer official Java 9 operations;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE7ef8d77ee761: proper dock icon for macOS;.
proper dock icon for macOS;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEf996348d28ee: obsolete;.
obsolete;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE8d9fb810462b: proper isabelle_home_prefix;.
proper isabelle_home_prefix;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEa95f5ae5a12a: discontinued macOS JavaAppLauncher: re-use plain shell script;.
discontinued macOS JavaAppLauncher: re-use plain shell script;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEd045d900a929: tuned whitespace;.
tuned whitespace;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE27f79e7eb356: tuned -- generate Info.plist in Isabelle/Scala;.
tuned -- generate Info.plist in Isabelle/Scala;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEdd68f20d4041: tuned signature;.
tuned signature;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE0b0c651e823f: more portable component setup;.
more portable component setup;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEf0180048d5ff: updated according to ~~/etc/settings;.
updated according to ~~/etc/settings;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE21af3a90d194: tuned signature;.
tuned signature;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE523806d71dea: proper treatment of XML.Wrapped_Elem, e.g. Markup.class_parameter;.
proper treatment of XML.Wrapped_Elem, e.g. Markup.class_parameter;
Jan 5 2021, 11:19 PM
makarius committed rISABELLEabaff6fb0ff2: clarified quotes;.
clarified quotes;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE4b620e1cb1e9: tuned -- generate script by Isabelle/Scala;.
tuned -- generate script by Isabelle/Scala;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE32618ae1b65d: proper theory name, e.g. for HTML/PIDE presentation;.
proper theory name, e.g. for HTML/PIDE presentation;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE45a34cc581b8: more robust and permissive;.
more robust and permissive;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE696819fe2424: present theory using PIDE markup;.
present theory using PIDE markup;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE517b17e54d28: tuned signature;.
tuned signature;
Jan 5 2021, 11:19 PM
makarius committed rISABELLE3e4df2e689ff: clarified signature;.
clarified signature;
Jan 5 2021, 11:19 PM
nipkow committed rISABELLE2138a4a9031a: tuned.
tuned
Jan 5 2021, 11:25 AM
pruvisto committed rISABELLEc03a148110cc: HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset.
HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset
Jan 5 2021, 3:36 AM
pruvisto committed rAFP8bf81decb8ac: adapted to isabelle-dev/74be162a47cd: added some renamings that were missed….
adapted to isabelle-dev/74be162a47cd: added some renamings that were missed…
Jan 5 2021, 2:25 AM

Jan 4 2021

makarius committed rISABELLE6ba08ec184a1: merged.
merged
Jan 4 2021, 9:51 PM
makarius committed rISABELLEd77bb4441250: more documentation;.
more documentation;
Jan 4 2021, 9:51 PM
makarius committed rISABELLEbef32cb5d26b: override existing action, to retain menu item;.
override existing action, to retain menu item;
Jan 4 2021, 9:51 PM
pruvisto committed rAFPdfe83cc412a3: adapted to isabelle-dev/74be162a47cd.
adapted to isabelle-dev/74be162a47cd
Jan 4 2021, 8:58 PM
pruvisto committed rISABELLE7ad9f197ca7e: HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions.
HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions
Jan 4 2021, 8:55 PM
pruvisto committed rISABELLEab9e27da0e85: HOL-Library: Changed notation for sum_mset.
HOL-Library: Changed notation for sum_mset
Jan 4 2021, 8:55 PM
makarius committed rISABELLE32edc2b4e243: tuned;.
tuned;
Jan 4 2021, 8:35 PM
makarius committed rISABELLE759b6869377d: misc tuning and clarification;.
misc tuning and clarification;
Jan 4 2021, 8:35 PM
makarius committed rISABELLEe7855739409e: tuned signature;.
tuned signature;
Jan 4 2021, 8:35 PM
makarius committed rISABELLE1edf30bc1008: proper thread position for reports;.
proper thread position for reports;
Jan 4 2021, 8:35 PM
makarius committed rISABELLE66b45c3389d3: tuned;.
tuned;
Jan 4 2021, 8:35 PM
makarius committed rISABELLE22f5a6283477: tuned signature;.
tuned signature;
Jan 4 2021, 8:35 PM

Jan 3 2021

makarius committed rISABELLE382309d4b4dc: alternative shortcut, notably for macOS;.
alternative shortcut, notably for macOS;
Jan 3 2021, 11:34 PM
makarius committed rISABELLE4b1cfbf96e36: action isabelle.toggle-full-screen;.
action isabelle.toggle-full-screen;
Jan 3 2021, 11:34 PM
makarius committed rISABELLE473509b160d9: more operations;.
more operations;
Jan 3 2021, 11:34 PM
makarius committed rISABELLE3b14f7315dd2: some attempts at multi-platform full-screen mode;.
some attempts at multi-platform full-screen mode;
Jan 3 2021, 11:34 PM
makarius committed rISABELLEb028e8d22d8d: clarified HTML presentation elements;.
clarified HTML presentation elements;
Jan 3 2021, 4:33 PM
makarius committed rISABELLE03e78b35ebbc: more robust bootstrap: Isabelle-jEdit.shasum could be absent;.
more robust bootstrap: Isabelle-jEdit.shasum could be absent;
Jan 3 2021, 12:18 PM

Jan 2 2021

makarius committed rAFPa31f698ef3f8: avoid multiple uses of the same ML file;.
avoid multiple uses of the same ML file;
Jan 2 2021, 11:55 PM
makarius committed rAFP0668d43edb22: more standard ML file/module names;.
more standard ML file/module names;
Jan 2 2021, 11:55 PM
makarius committed rAFP824acfe540c7: more standard headers;.
more standard headers;
Jan 2 2021, 11:55 PM
makarius committed rISABELLEd2690444c00a: clarified caching;.
clarified caching;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE43c534bba442: tuned whitespace (amending a4bffc0de967);.
tuned whitespace (amending a4bffc0de967);
Jan 2 2021, 11:31 PM
makarius committed rISABELLEf93f0597f4fb: clarified signature: absorb XZ.Cache into XML.Cache;.
clarified signature: absorb XZ.Cache into XML.Cache;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE72b13af7f266: persistent hash code: much faster caching;.
persistent hash code: much faster caching;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE72a8fdfa185d: support more direct hash-consing via XML.Cache;.
support more direct hash-consing via XML.Cache;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE64157cae1ba4: tuned;.
tuned;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE95e0f014cd24: tuned signature;.
tuned signature;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE000bcf2524fd: clarified boundary case;.
clarified boundary case;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE237bd6318cc1: more uniform default --- hardly relevant in practice;.
more uniform default --- hardly relevant in practice;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE3e5a61d9f46a: proper ssh_port (amending ffd8283b7be0);.
proper ssh_port (amending ffd8283b7be0);
Jan 2 2021, 11:31 PM
makarius committed rISABELLEe15621aa8c72: tuned comments;.
tuned comments;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE337e1b135d2f: clarified signature --- internal Cache.none;.
clarified signature --- internal Cache.none;
Jan 2 2021, 11:31 PM
makarius committed rISABELLE38528017e4c8: more verbosity for potentially bulky presentation;.
more verbosity for potentially bulky presentation;
Jan 2 2021, 12:09 AM
makarius committed rISABELLEb51515722274: tuned signature -- prefer Isabelle/ML structure Integer;.
tuned signature -- prefer Isabelle/ML structure Integer;
Jan 2 2021, 12:09 AM
makarius committed rISABELLEf602a380e4f2: tuned signature -- prefer Isabelle/ML structure Integer (despite minor….
tuned signature -- prefer Isabelle/ML structure Integer (despite minor…
Jan 2 2021, 12:09 AM
makarius committed rISABELLE05e2cab9af8b: tuned signature -- prefer Isabelle/ML structure Integer;.
tuned signature -- prefer Isabelle/ML structure Integer;
Jan 2 2021, 12:09 AM

Jan 1 2021

makarius added a comment to T33: Update to jdk-11.0.10, notably for macOS Big Sur.

Full-screen problem: https://bugs.openjdk.java.net/browse/JDK-8256465

Jan 1 2021, 4:53 PM · isabelle-release
makarius added a comment to T33: Update to jdk-11.0.10, notably for macOS Big Sur.

See also OpenJDK 16 development items:

Jan 1 2021, 4:46 PM · isabelle-release

Dec 31 2020

Lars Hupel <lars.hupel@mytum.de> committed rAFP459344fb0c40: Isabelle_Meta_Model: avoid multiple use of ML_file.
Isabelle_Meta_Model: avoid multiple use of ML_file
Dec 31 2020, 2:59 PM
Lars Hupel <lars.hupel@mytum.de> committed rAFP0327fb7d3352: ensure that at least an empty report file exists.
ensure that at least an empty report file exists
Dec 31 2020, 9:41 AM

Dec 30 2020

Lars Hupel <lars.hupel@mytum.de> committed rAFP0c0f25783758: delete report file if already exists.
delete report file if already exists
Dec 30 2020, 4:03 PM

Dec 29 2020

nipkow committed rISABELLE662f286492b1: more lemmas.
more lemmas
Dec 29 2020, 7:20 PM
nipkow committed rISABELLE9283e9d45060: added lemmas.
added lemmas
Dec 29 2020, 7:30 AM

Dec 28 2020

nipkow committed rISABELLE8644c1efbda2: added lemma.
added lemma
Dec 28 2020, 5:52 PM

Dec 27 2020

makarius committed rISABELLE2d7060a3ea11: tuned whitespace;.
tuned whitespace;
Dec 27 2020, 5:53 PM
makarius committed rISABELLE90f4df1970b8: Added tag Isabelle2021-RC1 for changeset d4b67dc6f4eb.
Added tag Isabelle2021-RC1 for changeset d4b67dc6f4eb
Dec 27 2020, 5:51 PM
makarius committed rWEBSITEcb90921a4216: tuned;.
tuned;
Dec 27 2020, 5:46 PM
makarius committed rWEBSITEa49a00fc4633: updated for release;.
updated for release;
Dec 27 2020, 5:13 PM
makarius committed rWEBSITE372d301ab6b6: updated URL (auto-forwarded);.
updated URL (auto-forwarded);
Dec 27 2020, 5:13 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2021.
Dec 27 2020, 5:02 PM
makarius committed rISABELLEd4b67dc6f4eb: updated for release;.
updated for release;
Dec 27 2020, 3:17 PM
makarius committed rISABELLE238ddf525da4: clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in….
clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in…
Dec 27 2020, 3:17 PM
makarius committed rISABELLE4519ba8da368: follow Phabricator update 2020 Week 42;.
follow Phabricator update 2020 Week 42;
Dec 27 2020, 2:14 PM
makarius committed rISABELLE56eae6d161db: tuned;.
tuned;
Dec 27 2020, 2:04 PM