Page MenuHomeIsabelle/Phabricator
Feed All Stories

Yesterday

makarius committed rISABELLE722937a213ef: merged.
merged
Wed, Nov 29, 10:12 PM
makarius committed rISABELLE2c457c4cd486: misc tuning and clarification;.
misc tuning and clarification;
Wed, Nov 29, 10:12 PM
makarius committed rISABELLE01f9128ec655: more compact representation;.
more compact representation;
Wed, Nov 29, 10:12 PM
makarius committed rISABELLE9d6359b71264: more compact representation of theory_id -- via consecutive thread-local ids;.
more compact representation of theory_id -- via consecutive thread-local ids;
Wed, Nov 29, 10:12 PM
makarius committed rISABELLE238c4acdf984: more compact representation;.
more compact representation;
Wed, Nov 29, 10:12 PM
makarius committed rISABELLE6b071d4041d5: tuned signature;.
tuned signature;
Wed, Nov 29, 10:12 PM
makarius committed rISABELLEa1b5357b5473: more compact representation of theory_id;.
more compact representation of theory_id;
Wed, Nov 29, 10:12 PM
makarius committed rISABELLEe671abce8f8e: tuned signature;.
tuned signature;
Wed, Nov 29, 10:12 PM
makarius committed rISABELLE7f24c5be57bd: compact representation of sets of integers;.
compact representation of sets of integers;
Wed, Nov 29, 10:12 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEb3fee0dafd72: generated build schedule explicitly (e.g., for further analysis);.
generated build schedule explicitly (e.g., for further analysis);
Wed, Nov 29, 6:33 PM

Tue, Nov 28

florian.haftmann committed rISABELLEa91050cd5c93: de-duplicated specification of class ring_bit_operations.
de-duplicated specification of class ring_bit_operations
Tue, Nov 28, 9:16 PM
florian.haftmann committed rAFP41e34fa525fe: de-duplicated specification of class ring_bit_operations.
de-duplicated specification of class ring_bit_operations
Tue, Nov 28, 9:16 PM
nipkow committed rAFPddcba483b350: adjusted T_sift_down: all primitives take 0 time..
adjusted T_sift_down: all primitives take 0 time.
Tue, Nov 28, 6:26 PM

Mon, Nov 27

desharna committed rAFPd9d71f72ce4e: added missing file following 2702f2046afa.
added missing file following 2702f2046afa
Mon, Nov 27, 9:12 PM
desharna committed rAFPefc72a123fad: documented change in VeriComp.
documented change in VeriComp
Mon, Nov 27, 10:53 AM
desharna committed rAFP2702f2046afa: added framework-independent lemma to lift simulation to bisimulation.
added framework-independent lemma to lift simulation to bisimulation
Mon, Nov 27, 10:53 AM
florian.haftmann committed rISABELLE7ab8b3f1d84b: generalized.
generalized
Mon, Nov 27, 8:56 AM
florian.haftmann committed rISABELLEa4775fe69f5d: restructured.
restructured
Mon, Nov 27, 8:56 AM
florian.haftmann committed rISABELLE48ca09068adf: grouped lemmas for symbolic computations.
grouped lemmas for symbolic computations
Mon, Nov 27, 8:56 AM
florian.haftmann committed rISABELLEcb72e2c0c539: sorted out lemma duplicates.
sorted out lemma duplicates
Mon, Nov 27, 8:56 AM

Sun, Nov 26

