- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Yesterday
Yesterday
misc tuning and clarification;
more compact representation;
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;
more compact representation;
more compact representation of theory_id;
compact representation of sets of integers;
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);
Tue, Nov 28
Tue, Nov 28
florian.haftmann committed rISABELLEa91050cd5c93: de-duplicated specification of class ring_bit_operations.
de-duplicated specification of class ring_bit_operations
florian.haftmann committed rAFP41e34fa525fe: de-duplicated specification of class ring_bit_operations.
de-duplicated specification of class ring_bit_operations
nipkow committed rAFPddcba483b350: adjusted T_sift_down: all primitives take 0 time..
adjusted T_sift_down: all primitives take 0 time.
Mon, Nov 27
Mon, Nov 27
desharna committed rAFPd9d71f72ce4e: added missing file following 2702f2046afa.
added missing file following 2702f2046afa
desharna committed rAFPefc72a123fad: documented change in VeriComp.
documented change in VeriComp
desharna committed rAFP2702f2046afa: added framework-independent lemma to lift simulation to bisimulation.
added framework-independent lemma to lift simulation to bisimulation
grouped lemmas for symbolic computations
sorted out lemma duplicates
Sun, Nov 26
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…
Sat, Nov 25
Sat, Nov 25
clarified signature;
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…
more thorough transaction_lock;
obsolete, see also a5896fe040dd;
makarius committed rISABELLEae682b2aab03: removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);.
removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf);
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;
Fri, Nov 24
Fri, Nov 24
clarified buffer_size;
makarius committed rISABELLE1f34f6394383: more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);.
more uniform buffer_size (see also c83cdd300848 and 26c790a6ce43);
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…
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…
prefer Unix-domain socket on Unix;
makarius committed rISABELLE10b6add456d0: support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;.
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
clarified signature: more general make_streams;
more robust exception handling (amending 8cc1ae43e12e);
clarified signature: avoid deprecated URL constructors;
avoid deprecated URL constructors;
Fabian Huch <huch@in.tum.de> committed rISABELLE1a9f3806987d: proper split;.
proper split;
Fabian Huch <huch@in.tum.de> committed rISABELLEff7d48e776ab: properly sort entries;.
properly sort entries;
Fabian Huch <huch@in.tum.de> committed rISABELLEcd7c1acc9cf2: better estimation for unknown jobs;.
better estimation for unknown jobs;
Fabian Huch <huch@in.tum.de> committed rISABELLE1b3a6cc4a2bf: clarified and tuned timing estimation;.
clarified and tuned timing estimation;
Fabian Huch <huch@in.tum.de> committed rISABELLEbe42ba4b4672: split actual approximation from data handling;.
split actual approximation from data handling;
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…
Fabian Huch <huch@in.tum.de> committed rISABELLE30411c1c575d: proper filter for approximations;.
proper filter for approximations;
Fabian Huch <huch@in.tum.de> committed rISABELLE83288e02c6fa: proper inflection point check;.
proper inflection point check;
florian.haftmann committed rAFPf7e0a078fa7b: slightly more elementary characterization of unset_bit.
slightly more elementary characterization of unset_bit
florian.haftmann committed rISABELLE4596a14d9a95: slightly more elementary characterization of unset_bit.
slightly more elementary characterization of unset_bit
florian.haftmann committed rISABELLEbdea2b95817b: more direct characterization of binary bit operations.
more direct characterization of binary bit operations
Thu, Nov 23
Thu, Nov 23
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);
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;
Fabian Huch <huch@in.tum.de> committed rISABELLE6585acdd6505: clarified time estimation: does not use config;.
clarified time estimation: does not use config;
Fabian Huch <huch@in.tum.de> committed rISABELLEf78ee2d48bf5: handle inflection point in interpolation with monotone prefix;.
handle inflection point in interpolation with monotone prefix;
Fabian Huch <huch@in.tum.de> committed rISABELLEd989e00c3ff5: proper computation of sorted prefix;.
proper computation of sorted prefix;
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;
Fabian Huch <huch@in.tum.de> committed rISABELLE1c91e884035d: properly incorporate running tasks into timing heuristic;.
properly incorporate running tasks into timing heuristic;
Fabian Huch <huch@in.tum.de> committed rISABELLEe4fc535d4d2f: proper piecewise linear build time interpolation;.
proper piecewise linear build time interpolation;
Fabian Huch <huch@in.tum.de> committed rISABELLEef76705bf402: clarified ready vs. next ready;.
clarified ready vs. next ready;
Fabian Huch <huch@in.tum.de> committed rISABELLE4df053d29215: introduced path heuristic abstraction;.
introduced path heuristic abstraction;
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…
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…
Wed, Nov 22
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;
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…
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…
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…
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…
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…
dcjm committed rPOLYMLedccebe6f2ac: Fold constant expressions involving shifts and Log2Word. (authored by dcjm).
Fold constant expressions involving shifts and Log2Word.
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.
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…
modernized, reordered, generalized
more correct type annotation
Tue, Nov 21
Tue, Nov 21
proper build with jdk-21 (amending 4fb5e6499da9);
Mon, Nov 20
Mon, Nov 20
more realistic timeouts for lrzcloud2:threads=1;
update to jdk-21.0.1;
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;
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;
makarius committed rISABELLE3641cd880bb3: clarified operation: pick current pull_date instead of previous one;.
clarified operation: pick current pull_date instead of previous one;
florian.haftmann committed rAFP28289b02b23b: operations AND, OR, XOR are specified by characteristic recursive equation.
operations AND, OR, XOR are specified by characteristic recursive equation
florian.haftmann committed rISABELLE74a4776f7a22: operations AND, OR, XOR are specified by characteristic recursive equation.
operations AND, OR, XOR are specified by characteristic recursive equation
Sun, Nov 19
Sun, Nov 19
Fabian Huch <huch@in.tum.de> committed rISABELLEeed4ca224c9c: clarified toml keys operations;.
clarified toml keys operations;
Fabian Huch <huch@in.tum.de> committed rISABELLE6201057b98dd: clarified toml keys: more operations;.
clarified toml keys: more operations;