Page MenuHomeIsabelle/Phabricator

makarius (Makarius Wenzel)
UserAdministrator

Projects

User Details

User Since
Sep 24 2019, 9:33 PM (237 w, 3 d)
Roles
Administrator

Recent Activity

Wed, Apr 10

makarius committed rAFPb5c20c32ec87: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFPc60cdb60c99c: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFPd874320a81ca: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFP31fcd760227c: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFPec1c704f4022: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 9:37 PM
makarius committed rISABELLE36389d25d33e: rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04….
rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04…
Wed, Apr 10, 1:23 PM
makarius committed rISABELLE1a9f0159de5b: merged.
merged
Wed, Apr 10, 1:23 PM

Fri, Apr 5

makarius committed rAFP7efa5914d67a: avoid Scala if-expressions and thus make it work both for -new-syntax or -old….
avoid Scala if-expressions and thus make it work both for -new-syntax or -old…
Fri, Apr 5, 11:33 PM
makarius committed rISABELLE5afbf04418ec: avoid Scala if-expressions and thus make it work both for -new-syntax or -old….
avoid Scala if-expressions and thus make it work both for -new-syntax or -old…
Fri, Apr 5, 11:32 PM
makarius committed rISABELLEbda75c790bfa: proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);.
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
Fri, Apr 5, 11:32 PM
makarius committed rISABELLE1b986e5f9764: adjust generated Scala to make it work with scalac -old-syntax and -new-syntax….
adjust generated Scala to make it work with scalac -old-syntax and -new-syntax…
Fri, Apr 5, 11:32 PM

Thu, Apr 4

makarius committed rISABELLEe2174bf626b8: more portable: prefer official JDBC operation DatabaseMetaData.getColumns();.
more portable: prefer official JDBC operation DatabaseMetaData.getColumns();
Thu, Apr 4, 6:20 PM
makarius committed rISABELLE4f9e4527a4e3: tuned signature;.
tuned signature;
Thu, Apr 4, 6:20 PM
makarius committed rAFP931936ecb4e1: proper guard to avoid spurious system messages like "### Ignored report message….
proper guard to avoid spurious system messages like "### Ignored report message…
Thu, Apr 4, 5:48 PM
makarius committed rAFPe2ca9e3a5543: tuned: more readable;.
tuned: more readable;
Thu, Apr 4, 5:48 PM
makarius committed rAFPccce18642d4c: avoid danger of exponental blowup;.
avoid danger of exponental blowup;
Thu, Apr 4, 5:48 PM
makarius committed rAFP810c04472d86: tuned spelling;.
tuned spelling;
Thu, Apr 4, 5:48 PM
makarius committed rAFP93adc832ec72: avoid aliases of well-known Pure concepts, for the sake of readability;.
avoid aliases of well-known Pure concepts, for the sake of readability;
Thu, Apr 4, 5:48 PM

Wed, Apr 3

makarius committed rWEBSITE37c1362d06cd: update screenshot;.
update screenshot;
Wed, Apr 3, 3:30 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2024.
Wed, Apr 3, 2:57 PM · isabelle-release
makarius committed rWEBSITE4bc2f39188bf: update for release;.
update for release;
Wed, Apr 3, 2:50 PM
makarius committed rWEBSITEbd4ebadcd3f6: update for release;.
update for release;
Wed, Apr 3, 2:36 PM
makarius committed rWEBSITE3bede14bad93: merged.
merged
Wed, Apr 3, 1:20 PM
makarius committed rWEBSITEcff766c2f538: update for release;.
update for release;
Wed, Apr 3, 1:20 PM
makarius committed rISABELLE6e7f266b9ac2: updated for release;.
updated for release;
Wed, Apr 3, 1:20 PM
makarius committed rISABELLE01ddd3c203da: Added tag Isabelle2024-RC1 for changeset 1231a7fb2510.
Added tag Isabelle2024-RC1 for changeset 1231a7fb2510
Wed, Apr 3, 1:20 PM
makarius committed rAFP12db4a7858c0: proper condition = ISABELLE_GOEXE, to make it work without "isabelle go_setup";.
proper condition = ISABELLE_GOEXE, to make it work without "isabelle go_setup";
Wed, Apr 3, 11:36 AM
makarius committed rISABELLE1231a7fb2510: misc tuning for release;.
misc tuning for release;
Wed, Apr 3, 11:12 AM
makarius committed rISABELLEee07b7738a24: update for release;.
update for release;
Wed, Apr 3, 11:12 AM