makarius committed rISABELLE212c94edae2b: more reactive headless server, in contrast to 15656ad28691 (when "isabelle….
more reactive headless server, in contrast to 15656ad28691 (when "isabelle…
Sun, Nov 26, 2:04 PM
makarius committed rISABELLE0da44db32646: tuned whitespace;.
tuned whitespace;
Sun, Nov 26, 2:04 PM

Sat, Nov 25

makarius committed rISABELLEa54be9630ef8: clarified modules;.
clarified modules;
Sat, Nov 25, 8:56 PM
makarius committed rISABELLE07799c394b6d: clarified signature;.
clarified signature;
Sat, Nov 25, 8:56 PM
makarius committed rISABELLEad7f485195df: clarified modules;.
clarified modules;
Sat, Nov 25, 8:56 PM
makarius committed rISABELLE6977fb0153fb: clarified modules: Build_Log.private_data provides raw data access without….
clarified modules: Build_Log.private_data provides raw data access without…
Sat, Nov 25, 8:56 PM
makarius committed rISABELLE10eb2ebd23ba: more thorough transaction_lock;.
more thorough transaction_lock;
Sat, Nov 25, 8:56 PM
makarius committed rISABELLE9f2040e5e2d6: obsolete, see also a5896fe040dd;.
obsolete, see also a5896fe040dd;
Sat, Nov 25, 5:11 PM
makarius committed rISABELLEae682b2aab03: removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);.
removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);
Sat, Nov 25, 4:56 PM
makarius committed rISABELLEf13390b2c1ee: provide src/Tools/Demo as example for system component with Isabelle/Scala tool;.
provide src/Tools/Demo as example for system component with Isabelle/Scala tool;
Sat, Nov 25, 4:29 PM

Fri, Nov 24

makarius committed rISABELLE156bfa6a2836: merged.
merged
Fri, Nov 24, 10:27 PM
makarius committed rISABELLEc83cdd300848: clarified buffer_size;.
clarified buffer_size;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE1f34f6394383: more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);.
more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);
Fri, Nov 24, 10:27 PM
makarius committed rISABELLEedc0dbd59d48: merged.
merged
Fri, Nov 24, 10:27 PM
makarius committed rISABELLEbadb3da19ac6: disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL….
disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL…
Fri, Nov 24, 10:27 PM
makarius committed rISABELLEd5cf21ad8b47: workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read….
workaround for "fix" JDK-4512626 in Java 20/21: avoid spurious caret in read…
Fri, Nov 24, 10:27 PM
makarius committed rISABELLEc87e4a5a3823: tuned;.
tuned;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE4d8716098d41: prefer Unix-domain socket on Unix;.
prefer Unix-domain socket on Unix;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE10b6add456d0: support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;.
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLEcaddfe4949a8: tuned;.
tuned;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE13afea5203f1: clarified signature: more general make_streams;.
clarified signature: more general make_streams;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE926fc9ca7360: tuned;.
tuned;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE24d04dd5bf01: more robust exception handling (amending 8cc1ae43e12e);.
more robust exception handling (amending 8cc1ae43e12e);
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE8cc1ae43e12e: clarified signature: avoid deprecated URL constructors;.
clarified signature: avoid deprecated URL constructors;
Fri, Nov 24, 10:27 PM
makarius committed rISABELLE22c41ee13939: avoid deprecated URL constructors;.
avoid deprecated URL constructors;
Fri, Nov 24, 10:27 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE1a9f3806987d: proper split;.
proper split;
Fri, Nov 24, 9:57 PM
nipkow committed rAFPf1056e7f4114: tuned.
tuned
Fri, Nov 24, 6:17 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEff7d48e776ab: properly sort entries;.
properly sort entries;
Fri, Nov 24, 5:53 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE7bb8dba028ce: tuned;.
tuned;
Fri, Nov 24, 5:53 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE322bcfce2b37: tuned;.
tuned;
Fri, Nov 24, 5:53 PM
nipkow committed rAFPb9c5b84c3f11: added publication.
added publication
Fri, Nov 24, 5:37 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEcd7c1acc9cf2: better estimation for unknown jobs;.
better estimation for unknown jobs;
Fri, Nov 24, 5:08 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE1b3a6cc4a2bf: clarified and tuned timing estimation;.
clarified and tuned timing estimation;
Fri, Nov 24, 5:08 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEbe42ba4b4672: split actual approximation from data handling;.
split actual approximation from data handling;
Fri, Nov 24, 5:08 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE6beb60b508e6: clarified timing data vs. timing entries: full top-level data view vs. dynamic….
clarified timing data vs. timing entries: full top-level data view vs. dynamic…
Fri, Nov 24, 5:08 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE30411c1c575d: proper filter for approximations;.
proper filter for approximations;
Fri, Nov 24, 12:38 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE83288e02c6fa: proper inflection point check;.
proper inflection point check;
Fri, Nov 24, 10:41 AM
Fabian Huch <huch@in.tum.de> committed rISABELLE8f6c8a573716: tuned;.
tuned;
Fri, Nov 24, 10:41 AM
florian.haftmann committed rAFPf7e0a078fa7b: slightly more elementary characterization of unset_bit.
slightly more elementary characterization of unset_bit
Fri, Nov 24, 8:05 AM
florian.haftmann committed rISABELLE4596a14d9a95: slightly more elementary characterization of unset_bit.
slightly more elementary characterization of unset_bit
Fri, Nov 24, 8:03 AM
florian.haftmann committed rISABELLEbdea2b95817b: more direct characterization of binary bit operations.
more direct characterization of binary bit operations
Fri, Nov 24, 8:03 AM

