Changes

#2214 (Jun 26, 2024, 12:50:11 AM)

1. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
2. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
3. add root entry for non-local components; — Fabian Huch <huch@in.tum.de> / hgweb
4. clarified; — Fabian Huch <huch@in.tum.de> / hgweb
5. extra timer delay, to limit db transactions; — Fabian Huch <huch@in.tum.de> / hgweb
6. proper synchronized; — Fabian Huch <huch@in.tum.de> / hgweb
7. clarified ternary tries — nipkow / hgweb

#2213 (Jun 25, 2024, 12:50:12 AM)

1. clarified test parameters; — wenzelm / hgweb

#2212 (Jun 23, 2024, 12:50:07 AM)

1. more tests: Windows + AFP (see also 1fd5f96e1da3); — wenzelm / hgweb

#2211 (Jun 21, 2024, 12:50:10 AM)

1. dropped references to theorems from transitional theory Divides.thy — haftmann / hgweb

#2210 (Jun 20, 2024, 12:50:06 AM)

1. Tidied some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
2. Updated some archaic proofs — paulson <lp15@cam.ac.uk> / hgweb

#2209 (Jun 19, 2024, 12:50:08 AM)

1. tuned def: patter matching needs more beautification — nipkow / hgweb

#2208 (Jun 18, 2024, 12:50:09 AM)

1. removed lemma wellorder.wfP_less — desharna / hgweb

#2207 (Jun 17, 2024, 3:35:25 AM)

1. merged — wenzelm / hgweb
2. enforce rebuild of Isabelle/ML; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String); — wenzelm / hgweb
5. tuned: prefer Bytes operations; — wenzelm / hgweb
6. unused; — wenzelm / hgweb
7. proper treatment of long message blocks; — wenzelm / hgweb
8. clarified sizes; — wenzelm / hgweb
9. more scalable stream read operations; — wenzelm / hgweb
10. minor performance tuning; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. tuned module structure; — wenzelm / hgweb
13. tuned names; — wenzelm / hgweb
14. imitate internal policy of ByteArrayOutputStream: capacity is doubled after first push; — wenzelm / hgweb
15. tuned whitespace; — wenzelm / hgweb
16. unused; — wenzelm / hgweb
17. Bytes.Builder is unsynchronized, like java.io.OutputBuffer; — wenzelm / hgweb
18. notable performance tuning: avoid overhead of higher-order functions; — wenzelm / hgweb
19. more efficient equals: avoid somewhat slow sha1_digest (see also 29b761e290c5, 306f273c91ec); — wenzelm / hgweb
20. more scalable compression, using Bytes.Builder.Stream; — wenzelm / hgweb
21. tuned: more uniform, less ambitious; — wenzelm / hgweb
22. tuned; — wenzelm / hgweb
23. minor performance tuning; — wenzelm / hgweb
24. minor performance tuning;
    clarified signature; — wenzelm / hgweb
25. minor performance tuning; — wenzelm / hgweb
26. clarified signature; — wenzelm / hgweb
27. tuned; — wenzelm / hgweb
28. tuned; — wenzelm / hgweb
29. clarified signature; — wenzelm / hgweb
30. minor performance tuning; — wenzelm / hgweb
31. support large byte arrays, using multiple "chunks";
    support incremental builder;
    clarified "limit" (valid >= 0) vs. "hint" (valid > 0);
    clarified byte access: prefer unchecked acces and iterators internally; — wenzelm / hgweb
32. clarified File.eq_content, following 306f273c91ec; — wenzelm / hgweb
33. tuned; — wenzelm / hgweb
34. clarified hash and equality: depend on sha1 digest to be collision-free; — wenzelm / hgweb
35. clarified signature; — wenzelm / hgweb
36. tuned source structure; — wenzelm / hgweb
37. tuned signature; — wenzelm / hgweb
38. minor performance tuning; — wenzelm / hgweb
39. proper sha1_digest: need to include offset + length; — wenzelm / hgweb
40. clarified signature: pro-forma support for Bytes with size: Long; — wenzelm / hgweb
41. minor performance tuning; — wenzelm / hgweb
42. clarified signature (again); — wenzelm / hgweb
43. tuned; — wenzelm / hgweb
44. clarified signature: discontinue somewhat misleading Bytes <: CharSequence; — wenzelm / hgweb
45. minor performance tuning; — wenzelm / hgweb
46. clarified signature: more accurate types; — wenzelm / hgweb
47. clarified signature; — wenzelm / hgweb

#2206 (Jun 15, 2024, 12:50:10 AM)

1. tuned messages; — Fabian Huch <huch@in.tum.de> / hgweb
2. clarified web server paths; — Fabian Huch <huch@in.tum.de> / hgweb

#2205 (Jun 12, 2024, 4:30:54 AM)

1. sort web app parameters in list; — Fabian Huch <huch@in.tum.de> / hgweb
2. proper available hosts; — Fabian Huch <huch@in.tum.de> / hgweb
3. tuned proof — desharna / hgweb
4. tuned comments; — Fabian Huch <huch@in.tum.de> / hgweb
5. add build_manager_database tool to restore db from log files; — Fabian Huch <huch@in.tum.de> / hgweb
6. use build log in build manager to store meta-data persistently; — Fabian Huch <huch@in.tum.de> / hgweb
7. add build log format for managed builds; — Fabian Huch <huch@in.tum.de> / hgweb
8. improve build manager log (for build_log); — Fabian Huch <huch@in.tum.de> / hgweb
9. clarified; — Fabian Huch <huch@in.tum.de> / hgweb
10. proper web server address; — Fabian Huch <huch@in.tum.de> / hgweb
11. clarified names: more canonical; — Fabian Huch <huch@in.tum.de> / hgweb
12. clarified; — Fabian Huch <huch@in.tum.de> / hgweb
13. remove unused; — Fabian Huch <huch@in.tum.de> / hgweb
14. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
15. fixed NEWS — desharna / hgweb

#2204 (Jun 11, 2024, 5:19:04 AM)

1. merged — wenzelm / hgweb
2. tuned signature: more exports; — wenzelm / hgweb
3. clarified signature: prefer internal Thm_Name.T over external Facts.ref; — wenzelm / hgweb
4. more robust / permissive; — wenzelm / hgweb
5. clarified signature: more operations; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. clarified operations, following pretty_thm_name; — wenzelm / hgweb
8. more accurate treatment of Thm_Name.T; — wenzelm / hgweb
9. renamed lemmas — desharna / hgweb
10. merged — desharna / hgweb
11. renamed theorems — desharna / hgweb
12. renamed theorems — desharna / hgweb
13. add title; — Fabian Huch <huch@in.tum.de> / hgweb
14. use build_cluster in ci builds; — Fabian Huch <huch@in.tum.de> / hgweb
15. merged — desharna / hgweb
16. tuned alias names in formulas — desharna / hgweb
17. renamed theorems — desharna / hgweb
18. add favicon to web app; — Fabian Huch <huch@in.tum.de> / hgweb

#2203 (Jun 10, 2024, 4:02:22 AM)

1. merged — wenzelm / hgweb
2. clarified data representation: prefer explicit type Thm_Name; — wenzelm / hgweb
3. more operations, following Isabelle/ML; — wenzelm / hgweb
4. clarified signature: more explicit operations; — wenzelm / hgweb
5. clarified treatment of Thm_Name.T (again, see also 8a9588ffc133); — wenzelm / hgweb
6. clarified operations, including exceptions; — wenzelm / hgweb
7. tuned: more direct Isabelle/ML; — wenzelm / hgweb
8. clarified modules; — wenzelm / hgweb
9. more accurate thm "name_hint", using Thm_Name.T; — wenzelm / hgweb
10. more operationsd; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms); — wenzelm / hgweb
13. clarified signature; — wenzelm / hgweb
14. clarified output, following Consumer_Thread.failure; — wenzelm / hgweb
15. more informative exception output, with optional trace; — wenzelm / hgweb
16. more accurate output of Thm_Name.T wrt. facts name space; — wenzelm / hgweb
17. clarified signature: more operations; — wenzelm / hgweb
18. tuned structure; — wenzelm / hgweb
19. tuned; — wenzelm / hgweb
20. more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name; — wenzelm / hgweb
21. clarified signature: prefer explicit operation; — wenzelm / hgweb
22. clarified signature; — wenzelm / hgweb
23. tuned: prefer Thm_Name operations; — wenzelm / hgweb
24. tuned; — wenzelm / hgweb
25. prefer dynamic position from command transaction; — wenzelm / hgweb
26. tuned signature; — wenzelm / hgweb
27. clarified signature: more explicit preprocessing; — wenzelm / hgweb
28. clarified signature: separate formal context from exported theory_name; — wenzelm / hgweb
29. tuned signature: just one ZThm is sufficient; — wenzelm / hgweb

#2202 (Jun 9, 2024, 12:50:09 AM)

1. renamed lemmas — desharna / hgweb
2. build manager: echo error messages to server output; — Fabian Huch <huch@in.tum.de> / hgweb
3. omit showing previous failures for user builds; — Fabian Huch <huch@in.tum.de> / hgweb
4. always handle interrupted jobs; — Fabian Huch <huch@in.tum.de> / hgweb
5. add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware; — Fabian Huch <huch@in.tum.de> / hgweb
6. clarified context: operations now in build process; — Fabian Huch <huch@in.tum.de> / hgweb
7. clarified: add explicit build process; — Fabian Huch <huch@in.tum.de> / hgweb
8. remove unnecessary subdir; — Fabian Huch <huch@in.tum.de> / hgweb
9. tuned; — Fabian Huch <huch@in.tum.de> / hgweb

#2201 (Jun 7, 2024, 2:44:34 AM)

1. tuned proof: avoid smt/z3 to make this work with arm64-linux; — wenzelm / hgweb
2. proper afp_directory (amending 9308bc5f65d6); — wenzelm / hgweb
3. clarified names; — wenzelm / hgweb
4. clarified name: avoid clash with Library.Update; — wenzelm / hgweb
5. clarified signature; — wenzelm / hgweb
6. tuned whitespace; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. merged — wenzelm / hgweb
9. more informative ZBox; — wenzelm / hgweb
10. more operations; — wenzelm / hgweb
11. tuned signature; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb
14. remove unused (see also 04214caeb9ac); — wenzelm / hgweb
15. tuned signature; — wenzelm / hgweb
16. add triggers to ci jobs: on commit vs timed; — Fabian Huch <huch@in.tum.de> / hgweb
17. manage components of ci builds; — Fabian Huch <huch@in.tum.de> / hgweb
18. use external CSS for build manager page; — Fabian Huch <huch@in.tum.de> / hgweb
19. more build manager page; — Fabian Huch <huch@in.tum.de> / hgweb
20. more page elements; — Fabian Huch <huch@in.tum.de> / hgweb
21. web app: add automatic resize; — Fabian Huch <huch@in.tum.de> / hgweb
22. ensure permissions when starting build task (e.g., due to misconfigured client); — Fabian Huch <huch@in.tum.de> / hgweb
23. add verbose option to build_task; — Fabian Huch <huch@in.tum.de> / hgweb

#2200 (Jun 6, 2024, 12:50:07 AM)

1. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
2. build manager: manage directories/permissions, to minimize local administration; — Fabian Huch <huch@in.tum.de> / hgweb

#2199 (Jun 5, 2024, 12:50:08 AM)

1. read prefs properly; — Fabian Huch <huch@in.tum.de> / hgweb
2. allow explicit Isabelle rev in build task (e.g., for older Isabelle versions); — Fabian Huch <huch@in.tum.de> / hgweb
3. web app: proper document height; — Fabian Huch <huch@in.tum.de> / hgweb
4. merged — nipkow / hgweb
5. replace manual def. of timing function — nipkow / hgweb
6. add build manager module; — Fabian Huch <huch@in.tum.de> / hgweb
7. support ci job via hg_sync (cf. 7883f221d6d3); — Fabian Huch <huch@in.tum.de> / hgweb
8. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
9. use Content-Digest header in HEAD requests instead of length (to track non-monotone changes); — Fabian Huch <huch@in.tum.de> / hgweb

#2198 (Jun 4, 2024, 2:53:29 AM)

1. merged — paulson / hgweb
2. Simplification of sin, cos, exp of multiples of pi — paulson <lp15@cam.ac.uk> / hgweb
3. minor performance tuning: more compact data; — wenzelm / hgweb
4. removed unused/inefficient size_of_proof (see also 2241191a3c54); — wenzelm / hgweb

#2197 (Jun 3, 2024, 12:50:45 AM)

1. tuned; — wenzelm / hgweb
2. more robust: avoid crash of sleep() for negative time; — wenzelm / hgweb

#2196 (Jun 2, 2024, 12:50:40 AM)

1. clarified signature; — wenzelm / hgweb
2. clarified signature: more explicit types; — wenzelm / hgweb
3. support "rsync --chmod --chown" via Rsync.Context; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. bash: proper bash_process via SSH;
   getenv: prefer light-weight ssh.execute; — wenzelm / hgweb
6. clarified signature: support explicit cwd; — wenzelm / hgweb
7. support bash via SSH; — wenzelm / hgweb
8. clarified comments; — wenzelm / hgweb
9. proper support for remote cwd; — wenzelm / hgweb
10. clarified context for (remote) bash scripts: export variables are optional, support cwd; — wenzelm / hgweb
11. more operations for SSH.System: bash_process and bash; — wenzelm / hgweb
12. unused; — wenzelm / hgweb
13. clarified signature: prefer symbolic isabelle.Path over physical java.io.File; — wenzelm / hgweb

#2195 (Jun 1, 2024, 12:50:41 AM)

1. minor performance tuning; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. minor performance tuning: save approx. 70ms per SSH command; — wenzelm / hgweb
4. minor performance tuning: save approx. 70ms per SSH command; — wenzelm / hgweb
5. minor performance tuning: save approx. 70ms per SSH test command; — wenzelm / hgweb
6. suport Isabelle_System.bash via SSH.System; — wenzelm / hgweb
7. more operations; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. clarified signature; — wenzelm / hgweb
10. clarified signature; — wenzelm / hgweb
11. obsolete: macOS 10.x is no longer supported (see also 059743bc8311); — wenzelm / hgweb
12. tuned tmp name; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. tuned; — wenzelm / hgweb
15. tuned comments; — wenzelm / hgweb

#2194 (May 30, 2024, 12:50:43 AM)

1. merged — nipkow / hgweb
2. pretty-printing sledgehammer command: merge indexed theorems — nipkow / hgweb
3. clarify routes: absolute in api and relative for frontend; — Fabian Huch <huch@in.tum.de> / hgweb
4. add auto-reload for more interactive web apps; — Fabian Huch <huch@in.tum.de> / hgweb
5. clarified web app endpoints; — Fabian Huch <huch@in.tum.de> / hgweb
6. proper html script tag: source code must not be escaped; — Fabian Huch <huch@in.tum.de> / hgweb
7. add explicit Content-Length header to http response (otherwise it is missing in HEAD responses); — Fabian Huch <huch@in.tum.de> / hgweb
8. add HEAD to http server: should send same header fields as if request was GET; — Fabian Huch <huch@in.tum.de> / hgweb

#2193 (May 26, 2024, 12:50:39 AM)

1. tuned; — wenzelm / hgweb
2. tuned spelling; — wenzelm / hgweb
3. support direct rsync from Hg_Sync result directory (usually requires option -d "~~/dirs"); — wenzelm / hgweb
4. clarified signature; — wenzelm / hgweb
5. more general dirs for Sync.sync; — wenzelm / hgweb
6. tuned whitespace (amending beb4ee344c22); — wenzelm / hgweb
7. clarified signature (see also be0ab4b94c62 and c41791ad75c3); — wenzelm / hgweb

#2192 (May 25, 2024, 12:50:40 AM)

1. tuned; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. tuned names; — wenzelm / hgweb
4. proper SSH.System operation; — wenzelm / hgweb
5. clarified modules; — wenzelm / hgweb
6. more uniform/robust detect_repository/is_repository: actually check hg root; — wenzelm / hgweb
7. more uniform local/remote operations; — wenzelm / hgweb

#2191 (May 24, 2024, 12:50:06 AM)

1. disable Isabelle/Naproche after release; — wenzelm / hgweb
2. post-release updates; — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. Added tag Isabelle2024 for changeset 29f2b8ff84f3 — wenzelm / hgweb
5. proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f); — wenzelm / hgweb
6. provide scala-3.4.2, but do not activate it: scala-3.3.x is LTS version; — wenzelm / hgweb
7. update to naproche-20240519; — wenzelm / hgweb
8. proper formatting; — wenzelm / hgweb
9. more documentation on "isabelle build -H" and underlying system registry tables "host" and "cluster"; — wenzelm / hgweb

#2190 (May 14, 2024, 4:56:03 AM)

1. More binomial material — paulson <lp15@cam.ac.uk> / hgweb
2. syntax of gchoose now the same as choose — paulson <lp15@cam.ac.uk> / hgweb
3. Some new simprules – and patches for proofs — paulson <lp15@cam.ac.uk> / hgweb
4. merged — paulson / hgweb
5. merged — paulson / hgweb
6. A little more tidying in Nominal — paulson <lp15@cam.ac.uk> / hgweb

#2189 (May 3, 2024, 12:57:51 AM)

1. tuned proofs;
   tuned whitespace; — wenzelm / hgweb
2. merged, resoving conflicts in src/HOL/Nominal/Nominal.thy; — wenzelm / hgweb
3. Added tag Isabelle2024-RC3 for changeset 007e6af8a020 — wenzelm / hgweb
4. more documentation on "System registry via TOML"; — wenzelm / hgweb
5. update to naproche-20240502: proper platform_path for NAPROCHE_FORMALIZATIONS to make it work on Windows; — wenzelm / hgweb
6. provide 3.1 for testing (inactive); — wenzelm / hgweb
7. build e-3.1, without patch; — wenzelm / hgweb
8. disable Isabelle/Naproche for now: does not quite work on Windows; — wenzelm / hgweb
9. update and activate naproche component for release; — wenzelm / hgweb
10. changed URL to SystemOnTPTP at Geoff's request — desharna / hgweb
11. tuned spelling; — wenzelm / hgweb
12. build_cluster always uses build_database_server for now -- despite 1fa1b32b0379: its local/remote storage model often leads to incoherent state; — wenzelm / hgweb
13. proper directory permissions to make "rm" work, notably for cygwin/etc/pki/ca-trust/extracted/pem/directory-hash; — wenzelm / hgweb
14. support more Ubuntu versions; — wenzelm / hgweb
15. updated for release; — wenzelm / hgweb
16. more robust: avoid spurious ConcurrentModificationException; — wenzelm / hgweb
17. update to e-3.0.03-1, with proper support for trivial statements; — wenzelm / hgweb
18. more robust; — wenzelm / hgweb
19. minor patch for E Prover, based on "git diff -w -r E-3.0.03 E-3.0.08": proper support for trivial statements; — wenzelm / hgweb
20. backed out changeset 601ff5c7cad5: not relevant for Isabelle2024; — wenzelm / hgweb
21. clone of 0c51e0a6bc37; — wenzelm / hgweb