Tue, Apr 2

makarius committed rISABELLEd67cacd09251: merged.
merged
Tue, Apr 2, 7:32 PM
makarius committed rISABELLE09e9819beef6: update to stack-2.15.5, stackage-lts-22.15;.
update to stack-2.15.5, stackage-lts-22.15;
Tue, Apr 2, 7:32 PM
makarius committed rISABELLE951c371c1cd9: clarified names: discontinue odd convention from 3 decades ago;.
clarified names: discontinue odd convention from 3 decades ago;
Tue, Apr 2, 7:32 PM
makarius committed rISABELLE40f5ddeda2b4: further performance tuning (after f906f7f83dae): interactive mode is closer to….
further performance tuning (after f906f7f83dae): interactive mode is closer to…
Tue, Apr 2, 7:32 PM
makarius committed rAFP5819f2a448d6: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Tue, Apr 2, 4:11 PM
makarius committed rAFPc99fa2f32389: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Tue, Apr 2, 4:11 PM
makarius committed rAFP4034bbbba794: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Tue, Apr 2, 4:11 PM
makarius committed rAFPde38656982c3: tuned whitespace;.
tuned whitespace;
Tue, Apr 2, 4:11 PM
makarius committed rAFPc1af731e14b9: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Tue, Apr 2, 4:11 PM
makarius committed rAFP0c06ebfbaba1: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Tue, Apr 2, 4:11 PM

Mon, Apr 1

makarius committed rISABELLE60b6c735b5d5: clarified signature: prefer authentic cterm used in Simplifier, avoid potential….
clarified signature: prefer authentic cterm used in Simplifier, avoid potential…
Mon, Apr 1, 7:06 PM
makarius committed rISABELLE0d94dd2fd2d0: clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);.
clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
Mon, Apr 1, 7:06 PM
makarius committed rISABELLE588ea80f16bb: provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;.
provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;
Mon, Apr 1, 7:06 PM
makarius committed rISABELLE1478c6d52864: clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that….
clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that…
Mon, Apr 1, 7:06 PM

Thu, Mar 28

makarius committed rAFP0df87a34e8a0: merged.
merged
Thu, Mar 28, 5:51 PM
makarius committed rAFPabe7b3319f06: tuned whitespace;.
tuned whitespace;
Thu, Mar 28, 5:51 PM
makarius committed rAFP5aca58481bd5: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Thu, Mar 28, 5:51 PM
makarius committed rAFP2c25484e1496: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Thu, Mar 28, 5:51 PM
makarius committed rAFP4c396108a3a9: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Thu, Mar 28, 5:51 PM
makarius committed rISABELLE87f90735e6dd: removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g..
removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g.
Thu, Mar 28, 4:45 PM
makarius committed rISABELLE9279e96eb34e: clarified signature;.
clarified signature;
Thu, Mar 28, 4:45 PM
makarius committed rISABELLE42bc8ab751c1: clarified modules: more official Sessions.notable_groups;.
clarified modules: more official Sessions.notable_groups;
Thu, Mar 28, 4:45 PM
makarius committed rAFP9ce4d6a809c6: update to Isabelle/42bc8ab751c1;.
update to Isabelle/42bc8ab751c1;
Thu, Mar 28, 4:45 PM
makarius committed rISABELLE9cdc4f533b91: rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;.
rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;
Thu, Mar 28, 1:16 PM
makarius committed rISABELLE7d8a24c5559d: tuned signature;.
tuned signature;
Thu, Mar 28, 12:20 PM
makarius committed rISABELLEb525f783b784: tuned;.
tuned;
Thu, Mar 28, 12:20 PM
makarius committed rISABELLEa213dd3c0b29: tuned signature;.
tuned signature;
Thu, Mar 28, 12:19 PM

Wed, Mar 27