Thu, Nov 23

Fabian Huch <huch@in.tum.de> committed rISABELLE49e8b031e0cb: tuned;.
tuned;
Thu, Nov 23, 9:06 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE6bada416ba55: clarified timing data operations: proper estimation (instead of known points);.
clarified timing data operations: proper estimation (instead of known points);
Thu, Nov 23, 9:06 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEd08fb157e300: use proper max threads (limited by available hardware) in heuristics;.
use proper max threads (limited by available hardware) in heuristics;
Thu, Nov 23, 9:06 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE6585acdd6505: clarified time estimation: does not use config;.
clarified time estimation: does not use config;
Thu, Nov 23, 9:06 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEf78ee2d48bf5: handle inflection point in interpolation with monotone prefix;.
handle inflection point in interpolation with monotone prefix;
Thu, Nov 23, 9:06 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEd989e00c3ff5: proper computation of sorted prefix;.
proper computation of sorted prefix;
Thu, Nov 23, 9:06 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEabc27a824419: better build time interpolation: model with Amdahl's law where applicable;.
better build time interpolation: model with Amdahl's law where applicable;
Thu, Nov 23, 3:27 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE1c91e884035d: properly incorporate running tasks into timing heuristic;.
properly incorporate running tasks into timing heuristic;
Thu, Nov 23, 3:27 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEe4fc535d4d2f: proper piecewise linear build time interpolation;.
proper piecewise linear build time interpolation;
Thu, Nov 23, 3:27 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEef76705bf402: clarified ready vs. next ready;.
clarified ready vs. next ready;
Thu, Nov 23, 3:27 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE4df053d29215: introduced path heuristic abstraction;.
introduced path heuristic abstraction;
Thu, Nov 23, 3:27 PM
florian.haftmann committed rISABELLE7449ff77029e: base abstract specification of NOT on recursive equation rather than bit….
base abstract specification of NOT on recursive equation rather than bit…
Thu, Nov 23, 8:02 AM
florian.haftmann committed rAFP608f10ad4828: base abstract specification of NOT on recursive equation rather than bit….
base abstract specification of NOT on recursive equation rather than bit…
Thu, Nov 23, 8:02 AM

Wed, Nov 22