#2188 (Apr 27, 2024, 12:50:10 AM)

1. update Windows test machines; — wenzelm / hgweb

#2187 (Apr 25, 2024, 12:50:08 AM)

1. More tidying of proofs — paulson <lp15@cam.ac.uk> / hgweb
2. Another Nominal example — paulson <lp15@cam.ac.uk> / hgweb
3. merged — paulson / hgweb
4. Tidying up another Nominal example (SOS) — paulson <lp15@cam.ac.uk> / hgweb

#2186 (Apr 24, 2024, 12:50:11 AM)

1. update Windows build host; — wenzelm / hgweb
2. proper command-line; — wenzelm / hgweb
3. Tidying up another of the nominal examples — paulson <lp15@cam.ac.uk> / hgweb

#2185 (Apr 23, 2024, 12:50:07 AM)

1. More tidying of Nominal proofs — paulson <lp15@cam.ac.uk> / hgweb
2. Tidied up another messy theory — paulson <lp15@cam.ac.uk> / hgweb

#2184 (Apr 22, 2024, 12:50:08 AM)

1. More proof tidying for Nominal — paulson <lp15@cam.ac.uk> / hgweb

#2183 (Apr 21, 2024, 12:50:13 AM)

1. Tidying up more messy proofs — paulson <lp15@cam.ac.uk> / hgweb
2. Starting to tidy HOL-Nominal-Examples — paulson <lp15@cam.ac.uk> / hgweb

#2182 (Apr 19, 2024, 12:50:11 AM)

1. sketch & explore: recover from duplicate fixed variables in Isar proofs — Simon Wimmer <wimmers@in.tum.de> / hgweb
2. back to post-release mode -- after fork point; — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. Added tag Isabelle2024-RC2 for changeset ef2134570abb — wenzelm / hgweb
5. Acknowledgement of Ata Keskin for his Martingales material — paulson <lp15@cam.ac.uk> / hgweb

#2181 (Apr 18, 2024, 4:33:28 AM)

1. merged — wenzelm / hgweb
2. update to jdk-21.0.3;
   enforce rebuild of Isabelle/ML and Isabelle/Scala; — wenzelm / hgweb
3. merged — paulson / hgweb
4. Tidied up horrible archaic proofs — paulson <lp15@cam.ac.uk> / hgweb
5. clarified signature; — wenzelm / hgweb
6. make adhoc_overloading respect type constraints — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb

#2180 (Apr 17, 2024, 12:50:08 AM)

1. merged — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. minor performance tuning: avoid redundant server access; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. clarified modules and options (from store); — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. clarified signature; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. tuned signature; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. tuned; — wenzelm / hgweb
15. more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4); — wenzelm / hgweb
16. tuned messages; — wenzelm / hgweb
17. tuned; — wenzelm / hgweb
18. back to static numa_nodes (reverting part of c2c59de57df9); — wenzelm / hgweb
19. tuned messages; — wenzelm / hgweb
20. canonical time function for List.nth — Manuel Eberl <eberlm@in.tum.de> / hgweb

#2179 (Apr 16, 2024, 12:50:10 AM)

1. merged — paulson / hgweb
2. Streamlining of many more archaic proofs — paulson <lp15@cam.ac.uk> / hgweb
3. clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces); — Fabian Huch <huch@in.tum.de> / hgweb

#2178 (Apr 15, 2024, 12:50:10 AM)

1. More tidying of old proofs — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. More tidying and removal of "apply" — paulson <lp15@cam.ac.uk> / hgweb

#2177 (Apr 14, 2024, 12:50:10 AM)

1. Add subgoals variant of 'sketch' command — Simon Wimmer <wimmers@in.tum.de> / hgweb

#2176 (Apr 13, 2024, 12:50:11 AM)

1. merged — paulson / hgweb
2. Tidied some messy proofs — paulson <lp15@cam.ac.uk> / hgweb
3. prefer canonical theorem name for fact collection declarations — haftmann / hgweb
4. merged — paulson / hgweb
5. Tidying ugly proofs — paulson <lp15@cam.ac.uk> / hgweb
6. tuned; — Fabian Huch <huch@in.tum.de> / hgweb

#2175 (Apr 12, 2024, 12:50:07 AM)

1. tweaked time functions for median-of-medians selection in HOL-Data_Structures — Manuel Eberl <manuel@pruvisto.org> / hgweb

#2174 (Apr 11, 2024, 12:50:10 AM)

1. merged — wenzelm / hgweb
2. rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta; — wenzelm / hgweb
3. Tiny tweaks to proofs — paulson <lp15@cam.ac.uk> / hgweb

#2173 (Apr 9, 2024, 12:50:09 AM)

1. A bit of new material about type class "infinite", from Eval_FO — paulson <lp15@cam.ac.uk> / hgweb

#2172 (Apr 6, 2024, 4:16:54 AM)

1. avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax; — wenzelm / hgweb
2. proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...); — wenzelm / hgweb
3. adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested; — wenzelm / hgweb
4. Add entry on Sketch_and_Explore to CONTRIBUTORS — Simon Wimmer <wimmers@in.tum.de> / hgweb

#2171 (Apr 5, 2024, 3:42:58 AM)

1. moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory — Manuel Eberl <manuel@pruvisto.org> / hgweb
2. more portable: prefer official JDBC operation DatabaseMetaData.getColumns(); — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb

#2170 (Apr 4, 2024, 12:50:11 AM)

1. documented new syntax for fBall and fBex — desharna / hgweb
2. updated for release; — wenzelm / hgweb
3. Added tag Isabelle2024-RC1 for changeset 1231a7fb2510 — wenzelm / hgweb
4. misc tuning for release; — wenzelm / hgweb
5. update for release; — wenzelm / hgweb

#2169 (Apr 3, 2024, 1:05:02 AM)

1. merged — wenzelm / hgweb
2. update to stack-2.15.5, stackage-lts-22.15; — wenzelm / hgweb
3. clarified names: discontinue odd convention from 3 decades ago; — wenzelm / hgweb
4. 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
5. added documentation for meromorphicity etc. in HOL-Complex_Analysis — Manuel Eberl <manuel@pruvisto.org> / hgweb
6. merged — desharna / hgweb
7. merged — desharna / hgweb
8. added special syntax for FSet.Ball and FSet.Bex — desharna / hgweb
9. tuned proof — desharna / hgweb
10. tuned proofs of Equiv_Relations.equiv — desharna / hgweb
11. remove transitional (dummy) component list for Go — Lars Hupel <lars@hupel.info> / hgweb

#2168 (Apr 2, 2024, 12:50:07 AM)

1. clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code; — wenzelm / hgweb
2. 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
3. provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version; — wenzelm / hgweb
4. clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that "very_slow" is normally used together with "slow"; — wenzelm / hgweb

#2167 (Mar 31, 2024, 12:50:06 AM)

1. moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields — Manuel Eberl <eberlm@in.tum.de> / hgweb
2. update NEWS; — Fabian Huch <huch@in.tum.de> / hgweb
3. moved web_app module from AFP (e.g., for building web services for the distributed build); — Fabian Huch <huch@in.tum.de> / hgweb

#2166 (Mar 29, 2024, 12:50:09 AM)

1. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
2. removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML); — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. clarified modules: more official Sessions.notable_groups; — wenzelm / hgweb
5. tuned — nipkow / hgweb
6. merged — paulson / hgweb
7. An assortment of new material, mostly due to Manuel — paulson <lp15@cam.ac.uk> / hgweb
8. 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
9. tuned signature; — wenzelm / hgweb
10. tuned; — wenzelm / hgweb
11. tuned signature; — wenzelm / hgweb
12. merged — desharna / hgweb
13. added lemma wfp_on_image and author name to theory — desharna / hgweb

#2165 (Mar 28, 2024, 2:45:35 AM)

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

#2164 (Mar 27, 2024, 12:50:09 AM)

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

#2163 (Mar 26, 2024, 12:50:08 AM)

1. obsolete: base-line is macOS 11; — wenzelm / hgweb
2. more robust: always assume x86_64 (or its emulation on ARM); — wenzelm / hgweb
3. MLton lacks arm64-linux (see also 84f2d481d6d7); — wenzelm / hgweb
4. more ambitious test "AFP (macOS 14 Sonoma, Apple Silicon)", as replacement for AFP on lrzcloud2; — wenzelm / hgweb
5. update to stack-2.15.3, stackage-lts-22.6, ghc-9.6.4; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. merged — wenzelm / hgweb
8. misc updates, tuning and clarification; — wenzelm / hgweb
9. reformat source in jEdit (wrap margin 78); — wenzelm / hgweb
10. more accurate Markdown formatting, both for VSCode and Phabricator; — wenzelm / hgweb
11. just one README.md; — wenzelm / hgweb
12. tuned — nipkow / hgweb
13. merged — wenzelm / hgweb
14. more accurate platform directories: pkg/tool structure is hardwired in "go"; — wenzelm / hgweb
15. support for etc/platform.props, to specify multi-platform directory structure more accurately; — wenzelm / hgweb
16. clarified signature; — wenzelm / hgweb
17. tuned; — wenzelm / hgweb
18. clarified modules; — wenzelm / hgweb
19. clarified modules; — wenzelm / hgweb
20. build Isabelle component for Go: all platforms; — wenzelm / hgweb
21. misc tuning; — wenzelm / hgweb
22. just one copy of darwin-universal.tar.gz; — wenzelm / hgweb
23. documented running time function framework by Jonas Stahl — nipkow / hgweb
24. merged — desharna / hgweb
25. redefined wf as an abbreviation for "wf_on UNIV" — desharna / hgweb

#2162 (Mar 25, 2024, 12:50:24 AM)

1. merged — nipkow / hgweb
2. more uniform command names — nipkow / hgweb
3. tuned parameter order — nipkow / hgweb
4. shutdown lrzcloud2; — wenzelm / hgweb
5. tuned NEWS — desharna / hgweb
6. redefined wfP as an abbreviation for "wfp_on UNIV" — desharna / hgweb

#2161 (Mar 23, 2024, 12:50:09 AM)

1. merged — desharna / hgweb
2. added lemma wellorder.wfp_on_less[simp] — desharna / hgweb

#2160 (Mar 22, 2024, 4:21:33 AM)

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

#2159 (Mar 21, 2024, 1:39:20 AM)

1. build component for cvc5-latest (ef2bc3f735df); — wenzelm / hgweb
2. merged — desharna / hgweb
3. try proof method "order" in Sledgehammer's proof reconstruction — desharna / hgweb
4. added Mirabelle action "order" — desharna / hgweb
5. renamed lemma antisymp_on_reflcp to antisymp_on_reflclp — desharna / hgweb
6. tuned proof — desharna / hgweb
7. added lemma order_reflclp_if_transp_and_asymp — desharna / hgweb
8. added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on — desharna / hgweb
9. HOL-Library: added modulo/congruence for real numbers — Manuel Eberl <eberlm@in.tum.de> / hgweb
10. only print schedule if relevant; — Fabian Huch <huch@in.tum.de> / hgweb
11. remove laziness: no need, and errors during initialization loop with close(); — Fabian Huch <huch@in.tum.de> / hgweb
12. more general definition of meromorphicity; Weierstraß factorisation theorem — Manuel Eberl <eberlm@in.tum.de> / hgweb
13. always provide build_database_server option in benchmark command; — Fabian Huch <huch@in.tum.de> / hgweb
14. always check if node is defined, e.g. for exists_next operation wit empty schedule; — Fabian Huch <huch@in.tum.de> / hgweb

#2158 (Mar 20, 2024, 12:50:09 AM)

1. fixed typo — blanchet / hgweb

#2157 (Mar 19, 2024, 1:09:37 AM)

1. disable taskset for now: performance impact is negative; — Fabian Huch <huch@in.tum.de> / hgweb
2. allow specifying initial schedule; — Fabian Huch <huch@in.tum.de> / hgweb
3. clarify use of num_threads vs. max_cpus; — Fabian Huch <huch@in.tum.de> / hgweb
4. clarified host: pre-load max threads; — Fabian Huch <huch@in.tum.de> / hgweb
5. clarified: more operations; — Fabian Huch <huch@in.tum.de> / hgweb

#2156 (Mar 18, 2024, 4:06:08 AM)

1. added alias wfp for wfP — desharna / hgweb
2. merged — desharna / hgweb
3. added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset — desharna / hgweb
4. start scheduled jobs earlier, if possible; — Fabian Huch <huch@in.tum.de> / hgweb
5. tuned proofs — desharna / hgweb
6. added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal — desharna / hgweb
7. merged — desharna / hgweb
8. added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively — desharna / hgweb

#2155 (Mar 17, 2024, 12:50:10 AM)

1. read/write proper schedule date (amending 9da3019e1ee5); — Fabian Huch <huch@in.tum.de> / hgweb
2. allow read/write of schedule in build (read via option, write from tool); — Fabian Huch <huch@in.tum.de> / hgweb
3. file representation for schedule (e.g., for generating from external tool); — Fabian Huch <huch@in.tum.de> / hgweb
4. proper median/mean time; — Fabian Huch <huch@in.tum.de> / hgweb
5. remove schedule outdated limit: delay is sufficient; — Fabian Huch <huch@in.tum.de> / hgweb
6. tuned whitespace; — Fabian Huch <huch@in.tum.de> / hgweb
7. tie-breaking in schedule optimization to pick best schedule even when run-time is dominated by large task (e.g., session with long timeout but no data yet); — Fabian Huch <huch@in.tum.de> / hgweb
8. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
9. remove old build before generating schedule; — Fabian Huch <huch@in.tum.de> / hgweb
10. unused; — Fabian Huch <huch@in.tum.de> / hgweb

#2154 (Mar 16, 2024, 1:55:22 AM)

1. merged — desharna / hgweb
2. added lemmas antisymp_on_image, asymp_on_image, irreflp_on_image, reflp_on_image, symp_on_image, totalp_on_image, and transp_on_image — desharna / hgweb
3. clarified names; — wenzelm / hgweb
4. sketch & explore: TODO comments are addressed in parent commits — Simon Wimmer <wimmers@in.tum.de> / hgweb
5. sketch & explore: reduce unnecessary type constraints — Simon Wimmer <wimmers@in.tum.de> / hgweb
6. sketch & explore: replace functionality of `sketch` by more useful `nxsketch` (and remove `nxsketch`) — Simon Wimmer <wimmers@in.tum.de> / hgweb
7. sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text — Simon Wimmer <wimmers@in.tum.de> / hgweb
8. change benchmark session to FOLP-ex (faster and less mean squared error than ZF-Constructible); — Fabian Huch <huch@in.tum.de> / hgweb

#2153 (Mar 15, 2024, 12:50:13 AM)

1. unused; — Fabian Huch <huch@in.tum.de> / hgweb
2. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
3. proper IPC for scheduled builds, following 7ae25372ab04; — Fabian Huch <huch@in.tum.de> / hgweb
4. proper check (amending 9aef1d1535ff); — Fabian Huch <huch@in.tum.de> / hgweb
5. more synced options (following 6e5397fcc41b); — Fabian Huch <huch@in.tum.de> / hgweb
6. avoid [no_atp] declations shadowing propositions from sledgehammer — haftmann / hgweb
7. track start in build job results (following 9d484c5d3a63), so it can directly be written to build log database; — Fabian Huch <huch@in.tum.de> / hgweb
8. use inherited build_start, following d9fc2cc37694; — Fabian Huch <huch@in.tum.de> / hgweb
9. update NEWS + CONTRIBUTORS for release; — wenzelm / hgweb
10. Tuned proofs — haftmann / hgweb

#2152 (Mar 14, 2024, 12:50:07 AM)

1. merged — wenzelm / hgweb
2. revert most parts of 0e79fa88cab6: somewhat ambitious attempt to move towards "editing" builds via added/canceled workers;
   retain notion of next_jobs.limit and finished() from 0e79fa88cab6;
   clarified Job vs. optional Build_Job; — wenzelm / hgweb
3. database performance tuning: prefer light-weight IPC over heavy-duty transactions, following bf377e10ff3b; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned whitespace; — wenzelm / hgweb
6. proper system option, instead of hardwired default; — wenzelm / hgweb
7. tuned signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
8. tuned comments; — wenzelm / hgweb
9. clarified build schedule host: proper module; — Fabian Huch <huch@in.tum.de> / hgweb
10. remove unused dummy; — Fabian Huch <huch@in.tum.de> / hgweb
11. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
12. use timeout as default build time predictor if no data is available; — Fabian Huch <huch@in.tum.de> / hgweb

#2151 (Mar 13, 2024, 12:50:07 AM)

1. merged — paulson / hgweb
2. Restored Riemann_Mapping as an import of Complex_Analysis — paulson <lp15@cam.ac.uk> / hgweb
3. proper file headers; — wenzelm / hgweb
4. clarified modules; — wenzelm / hgweb
5. merged — wenzelm / hgweb
6. database performance tuning: pull changed entries only, based on recorded updates (see 98d65411bfdb); — wenzelm / hgweb
7. tuned signature: more operations; — wenzelm / hgweb
8. clarified signature: more explicit types; — wenzelm / hgweb
9. tuned signature; — wenzelm / hgweb
10. removed somewhat pointless check; — wenzelm / hgweb
11. tuned signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
12. merged — paulson / hgweb
13. Fixed a latex error in the markup — paulson <lp15@cam.ac.uk> / hgweb

#2150 (Mar 12, 2024, 12:50:08 AM)

1. minor performance tuning: SQL.order_by is only for demo purposes; — wenzelm / hgweb
2. support efficient access to state updates, based on LEFT OUTER JOIN; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned: prefer if_proper expression; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. tuned: prefer if_proper expression; — wenzelm / hgweb
7. New material by Wenda Li and Manuel Eberl — paulson <lp15@cam.ac.uk> / hgweb
8. merged — traytel / hgweb
9. export BNF properties about the cardinal bound (by Jan van Brügge) — traytel / hgweb

#2149 (Mar 11, 2024, 12:50:09 AM)

1. unused (see 123f2c0995b8); — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. more robust init_built: get_build_id and start_build within the same transaction; — wenzelm / hgweb
4. tuned: remove redundant guard; — wenzelm / hgweb
5. maintain short build_id vs. build_uuid, similar to Database_Progress context/context_uuid;
   clarified database table "isabelle_build_updates"; — wenzelm / hgweb
6. more operations; — wenzelm / hgweb
7. clarified signature: init_state vs. init_unsynchronized; — wenzelm / hgweb
8. more thorough "isabelle build_process -C -r -f"; — wenzelm / hgweb
9. more operations; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. tuned signature: more uniform SQL.Data instances; — wenzelm / hgweb
12. tuned signature; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb

#2148 (Mar 10, 2024, 12:50:07 AM)

