Started 4 days 9 hr ago
Took 3 hr 15 min on workermtahpc

Success Build #459 (May 3, 2021 11:09:10 PM)

Changes
  1. A nice cardinality lemma (detail / hgweb)
  2. tuned (detail / hgweb)
  3. more robust indentation: proper line context after insert; (detail / hgweb)
  4. more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName(); (detail / hgweb)
  5. support nested cases; (detail / hgweb)
  6. tuned; (detail / hgweb)
  7. tuned; (detail / hgweb)
  8. early definition of ML antiquotations; (detail / hgweb)
  9. tuned; (detail / hgweb)
  10. clarified signature: more operations; (detail / hgweb)
  11. clarified signature: more operations; (detail / hgweb)
  12. clarified signature; (detail / hgweb)
  13. tuned signature; (detail / hgweb)
  14. clarified command-line, following other build_XYZ tools; (detail / hgweb)
  15. more recent OCaml and GHC stack: better support for Apple Silicon; (detail / hgweb)
  16. merged (detail / hgweb)
  17. avoid "exec" to change the winpid; (detail / hgweb)
  18. clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c); (detail / hgweb)
  19. fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running); (detail / hgweb)
  20. clarified signature; (detail / hgweb)
  21. rebuild executable for x86_64-darwin; (detail / hgweb)
  22. clarified command-line; (detail / hgweb)
  23. update Linux base-line; (detail / hgweb)
  24. tuned comments; (detail / hgweb)
  25. tuned signature; (detail / hgweb)
  26. simplified typesetting of \<guillemotleft>...\<guillemotright>; (detail / hgweb)
  27. collecting more lemmas concerning multisets (detail / hgweb)
  28. proper use of antiquotations; (detail / hgweb)
  29. more documentation on "Conversions"; (detail / hgweb)
  30. tuned (detail / hgweb)
  31. updated example; (detail / hgweb)
  32. clarified options (again); (detail / hgweb)
  33. more options: update ISABELLE_IDENTIFIER; (detail / hgweb)
  34. clarified conditional ML; (detail / hgweb)
  35. support for conditional ML text; (detail / hgweb)
  36. updated example; (detail / hgweb)
  37. clarified options; (detail / hgweb)
  38. proper context variable handling when stripping leadings quantifiers from test goals (detail / hgweb)
  39. proper etc/ISABELLE_ID from archive (amending 4cba4e250c28); (detail / hgweb)
  40. eliminated perl: prefer elementary GNU printenv; (detail / hgweb)
  41. more robust bootstrap of components; (detail / hgweb)
  42. more self-contained support for macOS; (detail / hgweb)
  43. misc tuning and clarification; (detail / hgweb)
  44. tuned signature; (detail / hgweb)
  45. support for base64 via Isabelle/Scala/ML; (detail / hgweb)
  46. compile; (detail / hgweb)
  47. clarified signature: avoid overlap of String vs. Bytes (both are CharSequence); (detail / hgweb)
  48. clarified signature (again); (detail / hgweb)
  49. merged (detail / hgweb)
  50. clarified signature; (detail / hgweb)
  51. unused; (detail / hgweb)
  52. unused; (detail / hgweb)
  53. clarified signature: more structured arguments, notably for remote provers; (detail / hgweb)
  54. clarified signature; (detail / hgweb)
  55. clarified signature: avoid tmp file; (detail / hgweb)
  56. clarified signature for Scala functions; (detail / hgweb)
  57. clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9); (detail / hgweb)
  58. tuned; (detail / hgweb)
  59. clarified cache; (detail / hgweb)
  60. clarified signature: Bytes extends CharSequence already (see d201996f72a8); (detail / hgweb)
  61. clarified exceptions; (detail / hgweb)
  62. more uniform use of Byte_Message;
    support protocol_message with multiple chunks; (detail / hgweb)
  63. tuned signature; (detail / hgweb)
  64. tuned signature; (detail / hgweb)
  65. more robust treatment of empty markup: it allows to produce formal chunks; (detail / hgweb)
  66. collected combinatorial material (detail / hgweb)
  67. tuned; (detail / hgweb)
  68. tuned; (detail / hgweb)
  69. more documentation; (detail / hgweb)
  70. proper treatment of nested antiquotations;
    clarified signature; (detail / hgweb)
  71. support for ML special forms: modified evaluation similar to Scheme; (detail / hgweb)
  72. clarified signature: more detailed token positions for antiquotations; (detail / hgweb)
  73. merged (detail / hgweb)
  74. clarified signature; (detail / hgweb)
  75. confluent preprocessing for floats in presence of target language numerals (detail / hgweb)
  76. subclass relation (detail / hgweb)
  77. some tinkering with npm versions; (detail / hgweb)
  78. some tinkering with npm versions; (detail / hgweb)
  79. back to post-release mode; (detail / hgweb)
  80. tuned signature; (detail / hgweb)
  81. auto-update due to "isabelle build_vscode"; (detail / hgweb)
  82. tuned; (detail / hgweb)
  83. tuned --- following hints by IntelliJ IDEA; (detail / hgweb)
  84. fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes) (detail / hgweb)
  85. simplified definition (detail / hgweb)

Started by an SCM change

This run spent:

  • 7.4 sec waiting;
  • 3 hr 15 min build duration;
  • 3 hr 15 min total from scheduled to completion.
Revision: 58aed6f71f903b72c5f97b77cad73fc2ff857143