Fabian Huch <huch@in.tum.de> committed rAFPba031e9eb701: more realistic timeouts for lrzcloud2:threads=1;.
more realistic timeouts for lrzcloud2:threads=1;
Wed, Nov 22, 3:26 PM
dcjm committed rPOLYML9395056f7e37: Remove regression test. It doesn't work if int is arbitrary precision and it… (authored by dcjm).
Remove regression test. It doesn't work if int is arbitrary precision and it…
Wed, Nov 22, 9:33 AM
dcjm committed rPOLYMLa0bf38c441ce: Fix two warnings. Remove unused static definition for Real_Conv and remove… (authored by dcjm).
Fix two warnings. Remove unused static definition for Real_Conv and remove…
Wed, Nov 22, 9:33 AM
dcjm committed rPOLYMLba5cba6898bc: Implement Ryu code to convert decimal representation to reals. Remove explicit… (authored by dcjm).
Implement Ryu code to convert decimal representation to reals. Remove explicit…
Wed, Nov 22, 9:33 AM
dcjm committed rPOLYML9067a1f831a4: Use word shifts for IntInf.<< if the argument is short and the highest set bit… (authored by dcjm).
Use word shifts for IntInf.<< if the argument is short and the highest set bit…
Wed, Nov 22, 9:33 AM
dcjm committed rPOLYML57af3ed878bd: Remove RTS function to convert a string to a real since it's now implemented in… (authored by dcjm).
Remove RTS function to convert a string to a real since it's now implemented in…
Wed, Nov 22, 9:33 AM
dcjm committed rPOLYMLedccebe6f2ac: Fold constant expressions involving shifts and Log2Word. (authored by dcjm).
Fold constant expressions involving shifts and Log2Word.
Wed, Nov 22, 9:33 AM
dcjm committed rPOLYML7297b90dc3fd: Remove PolyRealBoxedToLongInt from RTS since it's now implemented in ML. (authored by dcjm).
Remove PolyRealBoxedToLongInt from RTS since it's now implemented in ML.
Wed, Nov 22, 9:33 AM
dcjm committed rPOLYMLaf1c9de31c1b: Implement conversion to arbitrary precision within ML. There is a separate… (authored by dcjm).
Implement conversion to arbitrary precision within ML. There is a separate…
Wed, Nov 22, 9:33 AM
florian.haftmann committed rISABELLE127ba61b2630: modernized, reordered, generalized.
modernized, reordered, generalized
Wed, Nov 22, 8:15 AM
florian.haftmann committed rISABELLE74440d820ba5: more correct type annotation.
more correct type annotation
Wed, Nov 22, 8:15 AM
florian.haftmann committed rAFPb7179a3d107c: tuned proof.
tuned proof
Wed, Nov 22, 8:14 AM

Tue, Nov 21

makarius committed rISABELLE3befd4d1e6f2: proper build with jdk-21 (amending 4fb5e6499da9);.
proper build with jdk-21 (amending 4fb5e6499da9);
Tue, Nov 21, 11:40 PM

Mon, Nov 20

makarius committed rAFPc9a93a5c83cd: more realistic timeouts for lrzcloud2:threads=1;.
more realistic timeouts for lrzcloud2:threads=1;
Mon, Nov 20, 10:32 PM
makarius created Blog Post: Update to OpenJDK 21.
Mon, Nov 20, 10:20 PM · isabelle-dev
makarius committed rISABELLEf318399a9fb6: NEWS;.
NEWS;
Mon, Nov 20, 10:17 PM
makarius committed rISABELLE4fb5e6499da9: update to jdk-21.0.1;.
update to jdk-21.0.1;
Mon, Nov 20, 9:50 PM
makarius committed rISABELLEb6bca0666c38: rebuild jedit with minimal patch for jdk-21, following SVN 25690;.
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
Mon, Nov 20, 9:50 PM
makarius committed rISABELLEd9b32243798f: clarified modules;.
clarified modules;
Mon, Nov 20, 9:50 PM
makarius committed rISABELLEaceca8baf804: suppress duplicate entries systematically using log_name: e.g. relevant for AFP;.
suppress duplicate entries systematically using log_name: e.g. relevant for AFP;
Mon, Nov 20, 9:50 PM
makarius committed rISABELLE3641cd880bb3: clarified operation: pick current pull_date instead of previous one;.
clarified operation: pick current pull_date instead of previous one;
Mon, Nov 20, 9:50 PM
florian.haftmann committed rAFP28289b02b23b: operations AND, OR, XOR are specified by characteristic recursive equation.
operations AND, OR, XOR are specified by characteristic recursive equation
Mon, Nov 20, 9:28 AM
florian.haftmann committed rISABELLE74a4776f7a22: operations AND, OR, XOR are specified by characteristic recursive equation.
operations AND, OR, XOR are specified by characteristic recursive equation
Mon, Nov 20, 9:09 AM

Sun, Nov 19

Fabian Huch <huch@in.tum.de> committed rISABELLEeed4ca224c9c: clarified toml keys operations;.
clarified toml keys operations;
Sun, Nov 19, 10:33 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEdad92daaf73a: tuned;.
tuned;
Sun, Nov 19, 10:33 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE6201057b98dd: clarified toml keys: more operations;.
clarified toml keys: more operations;
Sun, Nov 19, 10:33 PM