Skip to content
[Jenkins]Jenkins
log in

Changes

#1019 (Apr 11, 2024, 2:15:11 PM)

  1. tweaked time functions for median-of-medians selection in HOL-Data_Structures — Manuel Eberl <manuel@pruvisto.org> / hgweb
  2. merged — wenzelm / hgweb
  3. rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta; — wenzelm / hgweb
  4. Tiny tweaks to proofs — paulson <lp15@cam.ac.uk> / hgweb
  5. A bit of new material about type class "infinite", from Eval_FO — paulson <lp15@cam.ac.uk> / hgweb
  6. avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax; — wenzelm / hgweb
  7. proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...); — wenzelm / hgweb
  8. adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested; — wenzelm / hgweb
  9. Add entry on Sketch_and_Explore to CONTRIBUTORS — Simon Wimmer <wimmers@in.tum.de> / hgweb
  10. moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory — Manuel Eberl <manuel@pruvisto.org> / hgweb
  11. more portable: prefer official JDBC operation DatabaseMetaData.getColumns(); — wenzelm / hgweb
  12. tuned signature; — wenzelm / hgweb

#1018 (Apr 4, 2024, 3:30:29 PM)

  1. moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory — Manuel Eberl <manuel@pruvisto.org> / hgweb
  2. documented new syntax for fBall and fBex — desharna / hgweb
  3. updated for release; — wenzelm / hgweb
  4. Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 — wenzelm / hgweb
  5. misc tuning for release; — wenzelm / hgweb
  6. update for release; — wenzelm / hgweb
  7. merged — wenzelm / hgweb
  8. update to stack-2.15.5, stackage-lts-22.15; — wenzelm / hgweb
  9. clarified names: discontinue odd convention from 3 decades ago; — wenzelm / hgweb
  10. further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations; — wenzelm / hgweb
  11. added documentation for meromorphicity etc. in HOL-Complex_Analysis — Manuel Eberl <manuel@pruvisto.org> / hgweb
  12. merged — desharna / hgweb
  13. remove transitional (dummy) component list for Go — Lars Hupel <lars@hupel.info> / hgweb

#1017 (Apr 2, 2024, 8:36:08 AM)

  1. merged — desharna / hgweb
  2. clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code; — wenzelm / hgweb
  3. clarified names (see also 9c00a46d69d0, c5cd7a58cf2d);
    NB: Simplifier.set_trace_ops overrides Pure setup for Simplifier_Trace panel, but that is hardly every used in practice; — wenzelm / hgweb
  4. provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version; — wenzelm / hgweb
  5. clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that "very_slow" is normally used together with "slow"; — wenzelm / hgweb
  6. moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields — Manuel Eberl <eberlm@in.tum.de> / hgweb
  7. update NEWS; — Fabian Huch <huch@in.tum.de> / hgweb
  8. moved web_app module from AFP (e.g., for building web services for the distributed build); — Fabian Huch <huch@in.tum.de> / hgweb
  9. added special syntax for FSet.Ball and FSet.Bex — desharna / hgweb
  10. tuned proof — desharna / hgweb
  11. tuned proofs of Equiv_Relations.equiv — desharna / hgweb

#1016 (Mar 29, 2024, 7:30:12 PM)

  1. moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields — Manuel Eberl <eberlm@in.tum.de> / hgweb
  2. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
  3. removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML); — wenzelm / hgweb
  4. clarified signature; — wenzelm / hgweb
  5. clarified modules: more official Sessions.notable_groups; — wenzelm / hgweb
  6. tuned — nipkow / hgweb
  7. merged — paulson / hgweb
  8. An assortment of new material, mostly due to Manuel — paulson <lp15@cam.ac.uk> / hgweb

#1015 (Mar 28, 2024, 3:24:23 PM)

  1. test — wenzelm / hgweb
  2. rebuild rsync-3.2.7 on current platforms, including native arm64-darwin;
    provide official etc/platforms.props, to retain platform directories after Components.Directory.clean() -- e.g. for SSH upload; — wenzelm / hgweb
  3. tuned signature; — wenzelm / hgweb
  4. tuned; — wenzelm / hgweb
  5. tuned signature; — wenzelm / hgweb

#1014 (Mar 28, 2024, 1:39:38 PM)

  1. test — wenzelm / hgweb

#1013 (Mar 28, 2024, 8:33:11 AM)

  1. tuned proofs of Equiv_Relations.equiv — desharna / hgweb
  2. merged — desharna / hgweb
  3. proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests; — wenzelm / hgweb
  4. proper "isabelle go_setup" for Jenkins; — wenzelm / hgweb
  5. added lemma wfp_on_image and author name to theory — desharna / hgweb