1. disable write_updates from f425bbc4b2eb for now: "isabelle build_process -rf" does not quite work yet; — wenzelm / hgweb
2. revert part of 5969ead9f900 that does not quite work yet: only one accidental host is used; — wenzelm / hgweb
3. record updates within database, based on serial; — wenzelm / hgweb
4. proper tables (amending 4611b7b47b42); — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. clarified signature: improved data integrity; — wenzelm / hgweb
7. clarified modules; — wenzelm / hgweb
8. clarified modules; — wenzelm / hgweb
9. obsolete; — wenzelm / hgweb
10. misc tuning: prefer Build_Process.Update operations; — wenzelm / hgweb
11. misc tuning and clarification: prefer explicit type Build_Process.Update; — wenzelm / hgweb
12. misc tuning and clarification; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb
14. clarified data representation: more uniform treatment of State.Pending vs. State.Running; — wenzelm / hgweb
15. tuned: drop pointless SQL.order_by (see also 5f706f7c624b); — wenzelm / hgweb
16. upgrade pretty_maybe_quote following 2746dfc9ceae; — wenzelm / hgweb
17. tuned; — wenzelm / hgweb
18. eliminate odd aliases (see also 2746dfc9ceae); — wenzelm / hgweb
19. tuned signature: prefer bottom-up construction; — wenzelm / hgweb
20. tuned; — wenzelm / hgweb
21. tuned signature; — wenzelm / hgweb

#2147 (Mar 9, 2024, 12:50:07 AM)

1. clarified signature; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. more operations for Build_Log.Meta_Info: prefer explicit types; — wenzelm / hgweb
4. more operations for Date and Time; — wenzelm / hgweb
5. more accurate patterns --- reverting unused fc3ba0a1c82f; — wenzelm / hgweb
6. remove unused/fragile option (amending db37cae970a6) --- universal_table requires pull_date tables; — wenzelm / hgweb
7. prefer explicit option "build_log_verbose"; — wenzelm / hgweb
8. tuned whitespace; — wenzelm / hgweb
9. additional build_log column "session_start", with implicit upgrade of database schema; — wenzelm / hgweb
10. more robust build_start for master and workers (via database); — wenzelm / hgweb
11. more accurate progress.now(), notably for Database_Progress; — wenzelm / hgweb
12. update NEWS; — wenzelm / hgweb
13. activate E 3.0 after testing by Martin Desharnais, see also db72d9920186 and 788f11af9822; — wenzelm / hgweb

#2146 (Mar 8, 2024, 4:53:02 AM)

1. merged — desharna / hgweb
2. added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp] — desharna / hgweb
3. parallelize schedule optimization; — Fabian Huch <huch@in.tum.de> / hgweb

#2145 (Mar 7, 2024, 12:50:08 AM)

1. revised NEWS: OCaml / OPAM appears to be fine on arm64-linux, e.g. Ubuntu 22.04; — wenzelm / hgweb
2. update to current long-term-support version dotnet-8.0.x; — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. proper release bundle_name (amending 0e7dd3eaa6e8); — wenzelm / hgweb
5. more multiset lemmas — blanchet / hgweb
6. optional cartouche syntax and proper name printing in atp Isar output — Simon Wimmer <wimmers@in.tum.de> / hgweb
7. merged — desharna / hgweb
8. removed unused variable — desharna / hgweb
9. added virtual, greedy portfolio for E 3.0 — desharna / hgweb

#2144 (Mar 6, 2024, 1:14:23 AM)

1. tuned; — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb
3. Added tag Isabelle2024-RC0 for changeset 98f009f56400 — wenzelm / hgweb
4. updated for release; — wenzelm / hgweb
5. updated for release; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. misc tuning for release; — wenzelm / hgweb
8. tuned whitespace: avoid TABs; — wenzelm / hgweb
9. avoid suspicious Unicode; — wenzelm / hgweb
10. tuned whitespace; — wenzelm / hgweb
11. tuned signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
12. merged — wenzelm / hgweb
13. update NEWS; — wenzelm / hgweb
14. update cygwin near 3.5.1-1, also see https://cygwin.com/pipermail/cygwin-announce/2024-February/011524.html and https://cygwin.com/pipermail/cygwin-announce/2024-February/011611.html — wenzelm / hgweb
15. drop unused Task.info field; — wenzelm / hgweb
16. proper guard_time (amending 752806151432); — wenzelm / hgweb
17. proper dynamic access (amending c3f07c950116); — wenzelm / hgweb
18. more robust, notably for remote process (via SSH); — wenzelm / hgweb
19. prefer dynamic objects, following a5fda30edae2; — wenzelm / hgweb
20. proper dynamic access (amending 52b5c7c8e6d9); — wenzelm / hgweb
21. clarified signature: incorporate guard into Logger; — wenzelm / hgweb
22. merged — desharna / hgweb
23. added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp — desharna / hgweb
24. Moving valuable library material from Martingales into the distribution — paulson <lp15@cam.ac.uk> / hgweb

#2143 (Mar 5, 2024, 12:50:10 AM)

1. clarified signature;
   sleep unconditionally: avoid aggressive database access; — wenzelm / hgweb
2. clarified module signature and state; — wenzelm / hgweb
3. tuned messages; — wenzelm / hgweb
4. omit somewhat pointless message, following b7187d4cdf68; — wenzelm / hgweb
5. more robust handling of uninitialized value, notably Build_Process.progress; — wenzelm / hgweb
6. tuned — nipkow / hgweb
7. partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded; — Fabian Huch <huch@in.tum.de> / hgweb
8. clarified module signature and state; — wenzelm / hgweb
9. tuned signature: more protected operations; — wenzelm / hgweb
10. database performance tuning: just one synchronized_database for main loop body; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. more robust: assume that database is exclusive for this Progress instance --- always close on exit (see also bf377e10ff3b); — wenzelm / hgweb

#2142 (Mar 4, 2024, 12:50:07 AM)

1. more robust: imitate Isabelle/ML operation more closely (after 26a43785590b);
   logical_cores is e.g. relevant for server-arm.sketis.net, where /proc/cpuinfo looks quite different; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
4. official support for arm64-linux, despite a few missing tools; — wenzelm / hgweb
5. discontinue unstable z3-4.4.1 for arm64-linux from Debian (in contrast to 796ae338eb9d and 87718883c8b9); — wenzelm / hgweb
6. proper platform_name/platform_dir for native arm64-darwin: already published in 788f11af9822 after manual adjustment; — wenzelm / hgweb

#2141 (Mar 2, 2024, 2:20:59 AM)

1. update to scala-3.3.3;
   enforce rebuild of Isabelle/Scala + Isabelle/ML; — wenzelm / hgweb
2. provide e-3.0.03 on all platforms, including arm64-linux and arm64-darwin --- still inactive; — wenzelm / hgweb
3. update NEWS, following 0d7c7fe65638; — Fabian Huch <huch@in.tum.de> / hgweb

#2140 (Mar 1, 2024, 2:29:41 AM)

1. provide cvc5-1.1.1 for testing --- still inactive; — wenzelm / hgweb
2. rebuild bash_process executables on current reference platforms, including native arm64-darwin;
   enforce rebuild of Isabelle/Scala + Isabelle/ML; — wenzelm / hgweb
3. tuned NEWS, see also c62003e05e46; — wenzelm / hgweb
4. update NEWS, following ea1913c953ef; — wenzelm / hgweb
5. tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:"; — wenzelm / hgweb
6. more explicit NEWS (see 3648e9c88d0c); — wenzelm / hgweb
7. NEWS for a53287d9add3, 3e30ca77ccfe; — wenzelm / hgweb
8. add option for unify trace (now disabled by default as printing is excessive and rarely used); — Fabian Huch <huch@in.tum.de> / hgweb
9. tuned unify trace option names; — Fabian Huch <huch@in.tum.de> / hgweb

#2139 (Feb 29, 2024, 12:50:11 AM)

1. more scalable: avoid potentially expensive ordering of underlying key data type, e.g. in MESON.Cache of Naproche; — wenzelm / hgweb
2. updated to stack-2.15.1, lts-22.6, ghc-9.6.3; — wenzelm / hgweb

#2138 (Feb 28, 2024, 12:55:56 AM)

1. merged — nipkow / hgweb
2. tuned name — nipkow / hgweb
3. new simplifier trace_op for tracing simproc calls — nipkow / hgweb
4. merged — paulson / hgweb
5. Some new material about Ramsey's theorem, also sharpening the proof to deliver the Erdős–Szekeres upper bound on Ramsey numbers — paulson <lp15@cam.ac.uk> / hgweb
6. support Zipperposition's skolemization in generated Isar proofs — blanchet / hgweb
7. improved output in simps_case_conv; — Fabian Huch <huch@in.tum.de> / hgweb
8. improved output in inductive module; — Fabian Huch <huch@in.tum.de> / hgweb
9. simplifier: no trace info from simprocs unless simp_debug = true. — nipkow / hgweb

#2137 (Feb 27, 2024, 12:50:10 AM)

1. deal with new-style Vampire skolemization in reconstructed Isar proofs — blanchet / hgweb

#2136 (Feb 26, 2024, 12:50:11 AM)

1. database performance tuning: prefer light-weight IPC over heavy-duty transactions; — wenzelm / hgweb
2. tuned signature;
   tuned output; — wenzelm / hgweb
3. tuned signature: follow PostgreSQL syntax instead of JDBC API; — wenzelm / hgweb
4. more robust shutdown: interruptible database connection; — wenzelm / hgweb
5. clarified signature: more convenient send/receive operations; — wenzelm / hgweb

#2135 (Feb 25, 2024, 12:50:07 AM)

1. clarified versions for documentation; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. clarified signature: avoid hardwired values; — wenzelm / hgweb
4. clarified IPC via database server: receive notifications quasi-spontaneously via auxiliary thread; — wenzelm / hgweb
5. minor performance tuning: just 1 transaction for slices <= 1; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. tuned whitespace; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. clarified signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
10. removed unused database_server (amending 32ca3d1283de); — wenzelm / hgweb
11. timing function generation bug fix by Jonas Stahl — nipkow / hgweb

#2134 (Feb 24, 2024, 12:50:07 AM)

1. tuned signature: more types, fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
2. new less ad hoc implementation of the 'moura' tactic for skolemization — blanchet / hgweb

#2133 (Feb 23, 2024, 12:50:09 AM)

1. more thorough Store.clean_output (amending 1fa1b32b0379); — wenzelm / hgweb
2. clarified signature: Build_Process tells how to clean sessions; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. minor performance tuning; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. tuned, following 7a1153c95bf9; — wenzelm / hgweb
10. merged — wenzelm / hgweb
11. tuned signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
12. proper usage; — wenzelm / hgweb
13. recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark; — wenzelm / hgweb
14. clarified signature; — wenzelm / hgweb
15. more robust: make double-sure that heap digest is present; — wenzelm / hgweb
16. tuned; — wenzelm / hgweb
17. minor performance tuning: just one transaction for log_db without heap; — wenzelm / hgweb
18. tuned; — wenzelm / hgweb
19. proper store.cache.compress; — wenzelm / hgweb
20. tuned whitespace; — wenzelm / hgweb
21. clarified store_session: heap requires process_result.ok, but log_db is always stored;
    clarified ML_Heap.clean_entry vs. ML_Heap.init_entry; — wenzelm / hgweb
22. unused; — wenzelm / hgweb
23. tuned; — wenzelm / hgweb
24. tuned names; — wenzelm / hgweb
25. tuned names; — wenzelm / hgweb
26. clarified database layout; — wenzelm / hgweb
27. tuned signature;
    tuned messages; — wenzelm / hgweb
28. clarified signature; — wenzelm / hgweb
29. more accurate types; — wenzelm / hgweb
30. build local log_db, with store/restore via optional database server;
    tuned messages; — wenzelm / hgweb
31. propagate property "isabelle.debug", notably for Java/Scala exception trace; — wenzelm / hgweb
32. tuned; — wenzelm / hgweb
33. proper treatment of "isabelle build_process -C" (amending 0cac7e3634d0); — wenzelm / hgweb
34. clarified signature;
    more robust slice_size; — wenzelm / hgweb
35. clarified names; — wenzelm / hgweb
36. more explicit build_cluster flag to guard open_build_database server; — wenzelm / hgweb
37. tuned; — wenzelm / hgweb
38. clarified signature; — wenzelm / hgweb
39. simplified specification of type class semiring_bits — haftmann / hgweb

#2132 (Feb 22, 2024, 12:50:10 AM)

1. New material about transcendental functions, polynomials, et cetera, thanks to Manuel Eberl — paulson <lp15@cam.ac.uk> / hgweb

#2131 (Feb 20, 2024, 12:50:07 AM)

1. merged — paulson / hgweb
2. A small collection of new and useful facts, including the AM-GM inequality — paulson <lp15@cam.ac.uk> / hgweb
3. remove selected occurrences of 'moura' tactic — blanchet / hgweb
4. added lemmas relpowp_left_unique and relpow_left_unique — desharna / hgweb
5. added lemmas relpowp_right_unique and relpow_right_unique — desharna / hgweb
6. use define_time_fun — nipkow / hgweb

#2130 (Feb 19, 2024, 12:50:08 AM)

1. time funs: +1 instead of 1+ — nipkow / hgweb
2. minor performance tuning; — wenzelm / hgweb
3. clarified signature: more comprehensive operations; — wenzelm / hgweb
4. clarified signature: more explicit types; — wenzelm / hgweb
5. clarified signature: emphasize physical db files; — wenzelm / hgweb
6. tuned: afford untyped/unscoped update; — wenzelm / hgweb
7. clarified signature: avoid ill-defined type java.net.URL; — wenzelm / hgweb
8. unused; — wenzelm / hgweb

#2129 (Feb 18, 2024, 12:50:09 AM)

1. tuned: afford untyped/unscoped update; — wenzelm / hgweb
2. more robust default: Scala imposes explicit "threads" value on ML, both the Poly/ML RTS and Isabelle/ML; — wenzelm / hgweb
3. clarified signature: more explicit types/scopes; — wenzelm / hgweb
4. tuned names; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. tuned documentation; — wenzelm / hgweb
7. more robust: disallow empty clusters, so "isabelle build -H" really means cluster build; — wenzelm / hgweb
8. clarified modules: centralize default policy; — wenzelm / hgweb
9. more explicit types --- fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
10. tuned: avoid shadowing of names; — wenzelm / hgweb
11. clarified default "isabelle build -j0 -H"; — wenzelm / hgweb
12. tuned whitespace; — wenzelm / hgweb
13. clarifier worker vs. master, which may coincide for local build; — wenzelm / hgweb
14. clarified signature: more standard defaults; — wenzelm / hgweb
15. clarified signature; — wenzelm / hgweb
16. clarified signature; — wenzelm / hgweb
17. tuned; — wenzelm / hgweb
18. prefer static object, while class is required for "services"; — wenzelm / hgweb
19. clarified signature: prefer default; — wenzelm / hgweb

#2128 (Feb 17, 2024, 12:50:11 AM)

1. merged — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. more robust: check subclasses as well; — wenzelm / hgweb
4. more robust; — wenzelm / hgweb
5. support for alternative user home, e.g. to avoid slow NFS shares; — wenzelm / hgweb
6. support explicit USER_HOME within SSH session; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. merged — paulson / hgweb
9. Further adjustments to the syntax for Lebesgue integration — paulson <lp15@cam.ac.uk> / hgweb
10. tuned comments; — wenzelm / hgweb
11. more robust: always close, despite failure; — wenzelm / hgweb
12. clarified signature; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb
14. tuned comments; — wenzelm / hgweb
15. clarified signature; — wenzelm / hgweb
16. Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury — blanchet / hgweb

#2127 (Feb 16, 2024, 12:50:07 AM)

1. tuned whitespace; — wenzelm / hgweb
2. prefer static object, while class is required for "services" (see 47eb96592aa2); — wenzelm / hgweb
3. clarified directories;
   clarified names; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned: prefer explicit update operation for immutable options; — wenzelm / hgweb
6. tuned message; — wenzelm / hgweb
7. more robust type, with explicit default; — wenzelm / hgweb
8. tuned usage message; — wenzelm / hgweb
9. clarified signature; — wenzelm / hgweb
10. more robust defaults; — wenzelm / hgweb
11. merged — desharna / hgweb
12. added lemmas relpow_trans[trans] and relpowp_trans[trans] — desharna / hgweb
13. more on disjunctive addition/subtraction — haftmann / hgweb

#2126 (Feb 15, 2024, 2:28:54 AM)

1. merged — wenzelm / hgweb
2. prefer physical processors (see also 4b014e6c1dfe and 26a43785590b); — wenzelm / hgweb
3. more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0"); — wenzelm / hgweb
4. more robust default; — wenzelm / hgweb
5. more accurate, notably on lxbroy10 and vmnipkow9; — wenzelm / hgweb
6. clarified num_processors: follow Poly/ML (with its inaccuracies); — wenzelm / hgweb
7. clarified modules, following Isabelle/ML; — wenzelm / hgweb
8. clarified signature; — wenzelm / hgweb
9. tuned comments; — wenzelm / hgweb
10. merged — paulson / hgweb
11. the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses — paulson <lp15@cam.ac.uk> / hgweb
12. merged — paulson / hgweb
13. A few lemmas brought in from AFP entries — paulson <lp15@cam.ac.uk> / hgweb
14. merged — traytel / hgweb
15. made destructor-view tactic more robust (by Jan van Brügge) — traytel / hgweb

#2125 (Feb 14, 2024, 12:50:09 AM)

1. performance optimization; — Fabian Huch <huch@in.tum.de> / hgweb
2. clarified names; — Fabian Huch <huch@in.tum.de> / hgweb
3. clarified scheduler: proper split into scheduler, generator, and priority rules (following 32d00ec387f4); — Fabian Huch <huch@in.tum.de> / hgweb
4. proper "linux_arm", amending 76ad72736e9e; — wenzelm / hgweb

#2124 (Feb 13, 2024, 12:50:10 AM)

1. more lemmas — haftmann / hgweb

#2123 (Feb 12, 2024, 12:50:12 AM)

1. new lemmas involving Ramsey numbers, infinite sets — paulson <lp15@cam.ac.uk> / hgweb

#2122 (Feb 10, 2024, 2:38:57 AM)

1. simplified class specification — haftmann / hgweb

#2121 (Feb 9, 2024, 12:50:10 AM)

1. Removal of duplicate code — paulson <lp15@cam.ac.uk> / hgweb
2. Two new theorems — paulson <lp15@cam.ac.uk> / hgweb

#2120 (Feb 8, 2024, 12:50:06 AM)

1. more lemmas and more correct lemma names — haftmann / hgweb
2. NEWS: corrected the definition of convexity of functions — paulson <lp15@cam.ac.uk> / hgweb
3. Further lemmas concerning complexity and measures — paulson <lp15@cam.ac.uk> / hgweb

#2119 (Feb 7, 2024, 12:50:07 AM)

1. Correct the definition of a convex function, and updated the proofs — paulson <lp15@cam.ac.uk> / hgweb

#2118 (Feb 6, 2024, 12:50:08 AM)