makarius committed rISABELLE308ccc1ef982: proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;.
proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;
Wed, Mar 27, 10:56 PM
makarius committed rAFP1699d5f4b11d: proper Go setup, following Isabelle/da323d3d7570;.
proper Go setup, following Isabelle/da323d3d7570;
Wed, Mar 27, 10:35 PM
makarius committed rISABELLEda323d3d7570: proper "isabelle go_setup" for Jenkins;.
proper "isabelle go_setup" for Jenkins;
Wed, Mar 27, 10:12 PM
makarius committed rAFP1a2512112874: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFPd8244335636c: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFPd9d45697c125: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFP455b44957816: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rAFPd0bd37a0fea4: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Mar 27, 9:52 PM
makarius committed rISABELLEa0210a24b547: dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);.
dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);
Wed, Mar 27, 9:51 PM
makarius committed rISABELLE742e39db4d58: tuned message;.
tuned message;
Wed, Mar 27, 5:51 PM
makarius committed rISABELLEa0f93621c332: merged.
merged
Wed, Mar 27, 5:47 PM
makarius committed rISABELLE30eb547bda4a: tuned NEWS;.
tuned NEWS;
Wed, Mar 27, 5:47 PM
makarius committed rISABELLE0732ee5c8ee1: support for "all" platforms;.
support for "all" platforms;
Wed, Mar 27, 5:47 PM
makarius committed rISABELLEb1e2246147eb: clarified signature;.
clarified signature;
Wed, Mar 27, 5:47 PM
makarius committed rISABELLE71d005ffa9fe: remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and….
remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and…
Wed, Mar 27, 3:53 PM
makarius committed rISABELLE98808cc7b0c1: tuned;.
tuned;
Wed, Mar 27, 3:02 PM
makarius committed rISABELLEebd988ee1d57: more robust Markdown;.
more robust Markdown;
Wed, Mar 27, 2:40 PM
makarius committed rISABELLE5c00c04f09fb: misc tuning;.
misc tuning;
Wed, Mar 27, 2:39 PM
makarius committed rISABELLEa2d15ad6877a: run "isabelle components_build -u";.
run "isabelle components_build -u";
Wed, Mar 27, 2:20 PM
makarius committed rISABELLE38bbc2ff3c24: remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup";.
remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup";
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEa03a7d4b82f8: more Setup_Tool services;.
more Setup_Tool services;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLE64e57aafca1e: tuned order;.
tuned order;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLE27f2a6bd5616: proper SSH operations;.
proper SSH operations;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEd1ac1bb01060: clarified signature;.
clarified signature;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLE77e605c66797: clarified signature: explicit variable is easier to find in source;.
clarified signature: explicit variable is easier to find in source;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEc43a51fde4f5: tuned signature: more permissive;.
tuned signature: more permissive;
Wed, Mar 27, 1:41 PM
makarius committed rISABELLEba06861e91f9: proper services for Setup_Tool --- avoid hardwired stuff;.
proper services for Setup_Tool --- avoid hardwired stuff;
Wed, Mar 27, 1:41 PM

Tue, Mar 26

makarius committed rISABELLEac4412562c7b: more robust XML body: allow empty text, as well as arbitrary pro-forma markup….
more robust XML body: allow empty text, as well as arbitrary pro-forma markup…
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEce9b649ee2dd: NEWS for "isabelle go_setup";.
NEWS for "isabelle go_setup";
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEfb96063456fd: more robust: untyped/unscoped markup elements need to reside in module Markup….
more robust: untyped/unscoped markup elements need to reside in module Markup…
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE339325fdb128: misc tuning for release;.
misc tuning for release;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE6d01661a055b: merged;.
merged;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE07c83d3369c0: misc tuning, following go_setup;.
misc tuning, following go_setup;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEf1686f71dffc: proper platform_path for Windows;.
proper platform_path for Windows;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEb082476a8036: dynamic setup of Go component, similar to Dotnet;.
dynamic setup of Go component, similar to Dotnet;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEac10e32938df: clarified signature: more operations;.
clarified signature: more operations;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE6964a23f595a: tuned comments;.
tuned comments;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE914c4a81027d: clarified signature: explicit type Platform.Info with derived operations;.
clarified signature: explicit type Platform.Info with derived operations;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEa4d94dd5c210: less ambitious parallelism: avoid exhaustion of memory (64GB total);.
less ambitious parallelism: avoid exhaustion of memory (64GB total);
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE34c20c8bbdc5: tuned;.
tuned;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEd89685d3d306: provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup";.
provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup";
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE31ebb6be32b0: tuned messages;.
tuned messages;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLE7e52091795e8: update to bash_process-20240326;.
update to bash_process-20240326;
Tue, Mar 26, 10:12 PM
makarius committed rISABELLEee449ca91c3b: build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all….
build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all…
Tue, Mar 26, 10:12 PM