User Details
User Details
- User Since
- Sep 24 2019, 9:33 PM (218 w, 1 d)
- Roles
- Administrator
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;
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;
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;
Sun, Nov 19
Sun, Nov 19
makarius committed rISABELLE778831a801e3: build_history: proper support for ISABELLE_APPLE_PLATFORM64;.
build_history: proper support for ISABELLE_APPLE_PLATFORM64;
prefer symbolic build_history_base_arm;
clarified isabelle_hg (again, see b9d59669904a);
makarius committed rISABELLE674954a49364: clarified signature: explicit Remote_Build.count instead of duplicate entries….
clarified signature: explicit Remote_Build.count instead of duplicate entries…
makarius committed rISABELLEb9d59669904a: clarified signature: more operations and options concerning Isabelle hg;.
clarified signature: more operations and options concerning Isabelle hg;
performance tuning: cache graph;
unused (see also 004b39bf06a5);
tuned signature: fewer warnings in IntelliJ IDEA;
makarius committed rISABELLEae2f5fd0bb5d: clarified signature and modules: more explicit Build_Log.History;.
clarified signature and modules: more explicit Build_Log.History;
Sat, Nov 18
Sat, Nov 18
tuned: avoid recursion;
avoid duplicate data;
makarius committed rISABELLE24e686fe043e: clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;.
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
proper ml_statistics (amending aeb511a520f4);
Sun, Nov 12
Sun, Nov 12
makarius committed rISABELLE30360ee939f4: clarified signature: more operations, allow recursive get;.
clarified signature: more operations, allow recursive get;
makarius committed rISABELLEa2de1f6ff94e: support for "cluster" table with "hosts" array, and params/options as for….
support for "cluster" table with "hosts" array, and params/options as for…
tuned signature: more operations;
clarified signature;
more robust: prefer strict operations;
tuned signature: more operations;
Sat, Nov 11
Sat, Nov 11
makarius committed rISABELLEdb9dba720ac7: proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in….
proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in…
clarified signature;
clarified modules;
clarified signature: more operations;
prefer strict test of system options;
some build cluster resources at TUM;
makarius committed rISABELLE73162a487f94: build cluster host specifications are based on registry entries (table prefix….
build cluster host specifications are based on registry entries (table prefix…
makarius committed rISABELLE409442cb7814: support interpreted/typed entries via Registry.Category and Registry.Table;.
support interpreted/typed entries via Registry.Category and Registry.Table;
clarified signature: more operations;
clarified signature: more operations;
support for global registry;
makarius committed rISABELLE7774e1372476: clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require….
clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require…
Thu, Nov 9
Thu, Nov 9
clarified signature: emphasize mutable instance;
clarified signature: more operations;
support for explicit SSH hostname;
proper local host (amending 62d7ef1da441);
Wed, Nov 8
Wed, Nov 8
proper default for disjunction (amending 9f7a94117666);
makarius committed rISABELLE8378354bbdad: avoid option -C: free this latter for build-related configuration;.
avoid option -C: free this latter for build-related configuration;
more direct indentation, using Symbol.spaces;
more accurate treatment of surrounding whitespace;
clarified signature;
obsolete (see also f627ab8c276c);