1. merged; — wenzelm / hgweb
2. update to windows_app-20240205, with executables for linux, linux_arm, macos; — wenzelm / hgweb
3. omit redundant options; — wenzelm / hgweb
4. tuned README; — wenzelm / hgweb
5. uniform build of binutils for linux, linux_arm, macos; — wenzelm / hgweb
6. fix reconstruction of Alethe's and_pos rule — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
7. added lemmas Multiset.transp_on_multp and Multiset.trans_on_mult — desharna / hgweb

#2117 (Feb 5, 2024, 12:50:09 AM)

1. proper target option, following package binutils-mingw-w64-x86-64 from Debian/Ubuntu; — wenzelm / hgweb
2. updated windows_app based on launch4j-3.50-linux-x64, without rebuilding GNU binutils (missing COFF target pe-i386); — wenzelm / hgweb
3. proper sfx_archive_name; — wenzelm / hgweb
4. clarified options; — wenzelm / hgweb
5. more robust; — wenzelm / hgweb
6. build Isabelle windows_app component from GNU binutils and launch4j; — wenzelm / hgweb

#2116 (Feb 3, 2024, 12:50:07 AM)

1. proper windows_app/launch4j-linux_arm; — wenzelm / hgweb
2. merged — paulson / hgweb
3. A small number of new lemmas — paulson <lp15@cam.ac.uk> / hgweb
4. explicit reference to code_dt — haftmann / hgweb

#2115 (Feb 2, 2024, 4:05:58 AM)

1. made lift_bnf more robust for abstract types with 'phantom' type variables — traytel / hgweb

#2114 (Feb 1, 2024, 12:50:08 AM)

1. rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO";
   uniform baseline for "linux" and "linux_arm"; — wenzelm / hgweb
2. proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb); — wenzelm / hgweb
3. proper bash syntax (amending 0631dfc0db07); — wenzelm / hgweb
4. tuned proof: avoid z3; — wenzelm / hgweb
5. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
6. tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux; — wenzelm / hgweb
7. merged — wenzelm / hgweb
8. more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193); — wenzelm / hgweb
9. strengthened class parity — haftmann / hgweb

#2113 (Jan 31, 2024, 12:50:09 AM)

1. proper accessible paths for web server; — wenzelm / hgweb
2. more informative message (amending b8a6b2ec85a2); — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. more robust: do not affect "$ISABELLE_HOME_USER/contrib" on master node; — wenzelm / hgweb
5. avoid excessive ML heap on this 16GB node; — wenzelm / hgweb
6. more robust (amending c9774306a879); — wenzelm / hgweb
7. proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings; — wenzelm / hgweb
8. clarified symbolic host name; — wenzelm / hgweb
9. allow remote_build on this host (server-arm), without conflicts of this "isabelle_self"; — wenzelm / hgweb
10. more robust message; — wenzelm / hgweb
11. A few more new theorems taken from AFP entries — paulson <lp15@cam.ac.uk> / hgweb

#2112 (Jan 30, 2024, 1:36:05 AM)

1. merged — nipkow / hgweb
2. define_time_function: avoid unused let's — nipkow / hgweb
3. common type class for trivial properties on div/mod — haftmann / hgweb
4. more robust (amending 1600fb749c54), to support the following corner case:
     schematic_goal "PROP ((?f :: ?'a \<Rightarrow> _) (x :: ?'a))"
       apply (tactic \<open>PRIMITIVE (Thm.instantiate (TVars.make1 ((("'a", 0), []), @{ctyp prop}), Vars.empty))\<close>)
       oops — wenzelm / hgweb

#2111 (Jan 29, 2024, 12:50:07 AM)

1. proper test options; — wenzelm / hgweb

#2110 (Jan 28, 2024, 12:50:08 AM)

1. proper history_base for linux_arm; — wenzelm / hgweb
2. updated to PostgreSQL 12 on Ubuntu 20.04;
   more accurate command-line; — wenzelm / hgweb
3. routine build + test for linux_arm; — wenzelm / hgweb
4. disable test on "augsburg1": machine will be dismantled; — wenzelm / hgweb

#2109 (Jan 27, 2024, 12:50:10 AM)

1. add approximation factors in build schedule to estimate build times more conservatively; — Fabian Huch <huch@in.tum.de> / hgweb
2. merged — paulson / hgweb
3. Type class patch suggested by Achim Brucker, plus tidied lemma — paulson <lp15@cam.ac.uk> / hgweb
4. rearranged and reformulated abstract classes for bit structures and operations — haftmann / hgweb

#2108 (Jan 26, 2024, 12:50:07 AM)

1. Three new lemmas — paulson <lp15@cam.ac.uk> / hgweb

#2107 (Jan 25, 2024, 4:08:02 AM)

1. tuned proof: avoid z3 to make it work on arm64-linux; — wenzelm / hgweb
2. update to jdk-21.0.2;
   enforce rebuild of Isabelle/Scala + Isabelle/ML; — wenzelm / hgweb
3. make build process state protected to avoid copying in subclasses (e.g. for database connections); — Fabian Huch <huch@in.tum.de> / hgweb
4. add build_sync tag to sync certain options (e.g., build_engine) across build processes; — Fabian Huch <huch@in.tum.de> / hgweb

#2106 (Jan 24, 2024, 12:50:10 AM)

1. clarified Mercurial version: presumably the last version that supports both python2 and python3; — wenzelm / hgweb
2. more robust: avoid crash on non-Linux systems; — wenzelm / hgweb
3. clarified webserver names; — wenzelm / hgweb
4. proper Apache.php_name; — wenzelm / hgweb
5. proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04); — wenzelm / hgweb
6. tuned source structure; — wenzelm / hgweb
7. more robust systemd configuration; — wenzelm / hgweb
8. more robust nginx configuration, notably for "certbot --nginx -d DOMAIN"; — wenzelm / hgweb
9. tuned whitespace in generated file; — wenzelm / hgweb
10. tuned; — wenzelm / hgweb
11. clarified modules; — wenzelm / hgweb

#2105 (Jan 23, 2024, 12:50:06 AM)

1. recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL); — wenzelm / hgweb
2. proper php-fpm configuration for nginx; — wenzelm / hgweb
3. support multiple webservers: Apache or Nginx; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method); — wenzelm / hgweb
6. unused; — wenzelm / hgweb

#2104 (Jan 21, 2024, 1:16:57 AM)

1. enforce rebuild of Isabelle/Scala + Isabelle/ML; — wenzelm / hgweb
2. updated to postgresql-42.7.1; — wenzelm / hgweb
3. updated to sqlite-jdbc-3.45.0.0, including slf4j-1.7.36; — wenzelm / hgweb
4. update to llncs-2.23;
   update src/Doc/Demo_LLNCS to include the new mandatory section "Disclosure of Interests"; — wenzelm / hgweb
5. clarified bootstrap; — wenzelm / hgweb
6. clarified directories; — wenzelm / hgweb
7. clarified directories; — wenzelm / hgweb
8. obsolete (see also fc88b943e1b2); — wenzelm / hgweb
9. proper output, following 2cd23d587db9; — wenzelm / hgweb
10. always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c); — wenzelm / hgweb
11. clarified directories; — wenzelm / hgweb
12. more accurate Isabelle versions; — wenzelm / hgweb
13. more accurate Ubuntu versions; — wenzelm / hgweb

#2103 (Jan 20, 2024, 12:50:09 AM)

1. more uses of define_time_fun — nipkow / hgweb

#2102 (Jan 19, 2024, 12:50:10 AM)

1. translation to time functions now with canonical let. — nipkow / hgweb

#2101 (Jan 17, 2024, 12:50:11 AM)

1. merged — paulson / hgweb
2. A few new results (mostly brought in from other developments) — paulson <lp15@cam.ac.uk> / hgweb
3. merged — nipkow / hgweb
4. Added time function automation — nipkow / hgweb

#2100 (Jan 16, 2024, 5:19:39 AM)

1. streamlined type class specification — haftmann / hgweb
2. consolidated lemma name — haftmann / hgweb

#2099 (Jan 15, 2024, 5:17:16 AM)

1. support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49"; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. update links; — wenzelm / hgweb
5. follow post-maintenance updates of original Phabricator, as base-line for Phorge; — wenzelm / hgweb
6. refer to "localhost" as pro-forma domain; — wenzelm / hgweb
7. simplified specification of type class — haftmann / hgweb
8. consolidated name of lemma analogously to nat/int/word_bit_induct — haftmann / hgweb

#2098 (Jan 13, 2024, 1:08:08 AM)

1. more accurate syntax: 'obtain' vars are optional; — wenzelm / hgweb

#2097 (Jan 12, 2024, 12:50:08 AM)

1. clarified order, disregard structure of proof; — wenzelm / hgweb
2. minor performance tuning; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. more thorough treatment of hidden type variables within zproof; — wenzelm / hgweb
5. more uniform treatment of "hyps" within zproof; — wenzelm / hgweb
6. clarified order: follow Thm.fold_terms; — wenzelm / hgweb

#2096 (Jan 11, 2024, 2:32:04 AM)

1. merged — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. clarified test: no exception yet; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. tuned signature: more direct operations; — wenzelm / hgweb
10. clarified signature; — wenzelm / hgweb
11. clarified signature: more direct operations; — wenzelm / hgweb
12. tuned signature; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure); — wenzelm / hgweb
15. tuned whitespace; — wenzelm / hgweb
16. more robust: certify types uniformly (see also 62b75508eb66); — wenzelm / hgweb
17. tuned; — wenzelm / hgweb
18. clarified signature; — wenzelm / hgweb
19. clarified signature: avoid redundant Term.maxidx_of_term; — wenzelm / hgweb
20. proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75); — wenzelm / hgweb
21. misc tuning and clarification: prefer Same.operation; — wenzelm / hgweb
22. clarified signature; — wenzelm / hgweb
23. tuned names; — wenzelm / hgweb
24. clarified signature; — wenzelm / hgweb
25. tuned whitespace; — wenzelm / hgweb
26. clarified modules;
    minor performance tuning; — wenzelm / hgweb
27. clarified signature; — wenzelm / hgweb
28. added and removed lemmas — nipkow / hgweb
29. proper SMTP session: set envelope sender address correctly; — Fabian Huch <huch@in.tum.de> / hgweb

#2095 (Jan 10, 2024, 12:50:08 AM)

1. update javamail component with current jakarta mail APIs and eclipse angus implementation; — Fabian Huch <huch@in.tum.de> / hgweb

#2094 (Jan 9, 2024, 4:42:11 AM)

1. tuned source structure; — wenzelm / hgweb
2. clarified signature;
   minor performance tuning; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. minor performance tuning;
   eliminate clones; — wenzelm / hgweb
5. minor performance tuning; — wenzelm / hgweb
6. minor performance tuning; — wenzelm / hgweb
7. minor performance tuning; — wenzelm / hgweb
8. minor performance tuning; — wenzelm / hgweb
9. minor performance tuning; — wenzelm / hgweb
10. minor performance tuning; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. tuned signature; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb

#2093 (Jan 7, 2024, 2:46:27 AM)

1. more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT; — wenzelm / hgweb
2. omit syntactic of_class check, which is in conflict with sort constraints within the logic; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. minor performance tuning; — wenzelm / hgweb
5. clarified signature;
   clarified modules; — wenzelm / hgweb
6. misc tuning and clarification; — wenzelm / hgweb
7. tuned signature; — wenzelm / hgweb
8. tuned signature: canonical argument order; — wenzelm / hgweb

#2092 (Jan 5, 2024, 12:50:08 AM)

1. tuned; — wenzelm / hgweb
2. clarified datatype ztyp: omit special case that rarely occurs (thanks to ZClass and ZClassp); — wenzelm / hgweb
3. clarified box_proof: use sort constraints within the logic; — wenzelm / hgweb
4. more operations (see also 8368160d3c65); — wenzelm / hgweb

#2091 (Jan 3, 2024, 3:31:12 AM)

1. proper support for complex types, not just type variables (amending 623789141e39); — wenzelm / hgweb
2. proper instantiation for make_const_proof, notably change of types for term variables; — wenzelm / hgweb
3. tuned names; — wenzelm / hgweb
4. more operations; — wenzelm / hgweb

#2090 (Jan 2, 2024, 12:50:08 AM)

1. clarified signature; — wenzelm / hgweb

#2089 (Jan 1, 2024, 3:27:26 AM)

1. minor performance tuning: proper Same.operation; — wenzelm / hgweb
2. minor performance tuning: proper Same.operation;
   clarified modules; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. minor performance tuning: proper Same.operation;
   clarified modules; — wenzelm / hgweb
5. minor performance tuning: proper Same.operation; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. pro-forma support for ZTerm.sorts_zproof; — wenzelm / hgweb
9. tuned comments; — wenzelm / hgweb
10. tuned structure; — wenzelm / hgweb
11. minor performance tuning: proper Same.operation; — wenzelm / hgweb
12. tuned names (again); — wenzelm / hgweb

#2088 (Dec 31, 2023, 3:58:56 AM)

1. clarified modules; — wenzelm / hgweb
2. clarified signature: more operations; — wenzelm / hgweb
3. tuned names; — wenzelm / hgweb
4. clarified signature; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. tuned whitespace; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. clarified signature: prefer Same.operation; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. more zproofs; — wenzelm / hgweb
13. more operations; — wenzelm / hgweb
14. clarified modules;
    minor performance tuning; — wenzelm / hgweb
15. minor performance tuning, following 703201dbd413; — wenzelm / hgweb
16. tuned; — wenzelm / hgweb

#2087 (Dec 30, 2023, 1:21:03 AM)

1. clarified signature: suppress unused fields; — wenzelm / hgweb
2. eliminate clone (amending e7796c55d840); — wenzelm / hgweb
3. minor performance tuning; — wenzelm / hgweb
4. more operations; — wenzelm / hgweb
5. more operations; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb

#2086 (Dec 28, 2023, 3:46:53 AM)

1. clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned;
   more uniform Thm.transfer; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. more accurate Global_Theory.name_facts: burrow into expression of attributed theorems; — wenzelm / hgweb
7. clarified modules; — wenzelm / hgweb
8. clarified signature; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes; — wenzelm / hgweb
11. clarified signature; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. tuned: avoid duplicates; — wenzelm / hgweb
14. more operations; — wenzelm / hgweb
15. proper Thm.transfer; — wenzelm / hgweb

#2085 (Dec 27, 2023, 1:47:27 AM)

1. proper Thm.trim_context; — wenzelm / hgweb
2. clarified stored data: actual thm allows to replay zproofs in a modular manner; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned signature, following Proofterm.thm_header; — wenzelm / hgweb
5. more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. proper Thm_Name.make_list for thm_definition;
   tuned modules; — wenzelm / hgweb

#2084 (Dec 25, 2023, 12:53:48 AM)

1. more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923); — wenzelm / hgweb
2. more robust: zproofs need to be enabled (amending 43d8385db923); — wenzelm / hgweb
3. more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs; — wenzelm / hgweb
4. tuned names; — wenzelm / hgweb
5. clarified signature: support update of local_theory; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. clarified modules; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. unused; — wenzelm / hgweb
10. clarified modules; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. clarified modules; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. tuned signature; — wenzelm / hgweb
15. tuned; — wenzelm / hgweb
16. more operations; — wenzelm / hgweb

#2083 (Dec 24, 2023, 12:50:11 AM)

1. eliminate duplicate (see also 6cbcfac5b72e and af7b79271364); — wenzelm / hgweb
2. minor performance tuning: shorter names; — wenzelm / hgweb
3. minor performance tuning: static vs. dynamic rules; — wenzelm / hgweb
4. minor performance tuning; — wenzelm / hgweb

#2082 (Dec 23, 2023, 2:14:33 AM)

1. clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. more thorough treatment of zproof vs. proof: avoid accidental storage of large structures; — wenzelm / hgweb
5. clarified signature; — wenzelm / hgweb
6. observe option "prune_proofs"; — wenzelm / hgweb

#2081 (Dec 22, 2023, 2:43:49 AM)

1. clarified zproof storage: per-theory table in anticipation of session exports; — wenzelm / hgweb
2. proper thm_name for stored zproof; — wenzelm / hgweb
3. uniform treatment of lazy facts: actual proof terms are always strict; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned whitespace; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb

#2080 (Dec 21, 2023, 2:15:10 AM)

1. proper Thm.transfer; — wenzelm / hgweb
2. clarified context: avoid capture of thy2 within closure; — wenzelm / hgweb
3. tuned names; — wenzelm / hgweb
4. more informative exceptions; — wenzelm / hgweb
5. more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy"); — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. more informative exception; — wenzelm / hgweb
8. clarified signature; — wenzelm / hgweb
9. clarified ML toplevel output: avoid "??." prefix; — wenzelm / hgweb
10. tuned; — wenzelm / hgweb

#2079 (Dec 20, 2023, 3:59:53 AM)

1. merged — wenzelm / hgweb
2. use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. omit pointless future: proof terms are built sequentially; — wenzelm / hgweb
5. omit unclear / inaccurate renaming; — wenzelm / hgweb
6. more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm; — wenzelm / hgweb
7. more robust: avoid assumption about Context.certificate_theory; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041); — wenzelm / hgweb
10. tuned; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. more normalization; — wenzelm / hgweb
13. less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large); — wenzelm / hgweb
14. tuned; — wenzelm / hgweb
15. more thorough beta contraction, following Envir.norm_term; — wenzelm / hgweb
16. tuned, following Envir.norm_term; — wenzelm / hgweb
17. more operations; — wenzelm / hgweb
18. merged — nipkow / hgweb
19. unused lemma — nipkow / hgweb
20. restore benchmark requirement heaps properly; — Fabian Huch <huch@in.tum.de> / hgweb
21. continue build while waiting for updated schedule; — Fabian Huch <huch@in.tum.de> / hgweb
22. clarified signature; — Fabian Huch <huch@in.tum.de> / hgweb
23. added start-up sequence for benchmark with requirements; — Fabian Huch <huch@in.tum.de> / hgweb
24. use single-threaded session build as benchmark (using ZF-Constructible); — Fabian Huch <huch@in.tum.de> / hgweb
25. separate build processes for scheduler and scheduled; — Fabian Huch <huch@in.tum.de> / hgweb
26. add delay and limit options for when schedule is considered outdated; — Fabian Huch <huch@in.tum.de> / hgweb
27. proper closing order; — Fabian Huch <huch@in.tum.de> / hgweb
28. read serial for schedules (amending 2039f360); — Fabian Huch <huch@in.tum.de> / hgweb

#2078 (Dec 19, 2023, 2:42:04 AM)

1. more thorough beta contraction;
   removed unused operations; — wenzelm / hgweb
