#349 (Aug 11, 2023, 10:46:01 AM)

	Changes Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default) back to post-release mode -- after fork point; (detail) Added tag Isabelle2023-RC3 for changeset f5fb5bb2533f (detail) clarified option name (see also ff43a524aa5d); (detail) more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy; (detail) more robust: atomic file-system result via tmp file; (detail) removed junk (amending 8cd399b25dac); (detail) more robust wrt. undefined state; (detail) more informative error; (detail) more robust; (detail) tuned signature; (detail) clarified signature: more explicit types; (detail) more informative shasum: show differences explicitly; (detail) tuned messages; (detail) more robust ancestor_results: avoid total existence failure after build_process has crashed elsewhere; (detail) clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling; (detail) merged (detail) improved simp rule insert_Times_insert (following Dominique Unruh). (detail) afford multiple tests for arm64_32-darwin on this fast machine; (detail) proper history_base for AMR64; (detail) tuned (detail) more robust support for ARM64 platform; (detail) proper support for Apple Silicon (ARM64); (detail) merged (detail) tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state; (detail) proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure; (detail) proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of; (detail) made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch) (detail) made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch) (detail) systematic testing of arm64_32-darwin; (detail) more hardware details; (detail) update to polyml-219e0a248f70, with more robust support for ARM64; (detail) tuned generated README; (detail) merged (detail) Tidied up more messy proofs (detail) hints on "hg bisect"; (detail) no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds; (detail) Removal of ugly old proofs (detail) merged (detail) More cosmetic changes (detail) Cosmetic polishing of proofs (detail) remove debug printing (detail) merged (detail) added mbox-like latex sugar (detail) Added tag Isabelle2023-RC2 for changeset 53b59fa42696 (detail) prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a); (detail) revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion); (detail) output panel: don't discard already filtered messages (detail) merged (detail) tuned signature: more operations; (detail) avoid excessive accumulation of garbage, for profiling of huge sessions; (detail) clarified signature: systematic use of Properties.make_string; (detail) tuned; (detail) support for let in Alethe name bindings; (detail) merged (detail) A few more cosmetic changes to proofs (detail) merged (detail) tidying a few proofs a bit more (detail) partly tidied some truly horrible proofs (detail) update for release; (detail) back out 9d5e2a08ba1b, hoping the server room stays sufficiently cool; (detail) performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers); (detail) clarified statistics; (detail) show more build history for AFP; (detail) more statistics; (detail) proper base_thys; (detail) more thorough context tracing; (detail) proper check; (detail) proper symbolic hostname, as provided via Build_Cluster.Host; (detail) unused; (detail) clarified signature: Build_Cluster.Session.build_context; proper implementation of Build_Cluster.Session.start() based on Build.build_worker_command(); (detail) clarified exception handling and return_code; (detail) tuned signature: more operations; (detail) more robust; (detail) support for Build_Cluster.Session.init (rsync + Admin/init); clarified Build.Results and overall return code; (detail) prefer Process_Result.RC.merge: strict treatment of interrupt; (detail) clarified signature: more operations; (detail) proper afp_root; (detail) clarified signature: more "object-oriented" style; (detail) more flexible Build.Engine.process_options: e.g. to manipulate "process_policy" for ML process; (detail) clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster; (detail) tuned signature; (detail) tuned signature; more operations; (detail) clarified option (see also b66b6cc1eb8c); (detail) more build_cluster management: open SSH connections in parallel, but synchronously; (detail) tuned signature: more options; (detail) clarified signature: more operations; (detail) tuned signature; (detail) more accurate print vs. parse; (detail) clarified signature; tuned output; (detail) clarified signature (again); more explicit "local" name; (detail) tuned output; (detail) tuned output; (detail) clarified modules; (detail) more pro-forma support for afp_root; (detail) tuned NEWS: emphasize "isabelle build" add-ons; (detail) added option -A for AFP root, following "isabelle sync"; (detail) clarified signature: more operations; (detail) tuned signature; (detail) clarified file location: to be used by regular Isabelle/Scala tools; (detail) update headers; (detail) more pro-forma support for Build_Cluster; (detail) tuned; (detail) tuned; (detail) clarified options; (detail) clarified options; (detail) proper Build_Cluster.Host.parse for parameters and system options; clarified Build_Cluster.Host: empty "host" means local; (detail) more operations for independent "inline" options; (detail) clarified options: accommodate potentially slow database connection; (detail) minor performance tuning; (detail) add option "build_context" in anticipation of AFP entries that require special tricks in Isabelle/ML (NB: system component settings are unavailable in AFP); (detail) proper build_options (amending 822ddccda899); (detail) clarified options; (detail) proforma support for remote build hosts; (detail) more options for performance tuning; (detail) more operations; (detail) support for management of build cluster; (detail) clarified modules; (detail) renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database); (detail) more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh; (detail) proper running limit, based on this worker process; prefer bulk jobs: much faster cancellation; (detail) more robust: implicit locking of tables in standard order; (detail) more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked; (detail) removed unused "create_index": implicit index from primary_key is usually sufficient; (detail) clarified "vacuum" (again, reverting 0bd366fad888); (detail) clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888); (detail) update for release; (detail) merged (detail) more elementary transaction implementation (despite fda3f7a158b9 and 9da65bc75610); (detail) tuned signature; (detail) proper check (amending 234f2ff9afe6); (detail) more robust: exclude accidental nesting (synchronized block is re-entrant); (detail) clarified errors; (detail) removed junk (amending f8e3b228670c); (detail) tuned output; (detail) reuse SSH.Server connection for database server; (detail) tuned source structure; (detail) clarified check: uniform session_info_exists; (detail) more complete check; (detail) clarified signature: more specific exists_table --- avoid retrieving full list beforehand; (detail) reuse database_server connection; (detail) more informative trace; (detail) reuse SSH.Server connection database server; (detail) tuned output; (detail) make double-sure that this is a transaction context, notably for LOCK TABLE; (detail) more robust Java/Scala multithreading: transaction is always connection.synchronized; (detail) clarified signature: proper Scala function for command-line tool; (detail) tuned signature; (detail) clarified signature: more operations; (detail) more standard time unit; (detail) clarified options; (detail) tuned output; (detail) global transaction_count; (detail) tuned output; (detail) tuned output; (detail) prefer asynchronous operations: reduce time spent within synchronized_database("Build_Process.start_job"); (detail) clarified isabelle.transaction_log: support time_min (in ms); (detail) more operations; (detail) more informative trace; (detail) support trace of transaction_lock via property "isabelle.transaction_log"; (detail) proper db.transaction_lock instead of adhoc clone (amending 2df0f3604a67); (detail) tuned; (detail) proper close() operation; (detail) tuned comments; (detail) more robust: avoid nested transactions (on disjoint tables); (detail) potentially more robust: long-running operation only for build master, not workers; (detail) less ambitions transactions (amending 3f3dcf9f53f1): TRANSACTION_SERIALIZABLE may lead to spurious rollback exceptions; (detail) clarified signature: more operations; (detail) clarified signature: more operations; (detail) clarified signature; (detail) clarified signature; (detail) clarified signature: follow Store.open_database; (detail) tuned; (detail) clarified signature; (detail) clarified signature: more uniform SSH.Port_Forwarding; (detail) tuned signature; (detail) X = trivial_topology rather than topspace X = {} (detail) merged (detail) trivial_topology (detail) merged; (detail) 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 (detail) News update referring to Analysis (detail) tuned error message; (detail) more NEWS; (detail) tuned output; (detail) tuned output; (detail) clarified session_statistics: removed somewhat pointless per-theory statistics; (detail) tuned error messages; (detail) more TOML formatting functions; (detail) merged (detail) Doubled the time limit for HOL-Probability (detail) merged (detail) Some fixes, and SOME TIME LIMITS (detail) merged (detail) cosmetic improvements, new lemmas, especially more uses of function space (detail) more NEWS; (detail) NEWS; (detail) tuned whitespace; (detail) added TOML module from afp; (detail) proper system integration and renaming; (detail) copy/rename files from private autocorres version e45b9b680d3e; (detail) Added tag Isabelle2023-RC1 for changeset 006dbc9c2de1 (detail) update cygwin component; (detail) avoid bloat of approx. 300MB due to implicit dependency on python; (detail) suppress bad file, which does not work on regular Windows; (detail) revert ineffective b04ac8a017b2: etc/settings of polyml components needs to be changed as well; (detail) updated naproche-20230711 component for release; (detail) clarified signature; (detail) ML_system_apple=false for more stability; (detail) activate cygwin-20230711; (detail) update cygwin for Isabelle2023 -- somewhere after cygwin 3.4.0-1 (see https://cygwin.com/pipermail/cygwin-announce/2022-December/010821.html); (detail) proper set_executable for sqlitejdbc.dll (see also 3b0f8f1010f2); (detail) update to stack-2.9.3 with support for arm64-linux; (detail) provide tool for GHC stack component; (detail) tuned signature; (detail) "rlwrap" is back together with "perl", which is actually required for bib2xhtml; (detail) clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4); (detail) tuned; (detail) tuned; (detail) merged (detail) tuned; (detail) update for release; (detail) tuned; (detail) update for release; (detail) merged; (detail) publish component; (detail) latest version; (detail) update to current sqlite-jdbc-3.42.0.0; (detail) update to current lipics-3.1.3; (detail) update to flatlaf-2.6, which is the last release before recent moves towards 3.0 / 3.1 / 3.1.1; (detail) merged (detail) more small simplifications (detail) merged (detail) merged (detail) clarified modules (amending 570f65953173); (detail) more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax; (detail) create database view for diagnostic purposes; (detail) A bit of prerelease tidying (detail) NEWS tweak (detail) merged (detail) Last of the HOL Light metric space imports, and some supporting lemmas (detail) clarified "vacuum" operation for various database versions (PostgreSQL <= 10 is strictly speaking obsolete, but still used on some test machines); (detail) eliminate somewhat obsolete augment_tables (see ff164add75cd), to support obsolete versions 10 and 9.x; (detail) clarified operation: sequential vacuum to support obsolete versions 10 and 9.x; (detail) clarified operation: empty means "empty" instead of "full"; (detail) merged (detail) proper data_domain for symmetric difference; (detail) tuned: avoid redundant db access; (detail) clarified signature; (detail) proper transaction_lock; clarified signature; (detail) clarified signature: ensure disjoint data spaces; (detail) clarified signature; (detail) tuned; (detail) unused (see also ea35afdb1366); (detail) more robust transaction_lock: avoid overlapping data spaces; clarified modules; (detail) merged (detail) The sym_diff operator (symmetric difference) (detail) disable lxbroy10 for now: technical problems with cooling; (detail) A couple of new lemmas involving cardinality (detail) merged (detail) tuned; (detail) more robust; (detail) proper build_progress for local messages; (detail) proper SQL query; (detail) Another tranche of HOL Light material on metric and topological spaces (detail) merged (detail) EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis (detail) merged (detail) more robust "stop": further "stamp" ticks may happen afterwards; (detail) removed junk; (detail) tuned signature; (detail) tuned: prefer Scala over Java; (detail) clarified signature; (detail) tuned; (detail) more SQL data; (detail) add proof method "order" to command "try0" (detail) tuned signature; (detail) clarified static Build_Process.Context vs. dynamic Build_Process.State; more dynamic Build_Process.Sessions, to accomodate multiple workers (and multiple builds); (detail) tuned signature: more operations; (detail) clarified signature: proper equals/hashCode; (detail) more robust database setup; (detail) clarified signature; (detail) clarified signature; (detail) New theory Leftist_Heap_List (detail) added [simp] (detail) merged (detail) proper build_master.build_uuid; (detail) proper session_init after deleting db files (amending af6c493b0441); (detail) clarified signature: more concise data; (detail) tuned output; (detail) more robust; (detail) clarified signature: better default; (detail) show only active builds; (detail) clarified output; (detail) tuned; (detail) support for identified builds; more complete implementation of "isabelle build_worker"; (detail) clarified signature: more operations and options; (detail) tuned; (detail) clarified signature; (detail) clarified signature; (detail) more robust close() after failed initialization; (detail) avoid repeated open_database_server: synchronized transaction_lock; (detail) tuned signature; (detail) more robust: proper transaction_lock; (detail) tuned signature; (detail) tuned signature; (detail) tuned signature; (detail) clarified signature: more options; (detail) tuned; (detail) clarified database for heaps: do not depend on build_database_test; (detail) clarified signature; (detail) tuned signature; (detail) More metric space material (detail) merged (detail) New and generalised analysis lemmas (detail) tuned names (detail) clarified signature: prefer explicit combinator; (detail) unused; (detail) restore heaps from database, which takes precedence over file-system; (detail) tuned; (detail) more operations; (detail) tuned; (detail) more robust try-finally; (detail) tuned signature; (detail) proper clean_entry; (detail) afford larger build_database_slice for better compression (HOL: 1 slice, HOL-Proofs: multiple slices for testing); (detail) prefer system option; (detail) clarified signature: more explicit class SQL.Data; (detail) proper ML_Heap.clean_entry; (detail) tuned signature; (detail) tuned; (detail) store heaps within database server; (detail) tuned signature; (detail) clarified modules; (detail) tuned signature; (detail) clarified modules; (detail) clarified modules; (detail) early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals; (detail) merged (detail) proper close; (detail) separate host.db for independent db.transaction_lock; (detail) tuned comments; (detail) omit redundant data: already stored in progress database; (detail) tuned signature: more operations; (detail) proper support for SQLite: avoid conflicts on transaction_lock; (detail) minor performance tuning: avoid external process; (detail) clarified signature; (detail) obsolete; (detail) tuned; (detail) tuned signature; (detail) tuned signature; (detail) clarified signature; (detail) tuned; (detail) clarified signature; (detail) tuned; (detail) proper pattern (amending da5cc332ded3); (detail) tuned signature; (detail) proper hostname from build_context; (detail) prefer Database_Progress, which is more robust (amending afb1a19307c4); (detail) support for Database_Progress; (detail) tuned signature: more operations; (detail) tuned signature: more operations; (detail) tuned signature: more operations; (detail) clarified signature; (detail) optional description in Eisbach "method" command; (detail) disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice (detail) Added tag Isabelle2023-RC0 for changeset f4221ae7544c (detail) updated to zstd-jni-1.5.5-4; (detail) updated to postgresql-42.6.0; (detail) back to more concise build_release, thanks to build_host_macos = "mini3"; (detail) more PLATFORMS; (detail) updated for release; (detail) tuned NEWS; (detail) more realistic factor; (detail) proper trim_context; (detail) proper exception positions; (detail) proper trim_context / transfer, e.g. for Specification.definition; (detail) tuned; (detail) tuned; (detail) tuned signature: more operations; (detail) minor performance tuning: avoid append to end-of-list; (detail) TN has enough examples of the bug. (detail) added lemma ffUnion_fsubset_iff (detail) Even more material from the HOL Light metric space library (detail) NEWS: Announcing the metric space material (detail) merged (detail) Hiding the constructor names, particularly to avoid conflicts involving "ext" (detail) New HOL Light material on metric spaces and topological spaces (detail) enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML; (detail) provide scala-3.3.0; (detail) more NEWS; (detail) tuned NEWS; (detail) NEWS; (detail) removed intro, desc, elim, and simp annotations from FSet lemmas that are instances of lemmas in Set (detail) merged (detail) NEWS (detail) set up code generation for fset (detail) redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex (detail) merged (detail) tuned signature; (detail) clarified treatment of context; (detail) clarified treatment of context; (detail) more operations; (detail) NEWS (detail) renamed notin_fset to not_fmember (detail) added author (detail) merged (detail) adapted Transfer_Debug from fmember to fempty (detail) renamed variables (detail) merged (detail) fixed lemma name (detail) redefined FSet.fmember as an abbreviation based on Set.member (detail) replaced some lemmas' implicit formulas by explicit ones to avoid silent changes (detail) merged (detail) proper setup for rule attribute; (detail) more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure; (detail) clarified output of embedded values, e.g. for 'print_locale'; (detail) tuned: more antiquotations; (detail) tuned; (detail) tuned signature: more position information; (detail) tuned; (detail) Finally, the abstract metric space development (detail) merged (detail) misc tuning and clarification; (detail) tuned signature; (detail) tuned; (detail) tuned --- Token.make_string / Token.assign are value-oriented; (detail) more documentation; (detail) tuned signature; (detail) tuned signature; (detail) more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm); (detail) prefer static simpset; (detail) omit pointless morphism in global theory; (detail) more operations; (detail) more careful treatment of context for method source; (detail) clarified context; (detail) clarified signature; (detail) remove pointless context setup (see also b2e449c155a4); (detail) more careful reset_context for stored entity; (detail) more careful reset/set_context for stored declarations; (detail) tuned; (detail) tuned; (detail) clarified signature: more explicit types; (detail) clarified data: avoid pointless Morphism.transform; (detail) proper Token.Declaration for internal_declaration; (detail) more standard treatment of morphism context; (detail) tuned: avoid duplication; (detail) more standard treatment of morphism context, but hardly relevant here; (detail) tuned; (detail) more careful treatment of set_context / reset_context for persistent morphisms; avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition; (detail) clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context; clarified signature; (detail) tuned signature; (detail) support for context within morphism (for background theory); (detail) proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs"; (detail) clarified signature; (detail) tuned; (detail) tuned; (detail) tuned signature; (detail) more accurate Thm.trim_context / Thm.transfer; (detail) clarified stored thm: result from notes; tuned; (detail) tuned whitespace; (detail) clarified signature: avoid convoluted operations; (detail) tuned signature; (detail) update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof; (detail) avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c); (detail) proper transfer / trim_context; (detail) more operations "without_context", assuming that the thm has been properly transferred already; (detail) proper trim_context / transfer; (detail) tuned: more accurate check (is_norm_hhf protect); (detail) clarified build options: reduce heap size by approx. 3%; (detail) more standard merge order, following logical structure of imports rather than physical serials; (detail) tuned; (detail) tuned; (detail) proper Thm.trim_context / Thm.transfer; (detail) proper Thm.trim_context / Thm.transfer; (detail) tuned: avoid pointless Proof_Context.init_global of Context.proof_of; (detail) New material from the HOL Light metric space library, mostly about quasi components (detail) More material from the HOL Light metric space library (detail) proper Thm.trim_context / Thm.transfer; (detail) proper position for ML-like commands; (detail) Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default) merge with default (detail) Relational_Disjoint_Set_Forests: extended theory, refactored related entries (detail) Refactored and updated entry. Synchronize with companion paper. (detail) simplified proof without auxiliary function (detail) provide more unification algorithms, e.g., to compute mgu's modulo variable renamings (detail) Adapted to devel (detail) Relational_Disjoint_Set_Forests: simplified invariant (detail) Bell_Numbers_Spivey: Add code equations for the computation of Bell numbers. (detail) Distributed_Distinct_Elements: Swap epsilon/delta for the spec of the algorithm. The reason is to preserve consistency with the upcoming publication to appear at RANDOM 2023. (detail) proved a few properties of WPO with less assumption, so that Co-WPO properties can be derived (detail) Fixed LaTeX. (detail) Merge. (detail) Fixed missing entries in ROOTS file (previous erronous commit). (detail) Normalised email. (detail) Improved setup of the symbolic evaluator. (detail) Fix proofs broken by previous commit. (detail) Universal_Hash_Families: Avoid using non-descriptive theory names. Note: The namespace for theory names is global, i.e., a name like "Definitions" is likely to cause collisions. (detail) merged (detail) Adjustments for recent cosmetic changes to the Distribution (detail) Proper epsilon-syntax (detail) Merge. (detail) Minor improvement of handling of string literals in symbolic evaluator. (detail) Removing redundant definitions: - External - Fallback (detail) tuned (detail) Merge (detail) Updating history for Isabelle/Solidity (detail) Updating Isabelle/Solidity: - Changing expressions do not have side effects anymore. - Adding support for instantiation of contracts. - Adding weakest precondition calculus for the verification of statements. (detail) Relational_Disjoint_Set_Forests: added a new theory, refactored related entries (detail) remove some redundant constraint-types in simplex algorithm (detail) relation between has-maximum and bdd_above (detail) tuned names (detail) merged (detail) more comments (detail) merged (detail) back out Paraconsistency (detail) merged (detail) tuned and simplified proofs (detail) Some additions to IICF by Valentin Springsklee (detail) merge (detail) small changes in FOL_Seq_Calc1 metadata (detail) More Paraconsistency (detail) merged (detail) prefer existing Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); (detail) proper .ML file names; (detail) proper .ML file name; (detail) eliminated suspicious Unicode character, which often produce unexpected document output; (detail) eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); (detail) tuned whitespace; (detail) avoid hardwired document output; (detail) eliminate clone of Proof_Display.print_theorem (see Isabelle/4dffc47b7e91); (detail) tuned signature; (detail) tuned (detail) tuned (detail) fixed build following a13761ef6796 (detail) merged (detail) removed unnecessary theory with potential for name conflict (detail) provided var2-versions of all doubly-nested loops (detail) Added version of algorithm 4 with precise variant var2 and tuned (detail) Floyd Warshall: improve code refinements (detail) IMP2: fix typos (detail) New check 'coverage_rcv' added. (detail) Fixing typos. (detail) Updated formalization to include improvements described in the following publication: Andreas V. Hess, Sebastian A. Mödersheim, and Achim D. Brucker. 2023. Stateful Protocol Composition in Isabelle/HOL. ACM Trans. Priv. Secur. 26, 3, Article 25 (August 2023), 36 pages. https://doi.org/10.1145/3577020 (detail) typos (detail) remove AFP group already defined by chapter; (detail) Sync with my development repo. (detail) fix merge problems; (detail) merge from afp-2022 (detail) re-generate site; (detail) tuned for smaller diffs; (detail) New topic for Gray_Codes (detail) More Gray_Codes (detail) More Gray_Codes (detail) New entry Gray_Codes (detail) metadata and sitegen for Executable_Randomized_Algorithms (detail) New entry Executable_Randomized_Algorithms (detail) new entry DCR-ExecutionEquivalence (detail) Zeckendorf: metadata and sitegen (detail) new entry Zeckendorf (detail) Crypto_Standards: Fixed a spelling error (detail) Crypto_Standards metadata & website (detail) New entry Crypto_Standards (detail) move TOML module to Isabelle (see Isabelle/be8aaaa4ac25); (detail) added missing timeout; (detail) reformat; (detail) remove duplicate fields; (detail) check TOML parse structure properly; (detail) proper typed TOML layer; (detail) tuned imports; (detail) Updated links (detail) Added citations (detail) Added citations (detail) Added citations (detail) Added refs (detail) Added DOIs (detail) Added DOIs (detail) Added DOIs (detail) Added DOI (detail) Added DOI (detail) added DOI (detail) Median_Method: Add a tight version of the median bound, suggested by Yong Kiam Tan. (detail) parse proper toml syntax; (detail) Syntax for symmetric set difference, plus tidying (detail) Update (detail) Update (detail) Add (detail) Update (detail) Update (detail) merged (detail) Three_Squares: time limit increase; and now sym_diff is declared in main HOL (detail) moved Subterm_and_Context into First_Order_Terms, merged context of Term_Aux into Term (detail) replace scala.sys.process with proper Bash.Process; (detail) renamed "flatten" to "unindex" (detail) Resolved some operator clashes (detail) merged (detail) simplified some proofs (detail) Modifications for moving from f ` S <= T to f:S->T (detail) Updated for new HOL-CSP (detail) merge (detail) updated ROOT. (detail) Registers: Fixed nonterminating subproof (detail) Collected changes to Complex_Bounded_Operators AFP entry: Complex_Vector_Spaces.thy ========================= New lemmas: clinear_scaleR[simp], abs_summable_on_scaleC_left[intro], abs_summable_on_scaleC_right[intro], ccspan_superset', ccspan_closure[simp], ccspan_finite, ccspan_UNIV[simp], infsum_in_closed_csubspaceI, closed_csubspace_space_as_set[simp], SUP_ccspan Renamed lemma: bounded_clinear_eq_on -> bounded_clinear_eq_on_closure Changed typeclass: basis_enum (has additional constant "canonical_basis_length") Renamed definition: Abs_clinear_space -> Abs_ccsubspace Complex_Inner_Product.thy ========================= New lemmas: mem_ortho_ccspanI, basis_projections_reconstruct_has_sum, basis_projections_reconstruct, basis_projections_reconstruct_summable, parseval_identity_has_sum, parseval_identity_summable, parseval_identity, canonical_basis_is_onb[simp] Complex_Bounded_Linear_Functions.thy ==================================== New definition: invertible_cblinfun (operator has with left inverse) New lemmas: not_not_singleton_cblinfun_zero, cblinfun_norm_approx_witness', summable_on_cblinfun_apply, summable_on_cblinfun_apply_left, abs_summable_on_cblinfun_apply_left, infsum_cblinfun_apply_left, has_sum_cblinfun_apply_left, bounded_clinear_cblinfun_compose_left, bounded_clinear_cblinfun_compose_right, clinear_cblinfun_compose_left, clinear_cblinfun_compose_right, additive_cblinfun_compose_left[simp], additive_cblinfun_compose_right[simp], isCont_cblinfun_compose_left, isCont_cblinfun_compose_right, cspan_compose_closed, cspan_adj_closed, unitaryI, norm_isometry_compose', unitary_nonzero[simp], isometry_inj, unitary_adj_inv, isometry_cinner_both_sides, isometry_image_is_ortho_set, cblinfun_apply_in_image', cblinfun_image_ccspan_leqI, cblinfun_same_on_image, lift_cblinfun_comp, cblinfun_image_def2, unitary_image_onb, sandwich_arg_compose, sandwich_compose, inj_sandwich_isometry, sandwich_isometry_id, is_Proj_id[simp], norm_is_Proj_nonzero, Proj_compose_cancelI, space_as_setI_via_Proj, unitary_image_ortho_compl, Proj_on_image[simp], kernel_apply_self, leq_kernel_iff, cblinfun_image_kernel, cblinfun_image_kernel_unitary, kernel_cblinfun_compose, eigenspace_0[simp], kernel_isometry, cblinfun_image_eigenspace_isometry, cblinfun_image_eigenspace_unitary, kernel_member_iff, kernel_square[simp], cblinfun_inv_left, inv_cblinfun_invertible, cblinfun_inv_right, iso_cblinfun_unitary, invertible_cblinfun_isometry, summable_cblinfun_apply_invertible, infsum_cblinfun_apply_invertible, less_eq_scaled_id_norm, butterflies_sum_id_finite, butterfly_sum_left, butterfly_sum_right, cblinfun_extension_exists_restrict Changed lemmas: cblinfun_image_INF_eq_general, cblinfun_image_INF_eq (more general), positive_hermitianI (flipped sides of equality), rank1_compose_right, rank1_uminus, rank1_uminus_iff (more general type class) Removed lemma: dense_span_separating (use bounded_clinear_eq_on_closure instead) Removed bundles: blinfun_notation, no_blinfun_notation Complex_L2.thy ============== New lemmas: clinear_Rep_ell2[simp], Abs_ell2_inverse_finite[simp], norm_ell2_bound_trunc, bounded_clinear_Rep_ell2, trunc_ell2_singleton, trunc_ell2_insert, trunc_ell2_finite_sum, is_orthogonal_trunc_ell2, ell2_decompose_has_sum, ell2_decompose_infsum, ell2_decompose_summable, Rep_ell2_cblinfun_apply_sum, explicit_cblinfun_exists, explicit_cblinfun_exists_bounded, explicit_cblinfun_exists_finite_dim[simp], explicit_cblinfun_ket, Rep_ell2_explicit_cblinfun_ket[simp] Changed lemmas: cinner_ket (uses "of_bool" instead of "if") Changed definition: ket (uses "of_bool" instead of "if") New definition: explicit_cblinfun (define an operator by giving the entries of an infinite matrix) Cblinfun_Code: ============== New definition: butterfly_code New lemma: butterfly_code Renamed definition: cblinfun_apply_code -> cblinfun_apply_ell2 Renamed lemmas: - vec_of_ell2_timesScalarVec -> vec_of_ell2_scaleC - cinner_ell2_code' -> cinner_ell2_code - times_ell2_code' -> times_ell2_code - divide_ell2_code' -> divide_ell2_code - inverse_ell2_code' -> inverse_ell2_code - one_ell2_code' -> one_ell2_code - cblinfun_apply_code -> cblinfun_apply_ell2 - cblinfun_apply_code -> cblinfun_apply_ell2 Cblinfun_Matrix.thy =================== New lemmas: vec_of_basis_enum_carrier_vec, cblinfun_of_mat_invalid extra/Extra_General.thy ======================= New lemmas: not_not_singleton_zero, has_sumI_metric, limitin_pullback_topology, tendsto_coordinatewise, limitin_closure_of extra/Extra_Vector_Spaces.thy ============================= New lemmas: summable_on_bounded_linear, any_norm_exists, abs_summable_on_scaleR_left[intro], abs_summable_on_scaleR_right[intro], Changed lemma: enum_idx_bound (expressed using CARD, added [simp]) extra/Extra_Jordan_Normal_Form.thy ================================== New lemmas: map_map_vec_cols, map_vec_conjugate (detail) Renamings of operators, and a major theorem on distributivity of Mprefix vs Sync. Renamings of some lemmata. (detail) Updated metadata for several entries. - Updated categorization for derandomization libraries, based on the newly introduced CS/Alg./Randomized category. - Added related reference for Nils Cremer's Tree Enumeration - Removed obsolete comments in Expander Grapgs (detail) metadata and sitegen for Directed_Sets (detail) new entry: Directed_Sets (detail) merge from AFP 2022 (detail) metadata and sitegen for Multirelations_Heterogeneous (detail) new entry: Multirelations_Heterogeneous (detail) adjust Schwartz_Zippel entry - Use Pi_pmf from HOL-Probability - Generalize theorem(s) in example (detail) adjusted Simple_Clause_Learning from AFP 2022 to AFP devel (detail) adjusted Given_Clause_Loops from AFP 2022 to AFP devel (detail) adjusted CommCSL from AFP 2022 to AFP devel (detail) adjusted DigitsInBase from AFP 2022 to AFP devel (detail) adjusted Schwartz_Zippel from AFP 2022 to AFP devel (detail) adjusted TsirelsonBound from AFP 2022 to AFP devel (detail) adjusted Tree_Enumeration from AFP 2022 to AFP devel (detail) adjusted efficient WPO from AFP 2022 to afp devel (detail) merge from afp-2022 (detail) New entry Efficient_Weighted_Path_Order (detail) add edit mode to afp-submit UI; (detail) solved subtle problem with multiple entries and new authors; (detail) better error logging; (detail) added edit handler to submission app; (detail) added frontend in devel mode; (detail) tuned (mostly api path handling); (detail) A real title in place of MLSS_Decision_Proc (detail) MLSS_Decision_Proc sitegen (detail) New entry MLSS_Decision_Proc (detail) metadata and sitegen for TsirelsonBound (detail) new entry: TsirelsonBound (detail) New entry Tree_Enumeration (detail) Three_Squares citegen (detail) New entry Three_Squares (detail) fixed some ACM/AMS categories (detail) more files (detail) New entry MHComputation (detail) make index.json files line-by-line for smaller diffs; (detail) cleanup; (detail) added new entry DigitsInBase; (detail) fixed broken LaTeX quotation marks in abstracts (detail) recategorised some entries (detail) new topic: Computer science/Algorithms/Randomized (detail) sitegen for Schwartz_Zippel (detail) new entry: Schwartz_Zippel (detail) New entry: Simple_Clause_Learning (detail) New entry HyperHoareLogic (detail) New entry Distributed_Distinct_Elements (detail) metadata for CommCSL + sitegen (detail) new entry: CommCSL (detail) New entry No_FTL_observers_Gen_Rel (detail) added new files generated by sitegen (detail) sitegen (detail) metadata for Expander Graphs (detail) new entry: Expander Graphs (detail) tuned; (detail) fix of toml-entries and rerun of sitegen: problem: links where in these quotes: ”...” and not in the standard ones "..." (detail) sitegen (for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection) (detail) metadata for Binary_Code_Imprimitive and Two_Generated_Word_Monoids_Intersection (detail) new entry: Two_Generated_Word_Monoids_Intersection (detail) new entry: Binary_Code_Imprimitive (detail) running sort on ROOTS (detail) New entry Probability_Inequality_Completeness (detail) Rensets metadata (detail) New entry Rensets (detail) more Edwards (detail) New entry Edwards_Elliptic_Curves_Group (detail) metadata and sitegen for CVP_Hardness (detail) new entry: CVP_Hardness (detail) rerun sitegen (detail) revert proof compression experiment (detail) metadata for ABY3_Protocols (detail) new entry ABY3_Protocols (detail) sitegen for Given_Clause_Loops (detail) New entry Given_Clause_Loops (detail) Adjustments for the simplified version of real_le_lsqrt (detail) adapted to Isabelle/84a7a0029c82 (detail) merged (detail) adapted to Isabelle/0252d635bfb2 (detail) merge (detail) merge (detail) Merge with developper version on LISN gut (detail) merged (detail) prefer @{attributes} antiquotation over Attrib.internal; adapted to Isabelle/bc42c074e58f; (detail) tuned proofs; (detail) Deleted a superfluous assumption. This proof is a horror (detail) merged (detail) fixed some bibliographic entries (detail) merged (detail) tuned (detail) merged (detail) merged (detail) adapted to current Isabelle/ec1c0daa3fbd; (detail) adapted to current Isabelle/ec1c0daa3fbd; (detail) adapted to Isabelle/5edd5b12017d; (detail) proper morphism context; (detail) backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531; (detail) proper morphism context; (detail) adapted to Isabelle/5ab5add88922; (detail) SMT-LIB interpretation of floating-point arithmetic (detail) merged (detail) SMT-LIB interpretation of floating-point arithmetic (detail) IEEE model with a single NaN value (detail) Minor (detail) merging (detail) updates for future formalizations (detail) adapted to Isabelle/f78cdc6fe971; (detail) adapted to Isabelle/f78cdc6fe971; (detail)
	Started by user Administrative User
	This run spent: 1 min 3 sec waiting; 8.8 sec build duration; 1 min 12 sec total from scheduled to completion.
	Revision: f467ff4aa8f98c0b29004c8fa2f7d180ceff0c89
	Revision: 4605c928f00e9e8ce8060baf1bc20aa97f2f4626