#1012 (Mar 27, 2024, 10:09:08 PM)

  1. proper "isabelle go_setup" for Jenkins; — wenzelm / hgweb
  2. dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24); — wenzelm / hgweb
  3. tuned message; — wenzelm / hgweb
  4. merged — wenzelm / hgweb
  5. merged — nipkow / hgweb
  6. updated time functions for Array_Braun — nipkow / hgweb
  7. merged — paulson / hgweb
  8. New material and a bit of refactoring — paulson <lp15@cam.ac.uk> / hgweb
  9. tuned NEWS; — wenzelm / hgweb
  10. support for "all" platforms; — wenzelm / hgweb
  11. clarified signature; — wenzelm / hgweb
  12. remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and 37f852399a32); — wenzelm / hgweb
  13. tuned; — wenzelm / hgweb
  14. more robust Markdown; — wenzelm / hgweb
  15. misc tuning;
    more text; — wenzelm / hgweb
  16. run "isabelle components_build -u"; — wenzelm / hgweb
  17. remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup"; — wenzelm / hgweb
  18. tuned order; — wenzelm / hgweb
  19. more Setup_Tool services; — wenzelm / hgweb
  20. clarified signature; — wenzelm / hgweb
  21. proper SSH operations; — wenzelm / hgweb
  22. tuned signature: more permissive; — wenzelm / hgweb
  23. clarified signature: explicit variable is easier to find in source; — wenzelm / hgweb
  24. proper services for Setup_Tool --- avoid hardwired stuff; — wenzelm / hgweb

#1011 (Mar 27, 2024, 11:51:11 AM)

  1. added lemma wfp_on_image and author name to theory — desharna / hgweb
  2. merged — desharna / hgweb
  3. more robust XML body: allow empty text, as well as arbitrary pro-forma markup (e.g. see XML.blob in Isabelle/ML); — wenzelm / hgweb
  4. more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51); — wenzelm / hgweb
  5. misc tuning for release; — wenzelm / hgweb
  6. merged; — wenzelm / hgweb
  7. NEWS for "isabelle go_setup"; — wenzelm / hgweb
  8. proper platform_path for Windows; — wenzelm / hgweb
  9. misc tuning, following go_setup; — wenzelm / hgweb
  10. dynamic setup of Go component, similar to Dotnet; — wenzelm / hgweb
  11. tuned comments; — wenzelm / hgweb
  12. clarified signature: more operations; — wenzelm / hgweb
  13. clarified signature: explicit type Platform.Info with derived operations; — wenzelm / hgweb
  14. less ambitious parallelism: avoid exhaustion of memory (64GB total); — wenzelm / hgweb
  15. provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup"; — wenzelm / hgweb
  16. tuned; — wenzelm / hgweb
  17. tuned messages; — wenzelm / hgweb
  18. update to bash_process-20240326; — wenzelm / hgweb
  19. build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all platform directories (e.g. for SSH upload); — wenzelm / hgweb
  20. clarified meaning of platform.props: update on default; — wenzelm / hgweb
  21. allow raw input in HTML (e.g., for web applications); — Fabian Huch <huch@in.tum.de> / hgweb

#1010 (Mar 26, 2024, 2:37:33 PM)

  1. renamed lemma wfP_iff_ex_minimal to wfp_iff_ex_minimal — desharna / hgweb

#1009 (Mar 26, 2024, 9:33:11 AM)

  1. added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on — desharna / hgweb
  2. merged — desharna / hgweb
  3. obsolete: base-line is macOS 11; — wenzelm / hgweb
  4. more robust: always assume x86_64 (or its emulation on ARM); — wenzelm / hgweb
  5. MLton lacks arm64-linux (see also 84f2d481d6d7); — wenzelm / hgweb
  6. more ambitious test "AFP (macOS 14 Sonoma, Apple Silicon)", as replacement for AFP on lrzcloud2; — wenzelm / hgweb
  7. update to stack-2.15.3, stackage-lts-22.6, ghc-9.6.4; — wenzelm / hgweb
  8. tuned; — wenzelm / hgweb
  9. merged — wenzelm / hgweb
  10. misc updates, tuning and clarification; — wenzelm / hgweb
  11. reformat source in jEdit (wrap margin 78); — wenzelm / hgweb
  12. more accurate Markdown formatting, both for VSCode and Phabricator; — wenzelm / hgweb
  13. just one README.md; — wenzelm / hgweb