2. tuned whitespace; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. more operations, following proofterm.ML; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. clarified signature, following Term.subst_bounds_same; — wenzelm / hgweb
7. tuned whitespace; — wenzelm / hgweb
8. minor performance tuning: more concise union; — wenzelm / hgweb
9. tuned comments; — wenzelm / hgweb
10. tuned, following close_proof; — wenzelm / hgweb
11. proper treatment of proof hyps, following 8368160d3c65; — wenzelm / hgweb
12. proper treatment of proof hyps: unchangeable, like bound; — wenzelm / hgweb
13. proper Thm.transfer (required for zproofs); — wenzelm / hgweb
14. clarified signature; — wenzelm / hgweb
15. proper beta_norm after instantiation (amending 90c5aadcc4b2); — wenzelm / hgweb
16. minor performance tuning: more direct beta_norm; — wenzelm / hgweb
17. more robust norm_proof: turn env into instantiation, based on visible statement; — wenzelm / hgweb
18. proper scope of cache (amending 61af3e917597); — wenzelm / hgweb
19. tuned comments; — wenzelm / hgweb

#2077 (Dec 16, 2023, 12:52:09 AM)

1. tuned names; — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb
3. more zproofs; — wenzelm / hgweb

#2076 (Dec 15, 2023, 2:54:54 AM)

1. more operations: zterm ordering that follows fast_term_ord; — wenzelm / hgweb
2. clarified signature;
   clarified modules; — wenzelm / hgweb
3. clarified modules; — wenzelm / hgweb
4. more zproofs; — wenzelm / hgweb
5. more zproofs, imitating existing proofs (which are a bit rough here); — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. tuned whitespace; — wenzelm / hgweb
8. minor performance tuning; — wenzelm / hgweb

#2075 (Dec 12, 2023, 2:45:13 AM)

1. tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8); — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. minor performance tuning; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. minor performance tuning: prefer Same.operation; — wenzelm / hgweb
6. clarified signature;
   minor performance tuning: avoid redundant identity; — wenzelm / hgweb
7. minor performance tuning; — wenzelm / hgweb
8. more operations; — wenzelm / hgweb
9. revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")]; — wenzelm / hgweb
10. misc tuning and clarification; — wenzelm / hgweb
11. minor performance tuning: prefer Symset.T;
    tuned names; — wenzelm / hgweb
12. minor performace tuning; — wenzelm / hgweb
13. minor performance tuning: prefer Same.operation; — wenzelm / hgweb
14. tuned: more standard accumulation; — wenzelm / hgweb
15. tuned; — wenzelm / hgweb
16. clarified modules; — wenzelm / hgweb
17. clarified signature; — wenzelm / hgweb
18. tuned whitespace; — wenzelm / hgweb
19. tuned; — wenzelm / hgweb
20. proper ZTerm.lift_proof (amending 4a1a25bdf81d); — wenzelm / hgweb
21. filter predecessors properly (amending ee405c40db72); — Fabian Huch <huch@in.tum.de> / hgweb
22. improve graphical clarity by omitting intra-host dependencies (following ee405c40db72); — Fabian Huch <huch@in.tum.de> / hgweb
23. more zproofs; — wenzelm / hgweb
24. minor performance tuning: more direct abstraction level; — wenzelm / hgweb
25. more general Logic.incr_indexes_operation;
    more special Logic.incr_indexes; — wenzelm / hgweb
26. tuned; — wenzelm / hgweb
27. tuned; — wenzelm / hgweb
28. clarified modules; — wenzelm / hgweb
29. clarified ML; — wenzelm / hgweb
30. clarified signature;
    minor performance tuning; — wenzelm / hgweb
31. tuned signature; — wenzelm / hgweb
32. avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292); — wenzelm / hgweb
33. tuned; — wenzelm / hgweb
34. more robust: proper Proofterm.get_proofs_level with bound check; — wenzelm / hgweb
35. tuned; — wenzelm / hgweb
36. clarified signature: fewer tuples; — wenzelm / hgweb
37. clarified signature: fewer tuples; — wenzelm / hgweb
38. clarified signature: more explicit get_proofs_level with bounds check; — wenzelm / hgweb

#2074 (Dec 9, 2023, 1:56:28 AM)

1. merged — wenzelm / hgweb
2. misc tuning and clarification: more standard Same.commit discipline; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. tuned names; — wenzelm / hgweb
5. more operations;
   more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term; — wenzelm / hgweb
6. minor performance tuning: more careful treatment of empty environment; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. more zproofs; — wenzelm / hgweb
9. clarified signature: support shared cache; — wenzelm / hgweb
10. tuned; — wenzelm / hgweb
11. tuned: avoid shadowing; — wenzelm / hgweb
12. more zproofs; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. more operations;
    clarified cache; — wenzelm / hgweb
15. tuned signature; — wenzelm / hgweb
16. tuned names; — wenzelm / hgweb
17. tuned -- eliminate clones; — wenzelm / hgweb
18. tuned; — wenzelm / hgweb
19. more operations; — wenzelm / hgweb
20. more operations; — wenzelm / hgweb
21. tuned; — wenzelm / hgweb
22. clarified signature; — wenzelm / hgweb
23. tuned; — wenzelm / hgweb
24. tuned; — wenzelm / hgweb
25. consider schedule calculation time in estimation; — Fabian Huch <huch@in.tum.de> / hgweb
26. compare previous build schedule with new one, to prevent regressions; — Fabian Huch <huch@in.tum.de> / hgweb
27. clarified: build schedules may be outdated when empty, after some time, or due to build progress; — Fabian Huch <huch@in.tum.de> / hgweb
28. store previous build jobs in graph so schedules can be used later in the build process; — Fabian Huch <huch@in.tum.de> / hgweb
29. add serial for build schedule to avoid unnecessary db read/writes; — Fabian Huch <huch@in.tum.de> / hgweb
30. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
31. clarified; — Fabian Huch <huch@in.tum.de> / hgweb
32. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
33. use build database to synchronize build schedule computed on master node (e.g., such that view on cluster is consistent); — Fabian Huch <huch@in.tum.de> / hgweb
34. add build uuid to schedule; — Fabian Huch <huch@in.tum.de> / hgweb
35. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
36. use schedule directly instead of extra cache; — Fabian Huch <huch@in.tum.de> / hgweb
37. added build schedule command-line wrapper; — Fabian Huch <huch@in.tum.de> / hgweb
38. added graphical representation of build schedules; — Fabian Huch <huch@in.tum.de> / hgweb
39. clarified build heuristics parameters; — Fabian Huch <huch@in.tum.de> / hgweb
40. proper parallel paths: factor in elapsed time; — Fabian Huch <huch@in.tum.de> / hgweb
41. performance tuning: cache estimates; — Fabian Huch <huch@in.tum.de> / hgweb

#2073 (Dec 8, 2023, 5:28:32 AM)

1. misc tuning and clarification; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. misc tuning and clarification, following Term.incr_bv / Term.incr_boundvars; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. minor performance tuning: regular Same.operation; — wenzelm / hgweb
7. clarified signature: more standard argument order; — wenzelm / hgweb
8. clarified signature: more standard argument order; — wenzelm / hgweb
9. tuned whitespace; — wenzelm / hgweb
10. tuned: more standard names; — wenzelm / hgweb
11. clarified signature; — wenzelm / hgweb
12. tuned: prefer Same.commit; — wenzelm / hgweb
13. tuned: more standard argument order; — wenzelm / hgweb
14. clarified signature; — wenzelm / hgweb
15. more operations;
    more caching; — wenzelm / hgweb
16. tuned comments; — wenzelm / hgweb

#2072 (Dec 7, 2023, 5:40:15 AM)

1. tuned structure; — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. performance tuning: cache for ztyp_of within zterm_of;
   clarified signature; — wenzelm / hgweb
5. tuned names; — wenzelm / hgweb
6. minor performance tuning; — wenzelm / hgweb
7. more zproofs; — wenzelm / hgweb
8. minor performance tuning; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. more zproofs; — wenzelm / hgweb
11. clarified modules; — wenzelm / hgweb
12. more zproofs; — wenzelm / hgweb
13. more zproofs; — wenzelm / hgweb
14. proper treatment of ZConstP: term represents body of closure; — wenzelm / hgweb
15. proper substitution of types within term; — wenzelm / hgweb
16. more accurate treatment of term variables after instantiation of type variables; — wenzelm / hgweb
17. tuned signature; — wenzelm / hgweb
18. tuned; — wenzelm / hgweb
19. check that Isar proofs contain one 'show' — blanchet / hgweb
20. include unnamed chained facts in Sledgehammer's relevance filter — blanchet / hgweb
21. merge — blanchet / hgweb
22. removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics — blanchet / hgweb
23. don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts — blanchet / hgweb
24. tuned T functions: now 0 if not recursive — nipkow / hgweb
25. minor performance tuning; — wenzelm / hgweb
26. tuned; — wenzelm / hgweb
27. more zproofs;
    clarified signature; — wenzelm / hgweb
28. misc tuning and clarification;
    eliminate clones (see also 3ae09d27ee7a); — wenzelm / hgweb
29. more zproofs; — wenzelm / hgweb
30. more operations; — wenzelm / hgweb
31. more operations; — wenzelm / hgweb
32. tuned; — wenzelm / hgweb
33. clarified signature; — wenzelm / hgweb
34. more zproofs; — wenzelm / hgweb
35. more ML pretty-printing; — wenzelm / hgweb
36. clarified const_proof vs. zproof_name; — wenzelm / hgweb

#2071 (Dec 5, 2023, 4:20:29 AM)

1. merged — wenzelm / hgweb
2. more zproofs;
   misc tuning and clarification; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. more operations;
   tuned semicolons; — wenzelm / hgweb
6. clarified modules;
   more source positions; — wenzelm / hgweb
7. more zterm operations;
   more zproofs; — wenzelm / hgweb

#2070 (Dec 4, 2023, 12:50:08 AM)

1. compactified specification of type class parity — haftmann / hgweb
2. generalized — haftmann / hgweb
3. explicit annotation of lemma duplicates — haftmann / hgweb

#2069 (Dec 3, 2023, 2:02:48 AM)

1. merged — wenzelm / hgweb
2. clarified proof_body: cover zboxes from zproof; — wenzelm / hgweb
3. pro-forma support for optional zproof: no proper content yet; — wenzelm / hgweb
4. clarified signature: follow Term.could_unify; — wenzelm / hgweb
5. clarified bootstrap --- modules related to proofterm.ML; — wenzelm / hgweb

#2068 (Dec 2, 2023, 12:50:09 AM)

1. clarified path time heuristic: configurable parameters for larger search space; — Fabian Huch <huch@in.tum.de> / hgweb
2. clarified heuristics toString;
   add generator description to schedule; — Fabian Huch <huch@in.tum.de> / hgweb
3. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
4. add heuristic for non-scheduled (standard) build behaviour; — Fabian Huch <huch@in.tum.de> / hgweb
5. proper unused nodes; — Fabian Huch <huch@in.tum.de> / hgweb
6. clarified schedule message; — Fabian Huch <huch@in.tum.de> / hgweb
7. proper parallel paths; — Fabian Huch <huch@in.tum.de> / hgweb
8. clarified build schedule host: more operations; — Fabian Huch <huch@in.tum.de> / hgweb
9. clarified path heuristic; — Fabian Huch <huch@in.tum.de> / hgweb
10. clarified graph operations in timing heuristic; — Fabian Huch <huch@in.tum.de> / hgweb
11. merged — nipkow / hgweb
12. added and removed [simp]s — nipkow / hgweb

#2067 (Dec 1, 2023, 1:41:11 AM)

1. tight representation of types / terms / proof terms (presently unused); — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. reduce redundancy: avoid huge lists; — wenzelm / hgweb
4. more detailed profiling including "names";
   avoid overlapping results; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. misc tuning and clarification; — wenzelm / hgweb
7. slightly more compact heap: better sharing of persistent tuples; — wenzelm / hgweb
8. added method to generate build schedules directly; — Fabian Huch <huch@in.tum.de> / hgweb
9. clarified load vs. apply vs. make; — Fabian Huch <huch@in.tum.de> / hgweb
10. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
11. tuned heuristic; — Fabian Huch <huch@in.tum.de> / hgweb
12. use cpu time for approximation; — Fabian Huch <huch@in.tum.de> / hgweb
13. lower bound for approximated times; — Fabian Huch <huch@in.tum.de> / hgweb
14. use full timing information in build schedule; — Fabian Huch <huch@in.tum.de> / hgweb
15. consistent hosts ordering; — Fabian Huch <huch@in.tum.de> / hgweb
16. filter hosts properly; — Fabian Huch <huch@in.tum.de> / hgweb

#2066 (Nov 30, 2023, 2:52:04 AM)

1. merged — wenzelm / hgweb
2. more compact representation of theory_id -- via consecutive thread-local ids; — wenzelm / hgweb
3. misc tuning and clarification; — wenzelm / hgweb
4. more compact representation; — wenzelm / hgweb
5. more compact representation; — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. more compact representation of theory_id; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. compact representation of sets of integers; — wenzelm / hgweb
10. generated build schedule explicitly (e.g., for further analysis); — Fabian Huch <huch@in.tum.de> / hgweb

#2065 (Nov 29, 2023, 1:53:26 AM)

1. de-duplicated specification of class ring_bit_operations — haftmann / hgweb

#2064 (Nov 28, 2023, 12:50:10 AM)

1. generalized — haftmann / hgweb
2. restructured — haftmann / hgweb
3. grouped lemmas for symbolic computations — haftmann / hgweb
4. sorted out lemma duplicates — haftmann / hgweb

#2063 (Nov 27, 2023, 12:50:10 AM)

1. more reactive headless server, in contrast to 15656ad28691 (when "isabelle dump" was important to export AFP content); — wenzelm / hgweb
2. tuned whitespace; — wenzelm / hgweb

#2062 (Nov 26, 2023, 12:50:11 AM)

1. clarified signature; — wenzelm / hgweb
2. clarified modules; — wenzelm / hgweb
3. clarified modules;
   clarified transactions; — wenzelm / hgweb
4. clarified modules: Build_Log.private_data provides raw data access without transaction_lock; — wenzelm / hgweb
5. more thorough transaction_lock; — wenzelm / hgweb
6. obsolete, see also a5896fe040dd; — wenzelm / hgweb
7. removed obsolete/broken isabelle_scala_script wrapper (see also abf9fcfa65cf); — wenzelm / hgweb
8. provide src/Tools/Demo as example for system component with Isabelle/Scala tool; — wenzelm / hgweb

#2059 (Nov 23, 2023, 12:50:09 AM)

1. modernized, reordered, generalized — haftmann / hgweb
2. more correct type annotation — haftmann / hgweb
3. proper build with jdk-21 (amending 4fb5e6499da9); — wenzelm / hgweb
4. NEWS; — wenzelm / hgweb
5. update to jdk-21.0.1;
   enforce rebuild of Isabelle/Scala + Isabelle/ML; — wenzelm / hgweb
6. rebuild jedit with minimal patch for jdk-21, following SVN 25690; — wenzelm / hgweb
7. clarified modules; — wenzelm / hgweb
8. suppress duplicate entries systematically using log_name: e.g. relevant for AFP; — wenzelm / hgweb
9. clarified operation: pick current pull_date instead of previous one; — wenzelm / hgweb
10. operations AND, OR, XOR are specified by characteristic recursive equation — haftmann / hgweb
11. clarified toml keys operations; — Fabian Huch <huch@in.tum.de> / hgweb
12. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
13. clarified toml keys: more operations; — Fabian Huch <huch@in.tum.de> / hgweb
14. use toml key operations properly;
    clarified module; — Fabian Huch <huch@in.tum.de> / hgweb
15. clarified toml keys formatting vs. toString; — Fabian Huch <huch@in.tum.de> / hgweb
16. clarified keys module; — Fabian Huch <huch@in.tum.de> / hgweb
17. pull out toml keys module; — Fabian Huch <huch@in.tum.de> / hgweb
18. clarified toml parser interface; — Fabian Huch <huch@in.tum.de> / hgweb
19. prefer symbolic build_history_base_arm; — wenzelm / hgweb
20. build_history: proper support for ISABELLE_APPLE_PLATFORM64; — wenzelm / hgweb
21. clarified isabelle_hg (again, see b9d59669904a); — wenzelm / hgweb
22. clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc); — wenzelm / hgweb
23. clarified signature: more operations and options concerning Isabelle hg; — wenzelm / hgweb
24. performance tuning: cache graph; — wenzelm / hgweb
25. tuned signature: fewer warnings in IntelliJ IDEA; — wenzelm / hgweb
26. unused (see also 004b39bf06a5); — wenzelm / hgweb
27. clarified signature and modules: more explicit Build_Log.History; — wenzelm / hgweb
28. tuned: avoid recursion; — wenzelm / hgweb
29. tuned; — wenzelm / hgweb
30. avoid duplicate data; — wenzelm / hgweb
31. output more data; — wenzelm / hgweb
32. tuned whitespace; — wenzelm / hgweb
33. clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache; — wenzelm / hgweb
34. proper ml_statistics (amending aeb511a520f4); — wenzelm / hgweb
35. unify error messages; — Fabian Huch <huch@in.tum.de> / hgweb
36. add file information to toml parse context and error messages; — Fabian Huch <huch@in.tum.de> / hgweb
37. add position information to toml parser and error messages; — Fabian Huch <huch@in.tum.de> / hgweb
38. properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another; — Fabian Huch <huch@in.tum.de> / hgweb
39. allow re-defining keys in toml object (already checked during parse time); — Fabian Huch <huch@in.tum.de> / hgweb
40. clarified toString for toml objects; — Fabian Huch <huch@in.tum.de> / hgweb

#2058 (Nov 17, 2023, 12:50:10 AM)

1. tuned — nipkow / hgweb

#2057 (Nov 14, 2023, 12:50:07 AM)

1. tuned message; — Fabian Huch <huch@in.tum.de> / hgweb
2. better invalidation for schedule cache (only on relevant changes); — Fabian Huch <huch@in.tum.de> / hgweb
3. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
4. timing heuristic: parallelize more aggressively to utilize hosts fully; — Fabian Huch <huch@in.tum.de> / hgweb
5. proper parallel paths for timing heuristic; — Fabian Huch <huch@in.tum.de> / hgweb
6. scheduled build: allocate cpus more aggressively, to avoid idle threads; — Fabian Huch <huch@in.tum.de> / hgweb
7. finalize scheduled build only on master node; — Fabian Huch <huch@in.tum.de> / hgweb
8. finalize current sessions before generating schedule; — Fabian Huch <huch@in.tum.de> / hgweb
9. clarified signature: more operations; — Fabian Huch <huch@in.tum.de> / hgweb
10. NEWS — desharna / hgweb

#2056 (Nov 13, 2023, 12:50:06 AM)

1. merged — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb
3. support for "cluster" table with "hosts" array, and params/options as for "host" table;
   support for "isabelle build -H cluster.name"; — wenzelm / hgweb
4. clarified signature: more operations, allow recursive get; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. tuned signature: more operations; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. tuned output; — wenzelm / hgweb
9. more robust: prefer strict operations; — wenzelm / hgweb
10. tuned message; — wenzelm / hgweb
11. tuned signature: more operations; — wenzelm / hgweb
12. more specific name for type class — haftmann / hgweb

#2055 (Nov 12, 2023, 12:50:07 AM)

1. proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023); — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. clarified modules; — wenzelm / hgweb
4. clarified signature: more operations; — wenzelm / hgweb
5. tuned comments; — wenzelm / hgweb
6. more NEWS; — wenzelm / hgweb
7. more TODO; — wenzelm / hgweb
8. prefer strict test of system options; — wenzelm / hgweb
9. some build cluster resources at TUM; — wenzelm / hgweb
10. build cluster host specifications are based on registry entries (table prefix "host"); — wenzelm / hgweb
11. more robust init; — wenzelm / hgweb
12. clarified signature: more operations; — wenzelm / hgweb
13. support interpreted/typed entries via Registry.Category and Registry.Table; — wenzelm / hgweb
14. clarified signature: more operations; — wenzelm / hgweb
15. clarified output; — wenzelm / hgweb
16. support for global registry; — wenzelm / hgweb
17. clarified loading of symbols: permissive entries in $ISABELLE_SYMBOLS require explicit "?"; — wenzelm / hgweb

#2054 (Nov 11, 2023, 12:50:07 AM)

1. slightly less technical formulation of very specific type class — haftmann / hgweb
2. weakened dependency — haftmann / hgweb
3. explicit type class for discrete linordered semidoms — haftmann / hgweb

#2053 (Nov 10, 2023, 12:50:06 AM)

1. proper dummy timing entries; — Fabian Huch <huch@in.tum.de> / hgweb
2. use only finished sessions in timing data; — Fabian Huch <huch@in.tum.de> / hgweb
3. tuned; — Fabian Huch <huch@in.tum.de> / hgweb
4. performance tuning for build schedule: explicit schedule generation, without mixing heuristics; — Fabian Huch <huch@in.tum.de> / hgweb
5. performance tuning for build schedule: faster stopping; — Fabian Huch <huch@in.tum.de> / hgweb
6. performance tuning for timing heuristic: pre-calculate graph operations; — Fabian Huch <huch@in.tum.de> / hgweb
7. move timing data into scheduler for more efficient heuristics (e.g., with pre-calculated values); — Fabian Huch <huch@in.tum.de> / hgweb
8. clarified signature: emphasize mutable instance; — wenzelm / hgweb
9. clarified signature: more operations; — wenzelm / hgweb
10. support for explicit SSH hostname; — wenzelm / hgweb
11. proper local host (amending 62d7ef1da441); — wenzelm / hgweb

#2052 (Nov 9, 2023, 12:50:08 AM)

1. merged — nipkow / hgweb
2. added lemma — nipkow / hgweb
3. proper default for disjunction (amending 9f7a94117666); — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. more operations; — wenzelm / hgweb
6. avoid option -C: free this latter for build-related configuration; — wenzelm / hgweb
7. more direct indentation, using Symbol.spaces; — wenzelm / hgweb
8. clarified signature; — wenzelm / hgweb
9. more accurate treatment of surrounding whitespace; — wenzelm / hgweb
10. obsolete (see also f627ab8c276c); — wenzelm / hgweb
11. tuned signature; — wenzelm / hgweb
12. clarified signature: Command_Span.Kind already contains keyword_kind, so parsing document structure no longer requires Keyword.Keywords; — wenzelm / hgweb

#2051 (Nov 8, 2023, 12:50:43 AM)

1. clarified modules; — wenzelm / hgweb
2. tuned signature; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d); — wenzelm / hgweb

#2050 (Nov 6, 2023, 12:50:11 AM)

1. more tests; — wenzelm / hgweb
2. clarified exploration of history: more uniform options; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb

#2049 (Nov 5, 2023, 12:50:07 AM)

1. enable multi-builds (again, see also 0c7419d3dd59); — wenzelm / hgweb
2. explore history more thoroughly; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. clarified "recent" time: days <= 0 means infinity (no constraint); — wenzelm / hgweb
5. tuned whitespace; — wenzelm / hgweb
6. proper exploration of older history: avoid premature fallback on current "rev" (see also d3d5cb2d6866, 6706d6f0afda); — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb
8. tuned output; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. tuned message; — wenzelm / hgweb

#2048 (Nov 4, 2023, 12:50:10 AM)

1. proper option; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. proper SQL.string syntax, following actual SQL standard instead of historic variations before PostgreSQL 9.1;
   ensure connection defaults required for string literals; — wenzelm / hgweb
4. Added Kronecker's approximation theorem. Requires adding Real_Asymp to HOL-Analysis. Funny syntax issue in Probability/Projective_Family — paulson <lp15@cam.ac.uk> / hgweb
5. merged — wenzelm / hgweb
6. prefer Time.scale(), following Isabelle/ML; — wenzelm / hgweb
7. proper benchmark command; — Fabian Huch <huch@in.tum.de> / hgweb
8. merged — wenzelm / hgweb
9. proper progress (see also 45d570945fe4); — wenzelm / hgweb
10. improved build messages; — Fabian Huch <huch@in.tum.de> / hgweb

#2047 (Nov 3, 2023, 2:13:17 AM)

1. clarified; — Lukas Stevens <mail@lukas-stevens.de> / hgweb
2. merged — paulson / hgweb
3. fixed the simplification of Suc n - 1 — paulson <lp15@cam.ac.uk> / hgweb
4. tuned whitespace; — wenzelm / hgweb
5. tuned message; — wenzelm / hgweb
6. just one pass is sufficient (see also cc8391b92747, 3e8a897042d9); — wenzelm / hgweb
7. more detailed progress for build_log_database, to see better what happens when; — wenzelm / hgweb
8. clarified signature: explicit Progress date; — wenzelm / hgweb
9. more uniform progress; — wenzelm / hgweb
10. more robust: support concurrent output; — wenzelm / hgweb
11. disable multi-builds (again): does not quite work yet; — wenzelm / hgweb

#2046 (Nov 1, 2023, 12:50:12 AM)

1. clarified modules; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. clarified SEQ: more sequential evaluation to support multiple tests (see also 5c91bd51fc37); — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. proper Compress.Cache; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. more parallelism via consumer thread: with mailbox limit to avoid ressource problems; — wenzelm / hgweb
8. support for mailbox limit; — wenzelm / hgweb
9. tuned signature; — wenzelm / hgweb
10. discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement; — wenzelm / hgweb
11. clarified database transactions (see also 2c704ae04db1, 7bd0a250183b); — wenzelm / hgweb

#2045 (Oct 30, 2023, 12:50:10 AM)

1. afford multiple tests on fast machines (see also edb4faf666c9 and 2a26d423d9fb);
   proper history_base for ARM; — wenzelm / hgweb
2. performance tuning: parallel and incremental update of build_log_database; — wenzelm / hgweb
3. performance tuning: more careful database access; — wenzelm / hgweb
4. clarified message; — wenzelm / hgweb
5. tuned signature; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb

#2044 (Oct 29, 2023, 12:50:09 AM)

1. prefer old-style import "=>"; — wenzelm / hgweb
2. merged — wenzelm / hgweb
3. redundant (see also 3069da1743bc); — wenzelm / hgweb
4. removed obsolete table (see also 6acd1a2bd146); — wenzelm / hgweb
5. more robust init_database();
   proper treatment of views, not tables (amending dd350a41594c); — wenzelm / hgweb
6. proper private_data.transaction_lock;
   prefer execute_batch_statement; — wenzelm / hgweb
7. clarified names; — wenzelm / hgweb
8. proper support for SSH; — wenzelm / hgweb
9. tuned signature; — wenzelm / hgweb
10. tuned imports; — wenzelm / hgweb
11. add module for faster scheduled builds; — Fabian Huch <huch@in.tum.de> / hgweb
12. always use host database and make protected; — Fabian Huch <huch@in.tum.de> / hgweb
13. read relative cpu from build log; — Fabian Huch <huch@in.tum.de> / hgweb
14. prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway); — Fabian Huch <huch@in.tum.de> / hgweb
15. added start date to build jobs, e.g., for build time estimation; — Fabian Huch <huch@in.tum.de> / hgweb
16. added initial version of benchmark module, e.g., to compare performance of different hosts;
    added benchmark operation to build cluster; — Fabian Huch <huch@in.tum.de> / hgweb
17. generalized node infos: allow addressing of numa node segments via relative cpus;
    add more node options and process policy options using taskset as alternative to NUMA for more fine-grained cpu controls (e.g., for cpus with heterogeneous cores in the same NUMA segment); — Fabian Huch <huch@in.tum.de> / hgweb
18. add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning); — Fabian Huch <huch@in.tum.de> / hgweb
19. added Range object to Host, e.g. to parse/unparse NUMA node ranges; — Fabian Huch <huch@in.tum.de> / hgweb
20. defined statically known tables of Build_Log;
    read hostname from build logs, store in Session_Entry (e.g., to track hosts in distributed build); — Fabian Huch <huch@in.tum.de> / hgweb

#2043 (Oct 28, 2023, 12:50:09 AM)

1. added lemma — nipkow / hgweb
2. added lemma — nipkow / hgweb
3. added lemma — nipkow / hgweb

#2042 (Oct 27, 2023, 12:50:10 AM)

1. NEWS and CONTRIBUTORS; — Fabian Huch <huch@in.tum.de> / hgweb
2. remove unused ci-extras component; — Fabian Huch <huch@in.tum.de> / hgweb
3. use mail module in CI build; — Fabian Huch <huch@in.tum.de> / hgweb
4. added mail module; — Fabian Huch <huch@in.tum.de> / hgweb
5. build javamail component and add to main components; — Fabian Huch <huch@in.tum.de> / hgweb
6. added component for javax mail; — Fabian Huch <huch@in.tum.de> / hgweb

#2041 (Oct 26, 2023, 12:50:09 AM)

1. updated to vampire-4.8; — wenzelm / hgweb
2. tuned README; — wenzelm / hgweb
3. update Vampire version, following hints by Martin Desharnais; — wenzelm / hgweb
4. removed junk; — wenzelm / hgweb
5. tuned component_vampire script for Vampire 4.8 and added new flag to force version name — desharna / hgweb

#2040 (Oct 25, 2023, 12:50:09 AM)

1. prefer Isabelle options for CI mail settings over ci.properties; — Fabian Huch <huch@in.tum.de> / hgweb

#2039 (Oct 24, 2023, 12:50:08 AM)

1. Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal. — paulson <lp15@cam.ac.uk> / hgweb
2. proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e); — wenzelm / hgweb
3. unused (see fe9e590ae52f); — wenzelm / hgweb
4. clarified modules; — wenzelm / hgweb

#2038 (Oct 23, 2023, 1:28:51 AM)

1. merged — wenzelm / hgweb
2. update documentation on simproc_setup; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb
4. proper morphism; — wenzelm / hgweb
5. simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe); — wenzelm / hgweb
6. more compact ML source; — wenzelm / hgweb
7. more robust read_simproc_spec: proper error positions; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. more standard simproc_setup using ML antiquotation; — wenzelm / hgweb
10. more standard simproc_setup using ML antiquotation; — wenzelm / hgweb
11. more standard simproc_setup using ML antiquotation; — wenzelm / hgweb
12. added ML antiquotation "simproc_setup"; — wenzelm / hgweb
13. clarified signature; — wenzelm / hgweb
14. clarified signature;
    clarified modules; — wenzelm / hgweb
15. tuned signature; — wenzelm / hgweb
16. tuned signature; — wenzelm / hgweb
17. clarified signature; — wenzelm / hgweb
18. clarified syntax and order of parameters; — wenzelm / hgweb
19. clarified signature: Named_Target.setup works both for global and local theory; — wenzelm / hgweb
20. clarified signature;
    clarified modules; — wenzelm / hgweb
21. clarified signature: more concise simproc setup in ML; — wenzelm / hgweb
22. clarified signature: more concise variations on implicit theory setup; — wenzelm / hgweb
23. clarified simproc_setup (passive); — wenzelm / hgweb
24. clarified 'simproc_setup'; — wenzelm / hgweb
25. support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet); — wenzelm / hgweb
26. more standard simproc_setup in Isar;
    recovered examples from dead comments; — wenzelm / hgweb
27. more standard ML setup;
    proper tracing messages depending on context option, not Unsynchronized.ref;
    tuned whitespace; — wenzelm / hgweb

#2037 (Oct 21, 2023, 12:50:09 AM)

1. proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0 — desharna / hgweb

#2036 (Oct 19, 2023, 12:50:10 AM)

1. added new portfolio for Vampire 4.8 — desharna / hgweb

#2035 (Oct 18, 2023, 12:50:08 AM)

1. tuned signature, following Isabelle/Scala; — wenzelm / hgweb
2. more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt; — wenzelm / hgweb
3. tuned; — wenzelm / hgweb

#2034 (Oct 17, 2023, 12:50:08 AM)

1. proper parallel build tasks; — wenzelm / hgweb

#2033 (Oct 16, 2023, 12:50:09 AM)

1. more Haskell tests on macOS; — wenzelm / hgweb
2. more NEWS; — wenzelm / hgweb
3. disable naproche component for now: to be updated before the next Isabelle release; — wenzelm / hgweb
4. updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell");
   enforce rebuild of Isabelle/Pure and thus all Haskell applications; — wenzelm / hgweb

#2032 (Oct 15, 2023, 2:10:56 AM)

1. more NEWS; — wenzelm / hgweb
2. tuned structure; — wenzelm / hgweb
3. update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina; — wenzelm / hgweb
4. updated to official release of polyml-5.9.1, based on Ubuntu 18.04 LTS and macOS 11 Big Sur; — wenzelm / hgweb
5. proper options for macOS 11 Big Sur; — wenzelm / hgweb
6. support for official release of polyml-5.9.1; — wenzelm / hgweb
7. updated Linux baseline to Ubuntu 18.04; — wenzelm / hgweb
8. support for macOS 14 Sonoma (only for testing); — wenzelm / hgweb
9. more platform tests: initial support for macOS 14 Sonoma; — wenzelm / hgweb
10. updated to gmp-6.3.0, for the sake of macOS 14 Sonoma; — wenzelm / hgweb

#2031 (Oct 13, 2023, 2:44:43 AM)

1. merged — wenzelm / hgweb
2. prefer Exn.result: avoid accidental capture of interrupts, similar to ML; — wenzelm / hgweb
3. clarified user errors vs. failures, e.g. java.lang.StackOverflowError; — wenzelm / hgweb
4. further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt; — wenzelm / hgweb
5. proper Exn.capture with check_interrupt (amending a3dcae9a2ebe); — wenzelm / hgweb
6. distinguish proper interrupts from Poly/ML RTS breakdown; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb
9. proper Isabelle_Thread.try_catch; — wenzelm / hgweb
10. tuned; — wenzelm / hgweb
11. proper Exn.capture / Isabelle_Thread.try_catch; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. clarified signature; — wenzelm / hgweb
14. proper Exn.capture; — wenzelm / hgweb
15. more robust: avoid race condition; — wenzelm / hgweb
16. clarified name; — wenzelm / hgweb
17. clarified signature; — wenzelm / hgweb
18. clarified comments; — wenzelm / hgweb
19. Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts — paulson <lp15@cam.ac.uk> / hgweb
20. atin now an abbreviation for atin_within, which has been moved to Abstract_Limits — paulson <lp15@cam.ac.uk> / hgweb

#2030 (Oct 12, 2023, 12:50:11 AM)

1. merged — paulson / hgweb
2. New proofs also some slightly faster existing proofs — paulson <lp15@cam.ac.uk> / hgweb

#2029 (Oct 11, 2023, 12:50:06 AM)

1. updated to hugo-0.119.0; — Fabian Huch <huch@in.tum.de> / hgweb
2. add component build tool for hugo from afp-devel; — Fabian Huch <huch@in.tum.de> / hgweb
3. removed test failing on some platform — desharna / hgweb

#2028 (Oct 10, 2023, 12:50:08 AM)

1. mini2 is not active due to upgrade; — wenzelm / hgweb
2. more PLATFORMS; — wenzelm / hgweb

#2027 (Oct 9, 2023, 2:12:45 AM)

1. update documentation on Isabelle/ML exceptions; — wenzelm / hgweb
2. misc tuning; — wenzelm / hgweb
3. discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error); — wenzelm / hgweb
4. proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b); — wenzelm / hgweb
5. proper Scala version, e.g. for IntelliJ IDEA; — wenzelm / hgweb

#2026 (Oct 4, 2023, 12:50:09 AM)

1. NEWS — desharna / hgweb
2. used standard Time.compare in Sledgehammer's preplay — desharna / hgweb

#2025 (Sep 30, 2023, 3:59:55 AM)

1. moved variable bindings to tighter scope — desharna / hgweb
2. removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer — desharna / hgweb
3. removed unused function parameter — desharna / hgweb
4. merged — paulson / hgweb
5. A couple of new lemmas — paulson <lp15@cam.ac.uk> / hgweb
6. merged — wenzelm / hgweb
7. more NEWS; — wenzelm / hgweb
8. explicitly reject 'handle' with catch-all patterns; — wenzelm / hgweb
9. avoid accidental 'handle' of interrupts; — wenzelm / hgweb
10. tuned: prefer try-catch/finally over low-level 'handle'; — wenzelm / hgweb
11. clarified treatment of exceptions: avoid catch-all handlers; — wenzelm / hgweb
12. clarified output vs. error: presence of error messages means error (see also cb7264721c91); — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. more robust management of resources, using Thread_Attributes.uninterruptible; — wenzelm / hgweb
15. tuned; — wenzelm / hgweb
16. clarified signature; — wenzelm / hgweb
17. more robust management of resources, using Thread_Attributes.uninterruptible; — wenzelm / hgweb
18. tuned; — wenzelm / hgweb
19. tuned; — wenzelm / hgweb
20. tuned signature; — wenzelm / hgweb
21. clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet); — wenzelm / hgweb
22. clarified signature; — wenzelm / hgweb
23. clarified modules; — wenzelm / hgweb
24. unused; — wenzelm / hgweb
25. clarified order of modules: early access to interrupt management of Isabelle_Threads; — wenzelm / hgweb
26. tuned: prefer antiquotation for try-catch; — wenzelm / hgweb
27. tuned: prefer antiquotation for try-catch; — wenzelm / hgweb
28. tuned: prefer antiquotation for try-finally; — wenzelm / hgweb
29. omit pointless capture/release (see also 469a375212c1); — wenzelm / hgweb
30. omit pointless capture/release (see also 26774ccb1c74); — wenzelm / hgweb
31. clarified signature: avoid association with potentially dangerous Exn.capture; — wenzelm / hgweb
32. more robust: catch/finally part is uninterruptible; — wenzelm / hgweb
33. more position information, e.g. for warning about fn-pattern; — wenzelm / hgweb
34. unused; — wenzelm / hgweb
35. more general ML_Antiquotation.special_form;
    more general "try" forms: support 'finally' or 'catch'; — wenzelm / hgweb

#2024 (Sep 28, 2023, 12:50:10 AM)

1. Importing or moving a few more useful theorems — paulson <lp15@cam.ac.uk> / hgweb

#2023 (Sep 27, 2023, 12:50:07 AM)

1. merged — paulson / hgweb
2. A few new theorems — paulson <lp15@cam.ac.uk> / hgweb

