Changes
#1019 (Apr 11, 2024, 2:15:11 PM)
- tweaked time functions for median-of-medians selection in HOL-Data_Structures — Manuel Eberl <manuel@pruvisto.org> / hgweb
- merged — wenzelm / hgweb
- rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta; — wenzelm / hgweb
- Tiny tweaks to proofs — paulson <lp15@cam.ac.uk> / hgweb
- A bit of new material about type class "infinite", from Eval_FO — paulson <lp15@cam.ac.uk> / hgweb
- avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax; — wenzelm / hgweb
- proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...); — wenzelm / hgweb
- adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested; — wenzelm / hgweb
- Add entry on Sketch_and_Explore to CONTRIBUTORS — Simon Wimmer <wimmers@in.tum.de> / hgweb
- moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory — Manuel Eberl <manuel@pruvisto.org> / hgweb
- more portable: prefer official JDBC operation DatabaseMetaData.getColumns(); — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
#1018 (Apr 4, 2024, 3:30:29 PM)
- moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory — Manuel Eberl <manuel@pruvisto.org> / hgweb
- documented new syntax for fBall and fBex — desharna / hgweb
- updated for release; — wenzelm / hgweb
- Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 — wenzelm / hgweb
- misc tuning for release; — wenzelm / hgweb
- update for release; — wenzelm / hgweb
- merged — wenzelm / hgweb
- update to stack-2.15.5, stackage-lts-22.15; — wenzelm / hgweb
- clarified names: discontinue odd convention from 3 decades ago; — wenzelm / hgweb
- 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
- added documentation for meromorphicity etc. in HOL-Complex_Analysis — Manuel Eberl <manuel@pruvisto.org> / hgweb
- merged — desharna / hgweb
- remove transitional (dummy) component list for Go — Lars Hupel <lars@hupel.info> / hgweb
#1017 (Apr 2, 2024, 8:36:08 AM)
- merged — desharna / hgweb
- clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code; — wenzelm / hgweb
- 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 - provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version; — wenzelm / hgweb
- clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that "very_slow" is normally used together with "slow"; — wenzelm / hgweb
- moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields — Manuel Eberl <eberlm@in.tum.de> / hgweb
- update NEWS; — Fabian Huch <huch@in.tum.de> / hgweb
- moved web_app module from AFP (e.g., for building web services for the distributed build); — Fabian Huch <huch@in.tum.de> / hgweb
- added special syntax for FSet.Ball and FSet.Bex — desharna / hgweb
- tuned proof — desharna / hgweb
- tuned proofs of Equiv_Relations.equiv — desharna / hgweb
#1016 (Mar 29, 2024, 7:30:12 PM)
- moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields — Manuel Eberl <eberlm@in.tum.de> / hgweb
- tuned; — Fabian Huch <huch@in.tum.de> / hgweb
- removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML); — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- clarified modules: more official Sessions.notable_groups; — wenzelm / hgweb
- tuned — nipkow / hgweb
- merged — paulson / hgweb
- An assortment of new material, mostly due to Manuel — paulson <lp15@cam.ac.uk> / hgweb
#1015 (Mar 28, 2024, 3:24:23 PM)
- test — wenzelm / hgweb
- 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 - tuned signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned signature; — wenzelm / hgweb
#1014 (Mar 28, 2024, 1:39:38 PM)
#1013 (Mar 28, 2024, 8:33:11 AM)
- tuned proofs of Equiv_Relations.equiv — desharna / hgweb
- merged — desharna / hgweb
- proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests; — wenzelm / hgweb
- proper "isabelle go_setup" for Jenkins; — wenzelm / hgweb
- added lemma wfp_on_image and author name to theory — desharna / hgweb
#1012 (Mar 27, 2024, 10:09:08 PM)
- proper "isabelle go_setup" for Jenkins; — wenzelm / hgweb
- dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24); — wenzelm / hgweb
- tuned message; — wenzelm / hgweb
- merged — wenzelm / hgweb
- merged — nipkow / hgweb
- updated time functions for Array_Braun — nipkow / hgweb
- merged — paulson / hgweb
- New material and a bit of refactoring — paulson <lp15@cam.ac.uk> / hgweb
- tuned NEWS; — wenzelm / hgweb
- support for "all" platforms; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and 37f852399a32); — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- more robust Markdown; — wenzelm / hgweb
- misc tuning;
more text; — wenzelm / hgweb - run "isabelle components_build -u"; — wenzelm / hgweb
- remove obsolete component (see 8347ffa1f92c): superseded by "isabelle go_setup"; — wenzelm / hgweb
- tuned order; — wenzelm / hgweb
- more Setup_Tool services; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- proper SSH operations; — wenzelm / hgweb
- tuned signature: more permissive; — wenzelm / hgweb
- clarified signature: explicit variable is easier to find in source; — wenzelm / hgweb
- proper services for Setup_Tool --- avoid hardwired stuff; — wenzelm / hgweb
#1011 (Mar 27, 2024, 11:51:11 AM)
- added lemma wfp_on_image and author name to theory — desharna / hgweb
- merged — desharna / hgweb
- more robust XML body: allow empty text, as well as arbitrary pro-forma markup (e.g. see XML.blob in Isabelle/ML); — wenzelm / hgweb
- more robust: untyped/unscoped markup elements need to reside in module Markup for minimal static checking (see also 11a1f4d7af51); — wenzelm / hgweb
- misc tuning for release; — wenzelm / hgweb
- merged; — wenzelm / hgweb
- NEWS for "isabelle go_setup"; — wenzelm / hgweb
- proper platform_path for Windows; — wenzelm / hgweb
- misc tuning, following go_setup; — wenzelm / hgweb
- dynamic setup of Go component, similar to Dotnet; — wenzelm / hgweb
- tuned comments; — wenzelm / hgweb
- clarified signature: more operations; — wenzelm / hgweb
- clarified signature: explicit type Platform.Info with derived operations; — wenzelm / hgweb
- less ambitious parallelism: avoid exhaustion of memory (64GB total); — wenzelm / hgweb
- provide ISABELLE_DOTNET_VERSION via settings, following "isabelle ghc_setup"; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- tuned messages; — wenzelm / hgweb
- update to bash_process-20240326; — wenzelm / hgweb
- build bash_process in Isabelle/Scala, with etc/platforms.prop to preserve all platform directories (e.g. for SSH upload); — wenzelm / hgweb
- clarified meaning of platform.props: update on default; — wenzelm / hgweb
- 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)
#1009 (Mar 26, 2024, 9:33:11 AM)
- added lemmas wfp_on_inv_imagep, wfp_on_if_convertible_to_wfp_on, and wf_on_if_convertible_to_wf_on — desharna / hgweb
- merged — desharna / hgweb
- obsolete: base-line is macOS 11; — wenzelm / hgweb
- more robust: always assume x86_64 (or its emulation on ARM); — wenzelm / hgweb
- MLton lacks arm64-linux (see also 84f2d481d6d7); — wenzelm / hgweb
- more ambitious test "AFP (macOS 14 Sonoma, Apple Silicon)", as replacement for AFP on lrzcloud2; — wenzelm / hgweb
- update to stack-2.15.3, stackage-lts-22.6, ghc-9.6.4; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- merged — wenzelm / hgweb
- misc updates, tuning and clarification; — wenzelm / hgweb
- reformat source in jEdit (wrap margin 78); — wenzelm / hgweb
- more accurate Markdown formatting, both for VSCode and Phabricator; — wenzelm / hgweb
- just one README.md; — wenzelm / hgweb
#1008 (Mar 25, 2024, 9:39:07 PM)
- added lemma wf_on_iff_wf — desharna / hgweb
- changed number of consumed assumptions of wf_on_induct and wfp_on_induct — desharna / hgweb
- tuned — nipkow / hgweb
- merged — wenzelm / hgweb
- more accurate platform directories: pkg/tool structure is hardwired in "go"; — wenzelm / hgweb
- support for etc/platform.props, to specify multi-platform directory structure more accurately; — wenzelm / hgweb
- clarified signature; — wenzelm / hgweb
- tuned; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- clarified modules; — wenzelm / hgweb
- build Isabelle component for Go: all platforms; — wenzelm / hgweb
- misc tuning; — wenzelm / hgweb
- just one copy of darwin-universal.tar.gz; — wenzelm / hgweb
- documented running time function framework by Jonas Stahl — nipkow / hgweb
- merged — desharna / hgweb
- merged — nipkow / hgweb
- more uniform command names — nipkow / hgweb
- tuned parameter order — nipkow / hgweb
- shutdown lrzcloud2; — wenzelm / hgweb
#1007 (Mar 24, 2024, 9:45:07 AM)
#1006 (Mar 23, 2024, 6:57:06 PM)
#1005 (Mar 23, 2024, 4:48:11 PM)
#1004 (Mar 22, 2024, 11:00:07 AM)
- redefined wfP as an abbreviation for "wfp_on UNIV" — desharna / hgweb
- merged — desharna / hgweb
- merged — wenzelm / hgweb
- suppress arm64-darwin, which does not support "-codegen native" (required for AFP/PAC_Checker);
clarified NEWS; — wenzelm / hgweb - update to sumatra_pdf-3.5.2; — wenzelm / hgweb
- tuned signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
- update to jsoup-1.17.2; — wenzelm / hgweb
- proper bib entries (amending 82aaa0d8fc3b); — wenzelm / hgweb
- update to dotnet-8.0.203; — wenzelm / hgweb
- enforce rebuild of Isabelle/ML; — wenzelm / hgweb
- update to sqlite-3.45.2.0: clarified component name, following postgresql; — wenzelm / hgweb
- activate postgresql-42.7.3; — wenzelm / hgweb
- update to postgresql-42.7.3;
clarified component directory; — wenzelm / hgweb - update to mlton-20210117-2, which covers x86_64-linux, x86_64-darwin, arm64-darwin; — wenzelm / hgweb
- isabelle update -u cite; — wenzelm / hgweb
- raise error if benchmarking fails; — Fabian Huch <huch@in.tum.de> / hgweb
- option for benchmark session; — Fabian Huch <huch@in.tum.de> / hgweb
- add hosts option to run benchmark on the cluster from the command-line; — Fabian Huch <huch@in.tum.de> / hgweb
- only start jobs early if they are due (cf. 1966578feff8); — Fabian Huch <huch@in.tum.de> / hgweb
- New material from a variety of sources (including AFP) — paulson <lp15@cam.ac.uk> / hgweb
- build component for cvc5-latest (ef2bc3f735df); — wenzelm / hgweb
#1003 (Mar 22, 2024, 9:27:11 AM)
#1002 (Mar 21, 2024, 11:27:08 AM)
#1001 (Mar 20, 2024, 9:15:10 PM)
- added lemma wellorder.wfp_on_less[simp] — desharna / hgweb
- merged — desharna / hgweb
- HOL-Library: added modulo/congruence for real numbers — Manuel Eberl <eberlm@in.tum.de> / hgweb
- only print schedule if relevant; — Fabian Huch <huch@in.tum.de> / hgweb
- remove laziness: no need, and errors during initialization loop with close(); — Fabian Huch <huch@in.tum.de> / hgweb
- more general definition of meromorphicity; Weierstraß factorisation theorem — Manuel Eberl <eberlm@in.tum.de> / hgweb
- always provide build_database_server option in benchmark command; — Fabian Huch <huch@in.tum.de> / hgweb
- always check if node is defined, e.g. for exists_next operation wit empty schedule; — Fabian Huch <huch@in.tum.de> / hgweb