#1008 (Mar 25, 2024, 9:39:07 PM)

  1. added lemma wf_on_iff_wf — desharna / hgweb
  2. changed number of consumed assumptions of wf_on_induct and wfp_on_induct — desharna / hgweb
  3. tuned — nipkow / hgweb
  4. merged — wenzelm / hgweb
  5. more accurate platform directories: pkg/tool structure is hardwired in "go"; — wenzelm / hgweb
  6. support for etc/platform.props, to specify multi-platform directory structure more accurately; — wenzelm / hgweb
  7. clarified signature; — wenzelm / hgweb
  8. tuned; — wenzelm / hgweb
  9. clarified modules; — wenzelm / hgweb
  10. clarified modules; — wenzelm / hgweb
  11. build Isabelle component for Go: all platforms; — wenzelm / hgweb
  12. misc tuning; — wenzelm / hgweb
  13. just one copy of darwin-universal.tar.gz; — wenzelm / hgweb
  14. documented running time function framework by Jonas Stahl — nipkow / hgweb
  15. merged — desharna / hgweb
  16. merged — nipkow / hgweb
  17. more uniform command names — nipkow / hgweb
  18. tuned parameter order — nipkow / hgweb
  19. shutdown lrzcloud2; — wenzelm / hgweb

#1007 (Mar 24, 2024, 9:45:07 AM)

  1. redefined wf as an abbreviation for "wf_on UNIV" — desharna / hgweb

#1006 (Mar 23, 2024, 6:57:06 PM)

  1. redefined wf as an abbreviation for "wf_on UNIV" — desharna / hgweb

#1005 (Mar 23, 2024, 4:48:11 PM)

  1. tuned NEWS — desharna / hgweb

#1004 (Mar 22, 2024, 11:00:07 AM)

  1. redefined wfP as an abbreviation for "wfp_on UNIV" — desharna / hgweb
  2. merged — desharna / hgweb
  3. merged — wenzelm / hgweb
  4. suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
    clarified NEWS; — wenzelm / hgweb
  5. update to sumatra_pdf-3.5.2; — wenzelm / hgweb
  6. tuned signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
  7. update to jsoup-1.17.2; — wenzelm / hgweb
  8. proper bib entries (amending 82aaa0d8fc3b); — wenzelm / hgweb
  9. update to dotnet-8.0.203; — wenzelm / hgweb
  10. enforce rebuild of Isabelle/ML; — wenzelm / hgweb
  11. update to sqlite-3.45.2.0: clarified component name, following postgresql; — wenzelm / hgweb
  12. activate postgresql-42.7.3; — wenzelm / hgweb
  13. update to postgresql-42.7.3;
    clarified component directory; — wenzelm / hgweb
  14. update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64-darwin; — wenzelm / hgweb
  15. isabelle update -u cite; — wenzelm / hgweb
  16. raise error if benchmarking fails; — Fabian Huch <huch@in.tum.de> / hgweb
  17. option for benchmark session; — Fabian Huch <huch@in.tum.de> / hgweb
  18. add hosts option to run benchmark on the cluster from the command-line; — Fabian Huch <huch@in.tum.de> / hgweb
  19. only start jobs early if they are due (cf. 1966578feff8); — Fabian Huch <huch@in.tum.de> / hgweb
  20. New material from a variety of sources (including AFP) — paulson <lp15@cam.ac.uk> / hgweb
  21. build component for cvc5-latest (ef2bc3f735df); — wenzelm / hgweb

#1003 (Mar 22, 2024, 9:27:11 AM)

  1. redefined wfP as an abbreviation for "wfp_on UNIV" — desharna / hgweb

#1002 (Mar 21, 2024, 11:27:08 AM)

  1. redefined wfP as an abbreviation for "wfp_on UNIV" — desharna / hgweb

#1001 (Mar 20, 2024, 9:15:10 PM)

  1. added lemma wellorder.wfp_on_less[simp] — desharna / hgweb
  2. merged — desharna / hgweb
  3. HOL-Library: added modulo/congruence for real numbers — Manuel Eberl <eberlm@in.tum.de> / hgweb
  4. only print schedule if relevant; — Fabian Huch <huch@in.tum.de> / hgweb
  5. remove laziness: no need, and errors during initialization loop with close(); — Fabian Huch <huch@in.tum.de> / hgweb
  6. more general definition of meromorphicity; Weierstraß factorisation theorem — Manuel Eberl <eberlm@in.tum.de> / hgweb
  7. always provide build_database_server option in benchmark command; — Fabian Huch <huch@in.tum.de> / hgweb
  8. always check if node is defined, e.g. for exists_next operation wit empty schedule; — Fabian Huch <huch@in.tum.de> / hgweb

#1000 (Mar 20, 2024, 2:32:48 PM)

  1. try proof method "order" in Sledgehammer's proof reconstruction — desharna / hgweb
  2. added Mirabelle action "order" — desharna / hgweb
  3. renamed lemma antisymp_on_reflcp to antisymp_on_reflclp — desharna / hgweb
  4. tuned proof — desharna / hgweb