#2022 (Sep 26, 2023, 12:50:09 AM)

1. avoid legacy binding errors in Sledgehammer Isar proofs — blanchet / hgweb
2. parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition — blanchet / hgweb
3. added argo — blanchet / hgweb
4. allow (~) syntax in TPTP proofs for unapplied negation — blanchet / hgweb
5. reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs — blanchet / hgweb
6. use same associativity as Isabelle when parsing HOL proofs — blanchet / hgweb
7. improved Sledgehammer's HOL proof parser w.r.t. negation — blanchet / hgweb

#2021 (Sep 25, 2023, 1:23:55 AM)

1. clarified signature; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. minor performance tuning; — wenzelm / hgweb

#2020 (Sep 24, 2023, 12:50:07 AM)

1. merged — paulson / hgweb
2. A few new or simplified proofs — paulson <lp15@cam.ac.uk> / hgweb

#2019 (Sep 23, 2023, 12:50:09 AM)

1. tuned: more standard order; — wenzelm / hgweb
2. clarified signature;
   update component; — wenzelm / hgweb

#2018 (Sep 22, 2023, 4:46:47 AM)

1. proper fontenc for cartouches (amending d052d61da398); — wenzelm / hgweb
2. clarified modules;
   clarified signature; — wenzelm / hgweb
3. clarified signature; — wenzelm / hgweb
4. clarified modules; — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. more robust: prefer linear data flow; — wenzelm / hgweb

#2017 (Sep 21, 2023, 12:50:07 AM)

1. added first proof reconstruction test for Sledgehammer — desharna / hgweb

#2016 (Sep 20, 2023, 1:32:11 AM)

1. tuned; — wenzelm / hgweb
2. clarified signature; — wenzelm / hgweb
3. clarified signature (again): follow Isabelle/Java/Scala; — wenzelm / hgweb
4. tuned (following 69c6d3e87660); — wenzelm / hgweb
5. tuned --- avoid pointless indirection (see also a2df9de46060); — wenzelm / hgweb

#2015 (Sep 18, 2023, 12:50:10 AM)

1. (pointlessly) get rid of some simp calls within "proof" — paulson <lp15@cam.ac.uk> / hgweb

#2014 (Sep 17, 2023, 12:50:11 AM)

1. reduced prominence of lemma names — haftmann / hgweb
2. new formulation of an auxiliary lemma — haftmann / hgweb

#2013 (Sep 16, 2023, 2:33:20 AM)

1. A few more inclusion-exclusion theorems from HOL Light — paulson <lp15@cam.ac.uk> / hgweb

#2012 (Sep 15, 2023, 12:50:08 AM)

1. Corrected type calculation. — haftmann / hgweb
2. some hints on managed installations — haftmann / hgweb
3. prefer cartouches over quotes for clarity of resulting document — haftmann / hgweb

#2011 (Sep 13, 2023, 12:50:10 AM)

1. A little reorganisation — paulson <lp15@cam.ac.uk> / hgweb
2. post-release updates; — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. Added tag Isabelle2023 for changeset b5f3d1051b13 — wenzelm / hgweb
5. tuned; — wenzelm / hgweb
6. misc tuning; — wenzelm / hgweb
7. documentation for the "Document" panel in Isabelle/jEdit; — wenzelm / hgweb

#2010 (Sep 11, 2023, 1:57:04 AM)

1. Loads of new material related to porting the Euler Polyhedron Formula from HOL Light — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. merged — paulson / hgweb
4. tidying up old apply-style proofs — paulson <lp15@cam.ac.uk> / hgweb

#2009 (Sep 8, 2023, 12:50:08 AM)

1. allow higher-order unification of open terms (reviewed by Larry Paulson) — Kevin Kappelmann <kevin.kappelmann@tum.de> / hgweb

#2008 (Sep 7, 2023, 2:25:34 AM)

1. merged — wenzelm / hgweb
2. clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML; — wenzelm / hgweb
3. add ML_system_pp for type Isabelle_Thread.T; — wenzelm / hgweb
4. more explicit type Isabelle_Thread.T;
   total operation Isabelle_Thread.self: upgrade raw ML threads implicitly; — wenzelm / hgweb
5. discontinue somewhat pointless thread tracing/debugging: without PIDE command context, messages are not shown, and Exn.trace hardly works anyway (see also de20fccf6509 and 447972249785);
   prefer Isabelle_Thread.fork; — wenzelm / hgweb
6. tuned whitespace; — wenzelm / hgweb

#2007 (Sep 6, 2023, 12:50:08 AM)

1. tuned Sledgehammer messages — blanchet / hgweb
2. respect timeout better — blanchet / hgweb

#2004 (Aug 26, 2023, 12:50:07 AM)

1. avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer — blanchet / hgweb
2. merged — paulson / hgweb
3. some refinements in Algebra and Number_Theory — paulson <lp15@cam.ac.uk> / hgweb
4. provide Go component — Lars Hupel <lars.hupel@mytum.de> / hgweb

#2003 (Aug 24, 2023, 12:50:06 AM)

1. merged — paulson / hgweb
2. A subtle fix involving the "measurable" attribute — paulson <lp15@cam.ac.uk> / hgweb
3. merged — paulson / hgweb
4. Numerous minor tweaks and simplifications — paulson <lp15@cam.ac.uk> / hgweb
5. substantial tidy-up, shortening many proofs — paulson <lp15@cam.ac.uk> / hgweb
6. add Go component — Lars Hupel <lars@hupel.info> / hgweb

#2002 (Aug 14, 2023, 12:50:11 AM)

1. backed out changeset 2a26d423d9fb: build_log_database not run yet, so this tests the same changesets again; — wenzelm / hgweb

#2001 (Aug 11, 2023, 12:50:08 AM)

1. back to post-release mode -- after fork point; — wenzelm / hgweb
2. Added tag Isabelle2023-RC3 for changeset f5fb5bb2533f — wenzelm / hgweb
3. clarified option name (see also ff43a524aa5d); — wenzelm / hgweb
4. more thorough ML_Heap.restore: include ancestors;                                                         prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy; — wenzelm / hgweb
5. more robust: atomic file-system result via tmp file; — wenzelm / hgweb
6. removed junk (amending 8cd399b25dac); — wenzelm / hgweb
7. more robust wrt. undefined state; — wenzelm / hgweb
8. more informative error; — wenzelm / hgweb
9. more robust; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. clarified signature: more explicit types; — wenzelm / hgweb
12. more informative shasum: show differences explicitly; — wenzelm / hgweb
13. tuned messages; — wenzelm / hgweb
14. more robust ancestor_results: avoid total existence failure after build_process has crashed elsewhere; — wenzelm / hgweb
15. clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling; — wenzelm / hgweb

#2000 (Aug 10, 2023, 12:50:10 AM)

1. merged — nipkow / hgweb
2. improved simp rule insert_Times_insert (following Dominique Unruh). — nipkow / hgweb
3. afford multiple tests for arm64_32-darwin on this fast machine; — wenzelm / hgweb
4. proper history_base for AMR64; — wenzelm / hgweb
5. tuned — nipkow / hgweb

#1999 (Aug 9, 2023, 12:50:10 AM)

1. more robust support for ARM64 platform; — wenzelm / hgweb
2. proper support for Apple Silicon (ARM64); — wenzelm / hgweb
3. merged — wenzelm / hgweb
4. tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state; — wenzelm / hgweb
5. proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure; — wenzelm / hgweb
6. proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of; — wenzelm / hgweb
7. made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch) — traytel / hgweb
8. made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch) — traytel / hgweb

#1998 (Aug 8, 2023, 12:50:10 AM)

1. systematic testing of arm64_32-darwin; — wenzelm / hgweb
2. more hardware details; — wenzelm / hgweb

#1997 (Aug 7, 2023, 12:50:09 AM)

1. update to polyml-219e0a248f70, with more robust support for ARM64; — wenzelm / hgweb
2. tuned generated README; — wenzelm / hgweb
3. merged — paulson / hgweb
4. Tidied up more messy proofs — paulson <lp15@cam.ac.uk> / hgweb
5. hints on "hg bisect"; — wenzelm / hgweb
6. no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds; — wenzelm / hgweb

#1996 (Aug 5, 2023, 12:50:10 AM)

1. Removal of ugly old proofs — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. More cosmetic changes — paulson <lp15@cam.ac.uk> / hgweb
4. Cosmetic polishing of proofs — paulson <lp15@cam.ac.uk> / hgweb

#1995 (Aug 2, 2023, 12:50:07 AM)

1. remove debug printing — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb

#1994 (Jul 28, 2023, 12:50:08 AM)

1. merged — nipkow / hgweb
2. added mbox-like latex sugar — nipkow / hgweb

#1993 (Jul 27, 2023, 12:50:09 AM)

1. Added tag Isabelle2023-RC2 for changeset 53b59fa42696 — wenzelm / hgweb
2. prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a); — wenzelm / hgweb
3. revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion); — wenzelm / hgweb
4. output panel: don't discard already filtered messages — kleing / hgweb
5. merged — wenzelm / hgweb
6. tuned signature: more operations; — wenzelm / hgweb
7. avoid excessive accumulation of garbage, for profiling of huge sessions; — wenzelm / hgweb
8. clarified signature: systematic use of Properties.make_string; — wenzelm / hgweb
9. tuned; — wenzelm / hgweb
10. support for let in Alethe name bindings; — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb
11. merged — paulson / hgweb
12. A few more cosmetic changes to proofs — paulson <lp15@cam.ac.uk> / hgweb
13. merged — paulson / hgweb
14. tidying a few proofs a bit  more — paulson <lp15@cam.ac.uk> / hgweb
15. partly tidied some truly horrible proofs — paulson <lp15@cam.ac.uk> / hgweb

#1992 (Jul 26, 2023, 12:50:07 AM)

1. update for release; — wenzelm / hgweb
2. back out 9d5e2a08ba1b, hoping the server room stays sufficiently cool; — wenzelm / hgweb
3. performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers); — wenzelm / hgweb
4. clarified statistics; — wenzelm / hgweb

#1991 (Jul 25, 2023, 12:50:07 AM)

1. show more build history for AFP; — wenzelm / hgweb
2. more statistics; — wenzelm / hgweb
3. proper base_thys; — wenzelm / hgweb
4. more thorough context tracing; — wenzelm / hgweb

#1990 (Jul 24, 2023, 12:50:08 AM)

1. proper check; — wenzelm / hgweb
2. proper symbolic hostname, as provided via Build_Cluster.Host; — wenzelm / hgweb
3. unused; — wenzelm / hgweb
4. clarified signature: Build_Cluster.Session.build_context;
   proper implementation of Build_Cluster.Session.start() based on Build.build_worker_command(); — wenzelm / hgweb
5. clarified exception handling and return_code; — wenzelm / hgweb
6. tuned signature: more operations; — wenzelm / hgweb
7. more robust; — wenzelm / hgweb
8. support for Build_Cluster.Session.init (rsync + Admin/init);
   clarified Build.Results and overall return code; — wenzelm / hgweb
9. prefer Process_Result.RC.merge: strict treatment of interrupt; — wenzelm / hgweb
10. clarified signature: more operations; — wenzelm / hgweb
11. proper afp_root; — wenzelm / hgweb

#1989 (Jul 23, 2023, 12:50:09 AM)

1. clarified signature: more "object-oriented" style; — wenzelm / hgweb
2. more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process; — wenzelm / hgweb
3. clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned signature;
   more operations; — wenzelm / hgweb
6. clarified option (see also b66b6cc1eb8c); — wenzelm / hgweb
7. more build_cluster management: open SSH connections in parallel, but synchronously; — wenzelm / hgweb
8. tuned signature: more options; — wenzelm / hgweb
9. clarified signature: more operations; — wenzelm / hgweb
10. tuned signature; — wenzelm / hgweb
11. more accurate print vs. parse; — wenzelm / hgweb
12. clarified signature;
    tuned output; — wenzelm / hgweb
13. clarified signature (again);
    more explicit "local" name; — wenzelm / hgweb
14. tuned output; — wenzelm / hgweb
15. tuned output; — wenzelm / hgweb
16. clarified modules; — wenzelm / hgweb
17. more pro-forma support for afp_root; — wenzelm / hgweb
18. tuned NEWS: emphasize "isabelle build" add-ons; — wenzelm / hgweb
19. added option -A for AFP root, following "isabelle sync"; — wenzelm / hgweb
20. clarified signature: more operations; — wenzelm / hgweb
21. tuned signature; — wenzelm / hgweb
22. clarified file location: to be used by regular Isabelle/Scala tools; — wenzelm / hgweb
23. update headers; — wenzelm / hgweb
24. more pro-forma support for Build_Cluster; — wenzelm / hgweb
25. tuned; — wenzelm / hgweb
26. tuned; — wenzelm / hgweb
27. clarified options; — wenzelm / hgweb
28. clarified options; — wenzelm / hgweb
29. proper Build_Cluster.Host.parse for parameters and system options;
    clarified Build_Cluster.Host: empty "host" means local; — wenzelm / hgweb
30. more operations for independent "inline" options; — wenzelm / hgweb
31. clarified options: accommodate potentially slow database connection; — wenzelm / hgweb
32. minor performance tuning; — wenzelm / hgweb
33. add option "build_context" in anticipation of AFP entries that require special tricks in Isabelle/ML (NB: system component settings are unavailable in AFP); — wenzelm / hgweb
34. proper build_options (amending 822ddccda899); — wenzelm / hgweb
35. clarified options; — wenzelm / hgweb
36. proforma support for remote build hosts; — wenzelm / hgweb

#1988 (Jul 19, 2023, 12:50:06 AM)

1. more options for performance tuning; — wenzelm / hgweb
2. more operations; — wenzelm / hgweb
3. support for management of build cluster; — wenzelm / hgweb
4. clarified modules; — wenzelm / hgweb
5. renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database); — wenzelm / hgweb
6. more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh; — wenzelm / hgweb
7. proper running limit, based on this worker process;
   prefer bulk jobs: much faster cancellation; — wenzelm / hgweb
8. more robust: implicit locking of tables in standard order; — wenzelm / hgweb
9. more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked; — wenzelm / hgweb
10. removed unused "create_index": implicit index from primary_key is usually sufficient; — wenzelm / hgweb
11. clarified "vacuum" (again, reverting 0bd366fad888); — wenzelm / hgweb
12. clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888); — wenzelm / hgweb
13. update for release; — wenzelm / hgweb

#1987 (Jul 18, 2023, 12:50:10 AM)

1. merged — wenzelm / hgweb
2. more elementary transaction implementation (despite fda3f7a158b9 and 9da65bc75610); — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. proper check (amending 234f2ff9afe6); — wenzelm / hgweb
5. more robust: exclude accidental nesting (synchronized block is re-entrant); — wenzelm / hgweb
6. clarified errors; — wenzelm / hgweb
7. removed junk (amending f8e3b228670c); — wenzelm / hgweb
8. tuned output; — wenzelm / hgweb
9. reuse SSH.Server connection for database server; — wenzelm / hgweb
10. tuned source structure; — wenzelm / hgweb
11. clarified check: uniform session_info_exists; — wenzelm / hgweb
12. more complete check; — wenzelm / hgweb
13. clarified signature: more specific exists_table --- avoid retrieving full list beforehand; — wenzelm / hgweb
14. reuse database_server connection; — wenzelm / hgweb
15. more informative trace; — wenzelm / hgweb
16. reuse SSH.Server connection database server; — wenzelm / hgweb
17. tuned output; — wenzelm / hgweb
18. make double-sure that this is a transaction context, notably for LOCK TABLE; — wenzelm / hgweb
19. more robust Java/Scala multithreading: transaction is always connection.synchronized; — wenzelm / hgweb
20. clarified signature: proper Scala function for command-line tool; — wenzelm / hgweb
21. tuned signature; — wenzelm / hgweb
22. clarified signature: more operations; — wenzelm / hgweb
23. more standard time unit; — wenzelm / hgweb
24. clarified options; — wenzelm / hgweb
25. tuned output; — wenzelm / hgweb
26. global transaction_count; — wenzelm / hgweb
27. tuned output; — wenzelm / hgweb
28. tuned output; — wenzelm / hgweb
29. prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job"); — wenzelm / hgweb
30. clarified isabelle.transaction_log: support time_min (in ms); — wenzelm / hgweb
31. more operations; — wenzelm / hgweb
32. more informative trace; — wenzelm / hgweb
33. support trace of transaction_lock via property "isabelle.transaction_log"; — wenzelm / hgweb
34. proper db.transaction_lock instead of adhoc clone (amending 2df0f3604a67); — wenzelm / hgweb
35. tuned; — wenzelm / hgweb
36. proper close() operation; — wenzelm / hgweb
37. tuned comments; — wenzelm / hgweb
38. more robust: avoid nested transactions (on disjoint tables); — wenzelm / hgweb
39. potentially more robust: long-running operation only for build master, not workers; — wenzelm / hgweb
40. less ambitions transactions (amending 3f3dcf9f53f1): TRANSACTION_SERIALIZABLE may lead to spurious rollback exceptions; — wenzelm / hgweb
41. clarified signature: more operations; — wenzelm / hgweb
42. clarified signature: more operations; — wenzelm / hgweb
43. clarified signature; — wenzelm / hgweb
44. clarified signature; — wenzelm / hgweb
45. clarified signature: follow Store.open_database; — wenzelm / hgweb
46. tuned; — wenzelm / hgweb
47. clarified signature; — wenzelm / hgweb
48. clarified signature: more uniform SSH.Port_Forwarding; — wenzelm / hgweb
49. tuned signature; — wenzelm / hgweb

#1986 (Jul 17, 2023, 12:50:08 AM)

1. X = trivial_topology rather than topspace X = {} — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. trivial_topology — paulson <lp15@cam.ac.uk> / hgweb

#1985 (Jul 15, 2023, 12:50:07 AM)

1. merged; — Lukas Stevens <mail@lukas-stevens.de> / hgweb
2. added docs for order method in Orderings;
   
   The order method is now tried by try0.
   This adds some documentation for users of try0 that stumble over the order method — Lukas Stevens <mail@lukas-stevens.de> / hgweb
3. News update referring to Analysis — paulson <lp15@cam.ac.uk> / hgweb
4. tuned error message; — Fabian Huch <huch@in.tum.de> / hgweb

#1984 (Jul 14, 2023, 12:50:08 AM)

