Skip to content
Started 2 yr 11 mo ago
Took 1 day 6 hr
Aborted

Build #54 (May 30, 2021, 12:14:00 AM)

Changes
  1. merged (detail)
  2. some new and/or varient results about images (detail)
  3. nicer statement of Liouville_theorem (detail)
  4. more lemmas (detail)
  5. max word moved to Word_Lib in AFP (detail)
  6. more robust syntax; (detail)
  7. unused; (detail)
  8. clarified document export names; (detail)
  9. tuned signature; (detail)
  10. tuned; (detail)
  11. tuned; (detail)
  12. avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac; (detail)
  13. compose Latex text as XML, output exported YXML in Isabelle/Scala; (detail)
  14. more direct index_entry: no positions required -- text is eventually moved to .ind file; (detail)
  15. clarified signature; (detail)
  16. clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle"); (detail)
  17. tuned message, e.g. for Pure bootstrap; (detail)
  18. proper signature export (amending b50f8cc8c08e); (detail)
  19. syslog option for "isabelle build"; (detail)
  20. further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea); (detail)
  21. merged (detail)
  22. NEWS; (detail)
  23. clarified index, more like formal @{element_ref}; (detail)
  24. clarified treatment of type constructors; (detail)
  25. misc tuning and clarification; (detail)
  26. tuned signature; (detail)
  27. clarified context; (detail)
  28. more uniform document antiquotations for ML: consolidate former setup for manuals; (detail)
  29. clarified names; (detail)
  30. clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax; (detail)
  31. clarified modules; (detail)
  32. clarified modules; (detail)
  33. tuned; (detail)
  34. clarified signature: avoid dispatch via name; (detail)
  35. clarified, e.g. type variables; (detail)
  36. tuned index; (detail)
  37. more ambitious default for index "is like"; (detail)
  38. tuned; (detail)
  39. support for index entries; (detail)
  40. tuned; (detail)
  41. tuned signature; (detail)
  42. clarified modules; (detail)
  43. clarified old document build; (detail)
  44. unused; (detail)
  45. prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee; (detail)
  46. prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document; (detail)
  47. unused; (detail)
  48. proper Unix lines; (detail)
  49. prefer explicit option document_bibliography (actually ignored by build script); (detail)
  50. explicit option document_bibliography; (detail)
  51. proper bibliography; (detail)
  52. discontinued obsolete "isabelle latex"; (detail)
  53. more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
    clarified ISABELLE_MAKEINDEX options; (detail)
  54. default document_build (lualatex); (detail)
  55. more robust: allow \printindex within the document; (detail)
  56. clarified bash scripts, with public interfaces for user-defined Document_Build.Engine; (detail)
  57. tuned signature; (detail)
  58. option document_preprocessor; (detail)
  59. show symbols in Isabelle/ML instead of perl; (detail)
  60. more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; (detail)
  61. tuned --- more robust; (detail)
  62. discontinued somewhat pointless "fixbookmarks": default output works sufficiently well; (detail)
  63. more uniform bibtex error, without using perl (see 4710dd5093a3); (detail)
  64. proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error); (detail)
  65. tuned; (detail)
  66. clarified command-line options; (detail)
  67. obsolete (see 5a3a2a52648d); (detail)
  68. redundant: copy produced from session document_files; (detail)
  69. clarified treatment of Isabelle .sty files; (detail)
  70. option document_logo; (detail)
  71. proper options; (detail)
  72. option document_build refers to build engine in Isabelle/Scala;
    pdflatex is back as legacy build engine, e.g. for published proceedings; (detail)
  73. redundant: tmp_dir is purged anyway; (detail)
  74. misc tuning and clarification; (detail)
  75. clarified modules; (detail)
  76. tuned --- clarified corner cases; (detail)
  77. more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases; (detail)
  78. clarified signature -- avoid odd warning about scala/bug#6675; (detail)
  79. tuned; (detail)
  80. tuned; (detail)
  81. clarified signature; (detail)
  82. proper syntax of Scala 3; (detail)
  83. enforce syntax of Scala 3; (detail)
Changes
  1. complement reduced to mere abbreviation (detail)
  2. extracted more legacy abbreviations (detail)
  3. max word moved to Word_Lib in AFP (detail)
  4. merge from afp-2021 (detail)
  5. update website (detail)
  6. fix links (detail)
  7. Restore deleted theorem from Szpilrajn (detail)
  8. tuned presentation (detail)
  9. adapted to devel (detail)
  10. adjusted to changes in distribution (detail)
  11. adjust Combinatorics_Words to isabelle@493b1ae188da (detail)
  12. merge from afp-2021 (detail)
  13. make AFP ROOTS globally available for component (detail)
  14. merged (detail)
  15. New entries Combinatorics_Words* (detail)
  16. adjusted to change in distribution (detail)
  17. adapted to Isabelle/466fae6bf22e; (detail)
  18. tuned whitespace; (detail)
  19. Remove comment about missing refinement (detail)
  20. continued uglification, but also fixed some dodgy proofs (detail)
  21. fixed some broken / looping / fragile proofs (detail)
  22. merge from afp-2021 (detail)
  23. simplify usage instructions more (detail)
  24. sitegen for Padic_Ints (detail)
  25. new entry: Padic_Ints (detail)
  26. update affiliation (detail)
  27. New entry: Regressioon_Test_Selection (detail)
  28. metadata for Metalogic_ProofChecker (detail)
  29. new entry Metalogic_ProofChecker (detail)
  30. metadata for GaleStewart_Games (detail)
  31. new entry GaleStewart_Games (detail)
  32. fixed the ROOT file ofr BenOr_Kozen_Reif (detail)
  33. webpage for BenOr_Kozen_Reif (detail)
  34. new entry BenOr_Kozen_Reif (detail)
  35. Slight tidying to shorten too-long lines (detail)
  36. added a necessary acknowledgment (ERC) (detail)
  37. New entry Progress_Tracking (detail)
  38. Revisions by Wenda to eliminate the locale comp_affine_scheme (detail)
  39. renamed a lemma (detail)
  40. Fixed an error in the statement of closed_subsets_empty. Also added syntax priority hints for carrier_of_local_ring_at. (detail)
  41. consolidated metadata of Anthony Bordg, metadata for new Grothendieck entry + sitegen (detail)
  42. new entry: Grothendieck_Schemes (detail)
  43. metadata for IFC_Tracking (detail)
  44. new entry IFC_Tracking (detail)
  45. merged (detail)
  46. adapted to Isabelle/ef1a18e20ace; (detail)
  47. recover some patches after years of continuously changing Isabelle LaTeX output; (detail)
  48. prefer document_preprocessor over document_build; (detail)
  49. prefer document_logo instead of document_build script; (detail)
  50. proper options; (detail)

Started by timer

This run spent:

  • 97 ms waiting;
  • 1 day 6 hr build duration;
  • 1 day 6 hr total from scheduled to completion.
Revision: a1086aebcd78b577745c244d337fe2986b275983
Revision: bdcaff25a22009719555d71dfb8cf8b109bf1648

Timeout has been exceeded