Skip to content
[Jenkins]Jenkins
log in
Started 8 days 3 hr ago
Took 3 min 14 sec on workermta1
Failed

#1020 (May 6, 2024, 3:42:23 PM)

Changes
  1. Some new simprules – and patches for proofs (detail / hgweb)
  2. merged (detail / hgweb)
  3. tuned proofs;
    tuned whitespace; (detail / hgweb)
  4. merged, resoving conflicts in src/HOL/Nominal/Nominal.thy; (detail / hgweb)
  5. Added tag Isabelle2024-RC3 for changeset 007e6af8a020 (detail / hgweb)
  6. more documentation on "System registry via TOML"; (detail / hgweb)
  7. update to naproche-20240502: proper platform_path for NAPROCHE_FORMALIZATIONS to make it work on Windows; (detail / hgweb)
  8. provide 3.1 for testing (inactive); (detail / hgweb)
  9. build e-3.1, without patch; (detail / hgweb)
  10. disable Isabelle/Naproche for now: does not quite work on Windows; (detail / hgweb)
  11. update and activate naproche component for release; (detail / hgweb)
  12. changed URL to SystemOnTPTP at Geoff's request (detail / hgweb)
  13. tuned spelling; (detail / hgweb)
  14. build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state; (detail / hgweb)
  15. proper directory permissions to make "rm" work, notably for cygwin/etc/pki/ca-trust/extracted/pem/directory-hash; (detail / hgweb)
  16. support more Ubuntu versions; (detail / hgweb)
  17. updated for release; (detail / hgweb)
  18. more robust: avoid spurious ConcurrentModificationException; (detail / hgweb)
  19. update to e-3.0.03-1, with proper support for trivial statements; (detail / hgweb)
  20. more robust; (detail / hgweb)
  21. minor patch for E Prover, based on "git diff -w -r E-3.0.03 E-3.0.08": proper support for trivial statements; (detail / hgweb)
  22. backed out changeset 601ff5c7cad5: not relevant for Isabelle2024; (detail / hgweb)
  23. clone of 0c51e0a6bc37; (detail / hgweb)
  24. merged (detail / hgweb)
  25. update Windows test machines; (detail / hgweb)
  26. A little more tidying in Nominal (detail / hgweb)
  27. More tidying of proofs (detail / hgweb)
  28. Another Nominal example (detail / hgweb)
  29. merged (detail / hgweb)
  30. update Windows build host; (detail / hgweb)
  31. proper command-line; (detail / hgweb)
  32. Tidying up another Nominal example (SOS) (detail / hgweb)
  33. Tidying up another of the nominal examples (detail / hgweb)
  34. More tidying of Nominal proofs (detail / hgweb)
  35. Tidied up another messy theory (detail / hgweb)
  36. More proof tidying for Nominal (detail / hgweb)
  37. Tidying up more messy proofs (detail / hgweb)
  38. Starting to tidy HOL-Nominal-Examples (detail / hgweb)
  39. sketch & explore: recover from duplicate fixed variables in Isar proofs (detail / hgweb)
  40. back to post-release mode -- after fork point; (detail / hgweb)
  41. merged (detail / hgweb)
  42. Added tag Isabelle2024-RC2 for changeset ef2134570abb (detail / hgweb)
  43. Acknowledgement of Ata Keskin for his Martingales material (detail / hgweb)
  44. merged (detail / hgweb)
  45. update to jdk-21.0.3;
    enforce rebuild of Isabelle/ML and Isabelle/Scala; (detail / hgweb)
  46. merged (detail / hgweb)
  47. clarified signature; (detail / hgweb)
  48. make adhoc_overloading respect type constraints (detail / hgweb)
  49. merged (detail / hgweb)
  50. tuned; (detail / hgweb)
  51. clarified signature; (detail / hgweb)
  52. minor performance tuning: avoid redundant server access; (detail / hgweb)
  53. tuned; (detail / hgweb)
  54. clarified modules and options (from store); (detail / hgweb)
  55. clarified signature; (detail / hgweb)
  56. tuned; (detail / hgweb)
  57. clarified signature; (detail / hgweb)
  58. tuned signature; (detail / hgweb)
  59. tuned; (detail / hgweb)
  60. tuned signature; (detail / hgweb)
  61. tuned; (detail / hgweb)
  62. tuned; (detail / hgweb)
  63. more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4); (detail / hgweb)
  64. tuned messages; (detail / hgweb)
  65. tuned; (detail / hgweb)
  66. back to static numa_nodes (reverting part of c2c59de57df9); (detail / hgweb)
  67. tuned messages; (detail / hgweb)
  68. canonical time function for List.nth (detail / hgweb)
  69. Tidied up horrible archaic proofs (detail / hgweb)
  70. merged (detail / hgweb)
  71. clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces); (detail / hgweb)
  72. Streamlining of many more archaic proofs (detail / hgweb)
  73. More tidying of old proofs (detail / hgweb)
  74. merged (detail / hgweb)
  75. Add subgoals variant of 'sketch' command (detail / hgweb)
  76. More tidying and removal of "apply" (detail / hgweb)
  77. merged (detail / hgweb)
  78. prefer canonical theorem name for fact collection declarations (detail / hgweb)
  79. Tidied some messy proofs (detail / hgweb)
  80. merged (detail / hgweb)
  81. tuned; (detail / hgweb)
  82. Tidying ugly proofs (detail / hgweb)

Started by an SCM change

This run spent:

  • 5.5 sec waiting;
  • 3 min 14 sec build duration;
  • 3 min 19 sec total from scheduled to completion.
Revision: 200107cdd3ace94795120c67770f74402ab1903e