1. more NEWS; — wenzelm / hgweb
2. tuned output; — wenzelm / hgweb
3. tuned output; — wenzelm / hgweb
4. clarified session_statistics: removed somewhat pointless per-theory statistics; — wenzelm / hgweb
5. tuned error messages; — Fabian Huch <huch@in.tum.de> / hgweb
6. more TOML formatting functions; — Fabian Huch <huch@in.tum.de> / hgweb
7. merged — paulson / hgweb
8. Doubled the time limit for HOL-Probability — paulson <lp15@cam.ac.uk> / hgweb
9. merged — paulson / hgweb
10. Some fixes, and SOME TIME LIMITS — paulson <lp15@cam.ac.uk> / hgweb
11. merged — paulson / hgweb
12. cosmetic improvements, new lemmas, especially more uses of function space — paulson <lp15@cam.ac.uk> / hgweb
13. more NEWS; — wenzelm / hgweb
14. NEWS; — wenzelm / hgweb
15. tuned whitespace; — wenzelm / hgweb
16. added TOML module from afp; — Fabian Huch <huch@in.tum.de> / hgweb
17. proper system integration and renaming; — wenzelm / hgweb
18. copy/rename files from private autocorres version e45b9b680d3e; — wenzelm / hgweb
19. Added tag Isabelle2023-RC1 for changeset 006dbc9c2de1 — wenzelm / hgweb
20. update cygwin component; — wenzelm / hgweb
21. avoid bloat of approx. 300MB due to implicit dependency on python; — wenzelm / hgweb
22. suppress bad file, which does not work on regular Windows; — wenzelm / hgweb
23. revert ineffective b04ac8a017b2: etc/settings of polyml components needs to be changed as well; — wenzelm / hgweb
24. updated naproche-20230711 component for release; — wenzelm / hgweb
25. clarified signature; — wenzelm / hgweb
26. ML_system_apple=false for more stability; — wenzelm / hgweb
27. activate cygwin-20230711; — wenzelm / hgweb
28. update cygwin for Isabelle2023 -- somewhere after cygwin 3.4.0-1 (see https://cygwin.com/pipermail/cygwin-announce/2022-December/010821.html); — wenzelm / hgweb
29. proper set_executable for sqlitejdbc.dll (see also 3b0f8f1010f2); — wenzelm / hgweb
30. update to stack-2.9.3 with support for arm64-linux; — wenzelm / hgweb
31. provide tool for GHC stack component; — wenzelm / hgweb
32. tuned signature; — wenzelm / hgweb
33. "rlwrap" is back together with "perl", which is actually required for bib2xhtml; — wenzelm / hgweb
34. clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4); — wenzelm / hgweb
35. tuned; — wenzelm / hgweb
36. tuned; — wenzelm / hgweb
37. merged — wenzelm / hgweb
38. tuned; — wenzelm / hgweb
39. update for release; — wenzelm / hgweb
40. tuned; — wenzelm / hgweb
41. update for release; — wenzelm / hgweb
42. merged; — wenzelm / hgweb
43. publish component; — wenzelm / hgweb
44. latest version; — wenzelm / hgweb
45. update to current sqlite-jdbc-3.42.0.0; — wenzelm / hgweb
46. update to current lipics-3.1.3; — wenzelm / hgweb
47. update to flatlaf-2.6, which is the last release before recent moves towards 3.0 / 3.1 / 3.1.1; — wenzelm / hgweb
48. merged — paulson / hgweb
49. more small simplifications — paulson <lp15@cam.ac.uk> / hgweb
50. merged — wenzelm / hgweb
51. merged — wenzelm / hgweb
52. clarified modules (amending 570f65953173); — wenzelm / hgweb
53. more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax; — wenzelm / hgweb
54. create database view for diagnostic purposes; — wenzelm / hgweb
55. A bit of prerelease tidying — paulson <lp15@cam.ac.uk> / hgweb
56. NEWS tweak — paulson <lp15@cam.ac.uk> / hgweb
57. merged — paulson / hgweb
58. Last of the HOL Light metric space imports, and some supporting lemmas — paulson <lp15@cam.ac.uk> / hgweb
59. clarified "vacuum" operation for various database versions (PostgreSQL <= 10 is strictly speaking obsolete, but still used on some test machines); — wenzelm / hgweb
60. eliminate somewhat obsolete augment_tables (see ff164add75cd), to support obsolete versions 10 and 9.x; — wenzelm / hgweb
61. clarified operation: sequential vacuum to support obsolete versions 10 and 9.x; — wenzelm / hgweb
62. clarified operation: empty means "empty" instead of "full"; — wenzelm / hgweb
63. merged — wenzelm / hgweb
64. proper data_domain for symmetric difference; — wenzelm / hgweb
65. tuned: avoid redundant db access; — wenzelm / hgweb
66. clarified signature; — wenzelm / hgweb
67. proper transaction_lock;
    clarified signature; — wenzelm / hgweb
68. clarified signature: ensure disjoint data spaces; — wenzelm / hgweb
69. clarified signature; — wenzelm / hgweb
70. tuned; — wenzelm / hgweb
71. unused (see also ea35afdb1366); — wenzelm / hgweb
72. more robust transaction_lock: avoid overlapping data spaces;
    clarified modules; — wenzelm / hgweb
73. merged — paulson / hgweb
74. The sym_diff operator (symmetric difference) — paulson <lp15@cam.ac.uk> / hgweb
75. disable lxbroy10 for now: technical problems with cooling; — wenzelm / hgweb

#1983 (Jul 7, 2023, 12:50:08 AM)

1. A couple of new lemmas involving cardinality — paulson <lp15@cam.ac.uk> / hgweb

#1982 (Jul 6, 2023, 12:50:07 AM)

1. merged — wenzelm / hgweb
2. tuned; — wenzelm / hgweb
3. more robust; — wenzelm / hgweb
4. proper build_progress for local messages; — wenzelm / hgweb
5. proper SQL query; — wenzelm / hgweb
6. Another tranche of HOL Light material on metric and topological spaces — paulson <lp15@cam.ac.uk> / hgweb

#1981 (Jul 4, 2023, 12:50:10 AM)

1. merged — paulson / hgweb
2. EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis — paulson <lp15@cam.ac.uk> / hgweb

#1980 (Jul 3, 2023, 12:50:08 AM)

1. merged — wenzelm / hgweb
2. more robust "stop": further "stamp" ticks may happen afterwards; — wenzelm / hgweb
3. removed junk; — wenzelm / hgweb
4. tuned signature; — wenzelm / hgweb
5. tuned: prefer Scala over Java; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. tuned; — wenzelm / hgweb
8. more SQL data; — wenzelm / hgweb
9. add proof method "order" to command "try0" — desharna / hgweb

#1979 (Jul 2, 2023, 12:50:07 AM)

1. tuned signature; — wenzelm / hgweb
2. clarified static Build_Process.Context vs. dynamic Build_Process.State;
   more dynamic Build_Process.Sessions, to accomodate multiple workers (and multiple builds); — wenzelm / hgweb
3. tuned signature: more operations; — wenzelm / hgweb
4. clarified signature: proper equals/hashCode; — wenzelm / hgweb
5. more robust database setup; — wenzelm / hgweb
6. clarified signature; — wenzelm / hgweb
7. clarified signature; — wenzelm / hgweb

#1978 (Jul 1, 2023, 12:50:08 AM)

1. New theory Leftist_Heap_List — nipkow / hgweb
2. added [simp] — nipkow / hgweb

#1977 (Jun 29, 2023, 12:50:07 AM)

1. merged — wenzelm / hgweb
2. proper build_master.build_uuid; — wenzelm / hgweb
3. proper session_init *after* deleting db files (amending af6c493b0441); — wenzelm / hgweb
4. clarified signature: more concise data; — wenzelm / hgweb
5. tuned output; — wenzelm / hgweb
6. more robust; — wenzelm / hgweb
7. clarified signature: better default; — wenzelm / hgweb
8. show only active builds; — wenzelm / hgweb
9. clarified output; — wenzelm / hgweb
10. tuned; — wenzelm / hgweb
11. support for identified builds;
    more complete implementation of "isabelle build_worker"; — wenzelm / hgweb
12. clarified signature: more operations and options; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. clarified signature; — wenzelm / hgweb
15. clarified signature; — wenzelm / hgweb
16. more robust close() after failed initialization; — wenzelm / hgweb
17. avoid repeated open_database_server: synchronized transaction_lock; — wenzelm / hgweb
18. tuned signature; — wenzelm / hgweb
19. more robust: proper transaction_lock; — wenzelm / hgweb
20. tuned signature; — wenzelm / hgweb
21. tuned signature; — wenzelm / hgweb
22. tuned signature; — wenzelm / hgweb
23. clarified signature: more options; — wenzelm / hgweb
24. tuned; — wenzelm / hgweb
25. clarified database for heaps: do not depend on build_database_test; — wenzelm / hgweb
26. clarified signature; — wenzelm / hgweb
27. tuned signature; — wenzelm / hgweb

#1976 (Jun 28, 2023, 12:50:06 AM)

1. More metric space material — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. New and generalised analysis lemmas — paulson <lp15@cam.ac.uk> / hgweb

#1975 (Jun 27, 2023, 12:50:09 AM)

1. tuned names — nipkow / hgweb

#1974 (Jun 24, 2023, 12:50:10 AM)

1. clarified signature: prefer explicit combinator; — wenzelm / hgweb
2. unused; — wenzelm / hgweb
3. restore heaps from database, which takes precedence over file-system; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. more operations; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. more robust try-finally; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. proper clean_entry; — wenzelm / hgweb
10. afford larger build_database_slice for better compression (HOL: 1 slice, HOL-Proofs: multiple slices for testing); — wenzelm / hgweb
11. prefer system option; — wenzelm / hgweb
12. clarified signature: more explicit class SQL.Data; — wenzelm / hgweb
13. proper ML_Heap.clean_entry; — wenzelm / hgweb
14. tuned signature; — wenzelm / hgweb
15. tuned; — wenzelm / hgweb
16. store heaps within database server; — wenzelm / hgweb
17. tuned signature; — wenzelm / hgweb
18. clarified modules; — wenzelm / hgweb
19. tuned signature; — wenzelm / hgweb
20. clarified modules; — wenzelm / hgweb
21. clarified modules; — wenzelm / hgweb

#1973 (Jun 20, 2023, 3:12:47 AM)

1. early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals; — Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> / hgweb

#1972 (Jun 18, 2023, 1:24:13 AM)

1. merged — wenzelm / hgweb
2. proper close; — wenzelm / hgweb
3. separate host.db for independent db.transaction_lock; — wenzelm / hgweb
4. tuned comments; — wenzelm / hgweb
5. omit redundant data: already stored in progress database; — wenzelm / hgweb
6. tuned signature: more operations; — wenzelm / hgweb
7. proper support for SQLite: avoid conflicts on transaction_lock; — wenzelm / hgweb
8. minor performance tuning: avoid external process; — wenzelm / hgweb
9. clarified signature; — wenzelm / hgweb
10. obsolete; — wenzelm / hgweb
11. tuned; — wenzelm / hgweb
12. tuned signature; — wenzelm / hgweb
13. tuned signature; — wenzelm / hgweb
14. clarified signature; — wenzelm / hgweb
15. tuned; — wenzelm / hgweb
16. clarified signature; — wenzelm / hgweb
17. tuned; — wenzelm / hgweb
18. proper pattern (amending da5cc332ded3); — wenzelm / hgweb
19. tuned signature; — wenzelm / hgweb
20. proper hostname from build_context; — wenzelm / hgweb
21. prefer Database_Progress, which is more robust (amending afb1a19307c4); — wenzelm / hgweb
22. support for Database_Progress; — wenzelm / hgweb
23. tuned signature: more operations; — wenzelm / hgweb
24. tuned signature: more operations; — wenzelm / hgweb
25. tuned signature: more operations; — wenzelm / hgweb
26. clarified signature; — wenzelm / hgweb

#1971 (Jun 16, 2023, 12:50:10 AM)

1. optional description in Eisbach "method" command; — kleing / hgweb

#1970 (Jun 15, 2023, 12:50:07 AM)

1. disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice — blanchet / hgweb

#1969 (Jun 8, 2023, 12:50:08 AM)

1. Added tag Isabelle2023-RC0 for changeset f4221ae7544c — wenzelm / hgweb
2. updated to zstd-jni-1.5.5-4; — wenzelm / hgweb
3. updated to postgresql-42.6.0; — wenzelm / hgweb
4. back to more concise build_release, thanks to build_host_macos = "mini3"; — wenzelm / hgweb
5. more PLATFORMS; — wenzelm / hgweb
6. updated for release; — wenzelm / hgweb
7. tuned NEWS; — wenzelm / hgweb
8. more realistic factor; — wenzelm / hgweb
9. proper trim_context; — wenzelm / hgweb
10. proper exception positions; — wenzelm / hgweb
11. proper trim_context / transfer, e.g. for Specification.definition; — wenzelm / hgweb
12. tuned; — wenzelm / hgweb
13. tuned; — wenzelm / hgweb
14. tuned signature: more operations; — wenzelm / hgweb
15. minor performance tuning: avoid append to end-of-list; — wenzelm / hgweb

#1968 (Jun 4, 2023, 12:50:09 AM)

1. TN has enough examples of the bug. — nipkow / hgweb

#1967 (Jun 3, 2023, 12:50:06 AM)

1. added lemma ffUnion_fsubset_iff — desharna / hgweb

#1966 (Jun 2, 2023, 12:50:11 AM)

1. Even more material from the HOL Light metric space library — paulson <lp15@cam.ac.uk> / hgweb

#1965 (Jun 1, 2023, 12:50:07 AM)

1. NEWS: Announcing the metric space material — paulson <lp15@cam.ac.uk> / hgweb
2. merged — paulson / hgweb
3. Hiding the constructor names, particularly to avoid conflicts involving "ext" — paulson <lp15@cam.ac.uk> / hgweb
4. New HOL Light material on metric spaces and topological spaces — paulson <lp15@cam.ac.uk> / hgweb
5. enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML; — wenzelm / hgweb
6. provide scala-3.3.0; — wenzelm / hgweb
7. more NEWS; — wenzelm / hgweb
8. tuned NEWS; — wenzelm / hgweb

#1964 (May 31, 2023, 12:50:08 AM)

1. NEWS; — wenzelm / hgweb

#1963 (May 30, 2023, 12:50:10 AM)

1. removed intro, desc, elim, and simp annotations from FSet lemmas that are instances of lemmas in Set — desharna / hgweb

#1962 (May 28, 2023, 2:24:00 AM)

1. merged — desharna / hgweb
2. NEWS — desharna / hgweb
3. set up code generation for fset — desharna / hgweb
4. redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex — desharna / hgweb
5. merged — wenzelm / hgweb
6. tuned signature; — wenzelm / hgweb
7. clarified treatment of context; — wenzelm / hgweb
8. clarified treatment of context; — wenzelm / hgweb
9. more operations; — wenzelm / hgweb

#1961 (May 27, 2023, 12:50:08 AM)

1. NEWS — desharna / hgweb
2. renamed notin_fset to not_fmember — desharna / hgweb
3. added author — desharna / hgweb
4. merged — desharna / hgweb
5. adapted Transfer_Debug from fmember to fempty — desharna / hgweb
6. renamed variables — desharna / hgweb
7. merged — desharna / hgweb
8. fixed lemma name — desharna / hgweb
9. redefined FSet.fmember as an abbreviation based on Set.member — desharna / hgweb
10. replaced some lemmas' implicit formulas by explicit ones to avoid silent changes — desharna / hgweb

#1960 (May 26, 2023, 12:50:08 AM)

1. merged — wenzelm / hgweb
2. proper setup for rule attribute; — wenzelm / hgweb
3. more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure; — wenzelm / hgweb
4. clarified output of embedded values, e.g. for 'print_locale'; — wenzelm / hgweb
5. tuned: more antiquotations; — wenzelm / hgweb
6. tuned; — wenzelm / hgweb
7. tuned signature: more position information; — wenzelm / hgweb
8. tuned; — wenzelm / hgweb

#1959 (May 24, 2023, 12:50:10 AM)

1. Finally, the abstract metric space development — paulson <lp15@cam.ac.uk> / hgweb

#1958 (May 23, 2023, 12:50:08 AM)

1. merged — wenzelm / hgweb
2. misc tuning and clarification; — wenzelm / hgweb
3. tuned signature; — wenzelm / hgweb
4. tuned; — wenzelm / hgweb
5. tuned --- Token.make_string / Token.assign are value-oriented; — wenzelm / hgweb
6. more documentation; — wenzelm / hgweb
7. tuned signature; — wenzelm / hgweb
8. tuned signature; — wenzelm / hgweb
9. more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm); — wenzelm / hgweb
10. prefer static simpset; — wenzelm / hgweb
11. omit pointless morphism in global theory; — wenzelm / hgweb
12. more operations; — wenzelm / hgweb
13. more careful treatment of context for method source; — wenzelm / hgweb
14. clarified context; — wenzelm / hgweb
15. clarified signature; — wenzelm / hgweb
16. remove pointless context setup (see also b2e449c155a4); — wenzelm / hgweb
17. more careful reset_context for stored entity; — wenzelm / hgweb
18. more careful reset/set_context for stored declarations; — wenzelm / hgweb
19. tuned; — wenzelm / hgweb
20. tuned; — wenzelm / hgweb
21. clarified signature: more explicit types; — wenzelm / hgweb
22. clarified data: avoid pointless Morphism.transform; — wenzelm / hgweb
23. proper Token.Declaration for internal_declaration; — wenzelm / hgweb
24. more standard treatment of morphism context; — wenzelm / hgweb
25. tuned: avoid duplication; — wenzelm / hgweb
26. more standard treatment of morphism context, but hardly relevant here; — wenzelm / hgweb
27. tuned; — wenzelm / hgweb
28. more careful treatment of set_context / reset_context for persistent morphisms;
    avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition; — wenzelm / hgweb
29. clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
    clarified signature; — wenzelm / hgweb
30. tuned signature; — wenzelm / hgweb
31. support for context within morphism (for background theory); — wenzelm / hgweb
32. proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs"; — wenzelm / hgweb
33. clarified signature; — wenzelm / hgweb
34. tuned; — wenzelm / hgweb
35. tuned; — wenzelm / hgweb
36. tuned signature; — wenzelm / hgweb
37. more accurate Thm.trim_context / Thm.transfer; — wenzelm / hgweb
38. clarified stored thm: result from notes;
    tuned; — wenzelm / hgweb
39. tuned whitespace; — wenzelm / hgweb
40. clarified signature: avoid convoluted operations; — wenzelm / hgweb
41. tuned signature; — wenzelm / hgweb
42. update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof; — wenzelm / hgweb
43. avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c); — wenzelm / hgweb
44. proper transfer / trim_context; — wenzelm / hgweb
45. more operations "without_context", assuming that the thm has been properly transferred already; — wenzelm / hgweb
46. proper trim_context / transfer; — wenzelm / hgweb
47. tuned: more accurate check (is_norm_hhf protect); — wenzelm / hgweb
48. clarified build options: reduce heap size by approx. 3%; — wenzelm / hgweb
49. more standard merge order, following logical structure of imports rather than physical serials; — wenzelm / hgweb
50. tuned; — wenzelm / hgweb
51. tuned; — wenzelm / hgweb
52. proper Thm.trim_context / Thm.transfer; — wenzelm / hgweb
53. proper Thm.trim_context / Thm.transfer; — wenzelm / hgweb
54. tuned: avoid pointless Proof_Context.init_global of Context.proof_of; — wenzelm / hgweb