feat(route): Isabelle dev blog #15495
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Successfully generated as following: http://localhost:1200/isabelle-dev/blog/1 - Success ✔️<?xml version="1.0" encoding="UTF-8"?>
<rss xmlns:atom="http://www.w3.org/2005/Atom" version="2.0">
<channel>
<title>Isabelle News</title>
<link>https://isabelle-dev.sketis.net/phame/blog/view/1/</link>
<atom:link href="http://localhost:1200/isabelle-dev/blog/1" rel="self" type="application/rss+xml"></atom:link>
<description>Isabelle News - Made with love by RSSHub(https://github.com/DIYgod/RSSHub)</description>
<generator>RSSHub</generator>
<webMaster>i@diygod.me (DIYgod)</webMaster>
<language>en</language>
<lastBuildDate>Tue, 07 May 2024 04:46:32 GMT</lastBuildDate>
<ttl>5</ttl>
<item>
<title>Update to OpenJDK 21</title>
<description>Update to OpenJDK 21: the current long-term support version of Java.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/75/update_to_openjdk_21/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/75/update_to_openjdk_21/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotation for simproc_setup</title>
<description>ML antiquotation simproc_setup inlines an invocation of Simplifier.simproc_setup, using the same concrete syntax as the corresponding Isar command. This allows to introduce a new simproc conveniently within an ML module, and refer directly to its ML value. For example, the simproc Record.eq is defined in ~~/src/HOL/Tools/record.ML as follows:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/74/ml_antiquotation_for_simproc_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/74/ml_antiquotation_for_simproc_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of GHC stack with full support for ARM64 platforms</title>
<description>Update to GHC stack 2.13.1 with support for all platforms, including Apple Silicon.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/73/update_of_ghc_stack_with_full_support_for_arm64_platforms/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/73/update_of_ghc_stack_with_full_support_for_arm64_platforms/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Discontinuation of very old Linux and macOS versions</title>
<description>No longer support for very old versions of macOS and Linux: base-line is Ubuntu Linux 18.04 LTS and macOS 11 Big Sur.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/72/discontinuation_of_very_old_linux_and_macos_versions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/72/discontinuation_of_very_old_linux_and_macos_versions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML: distinguish proper interrupts from Poly/ML RTS breakdown</title>
<description>Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error. Exn.is_interrupt covers all kinds of interrupts as before, but Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/71/ml_distinguish_proper_interrupts_from_poly_ml_rts_breakdown/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/71/ml_distinguish_proper_interrupts_from_poly_ml_rts_breakdown/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Robust handling of program exceptions in Isabelle/ML</title>
<description>ML antiquotation try provides variants of exception handling that avoids accidental capture of physical interrupts (which could affect ML semantics in unpredictable ways):
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/70/robust_handling_of_program_exceptions_in_isabelle_ml/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/70/robust_handling_of_program_exceptions_in_isabelle_ml/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Significantly reduced ML heap usage</title>
<description>ML heap usage and stored heap size has been significantly reduced, especially for applications with a lot of definitions in a locale or class context. The shrink factor is usually in the range 1.1 .. 2.0, but a factor 3 .. 10 has been seen in unusual situations. This often allows big applications to return to the "small" 64_32 memory model with its hard limit of 16 GiB, and thus reduce the heap size by another factor 1.8.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/67/significantly_reduced_ml_heap_usage/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/67/significantly_reduced_ml_heap_usage/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Support for interactive document preparation in PIDE</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/66/support_for_interactive_document_preparation_in_pide/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/66/support_for_interactive_document_preparation_in_pide/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Demo documents for well-known LaTeX styles</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/65/demo_documents_for_well-known_latex_styles/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/65/demo_documents_for_well-known_latex_styles/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Zstd compression for Isabelle/Scala and Isabelle/ML</title>
<description>Operations for Zstd compression (via Isabelle/Scala):
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/64/zstd_compression_for_isabelle_scala_and_isabelle_ml/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/64/zstd_compression_for_isabelle_scala_and_isabelle_ml/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>MLton compiler for x86_64-linux</title>
<description>The MLton compiler for x86_64-linux has been bundled as Isabelle component, since Ubuntu 22.04 no longer provides a suitable package. Note that on macOS, MLton is readily available via Homebrew: https://formulae.brew.sh/formula/mlton
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/63/mlton_compiler_for_x86_64-linux/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/63/mlton_compiler_for_x86_64-linux/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Scala SSH connections use OpenSSH executables</title>
<description>Isabelle/Scala SSH connections now use regular OpenSSH executables from the local system: ssh, scp, sftp; the old ssh-java component has been discontinued. This has various practical consequences:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/62/isabelle_scala_ssh_connections_use_openssh_executables/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/62/isabelle_scala_ssh_connections_use_openssh_executables/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle log" and option "show_states"</title>
<description>Command-line tool isabelle log has been refined to support multiple sessions, and to match messages against regular expressions (using Java Pattern syntax).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/61/command-line_tool_isabelle_log_and_option_show_states/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/61/command-line_tool_isabelle_log_and_option_show_states/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Display of schematic goal instance</title>
<description>The instantiation of schematic goals is now displayed explicitly as a list of variable assignments. This works for proof state output, and at the end of a toplevel proof. In rare situations, a proof command or proof method may violate the intended goal discipline, by not producing an instance of the original goal, but there is only a warning, no hard error.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/60/display_of_schematic_goal_instance/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/60/display_of_schematic_goal_instance/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Session ROOT files support 'chapter_definition' entries</title>
<description>Old-style {* verbatim *} tokens have been discontinued (legacy feature since Isabelle2019). INCOMPATIBILITY, use ‹cartouche› syntax instead.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/59/session_root_files_support_chapter_definition_entries/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/59/session_root_files_support_chapter_definition_entries/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System: Isabelle/Scala is now based on Scala 3</title>
<description>Isabelle/Scala is now based on Scala 3. This is a completely different compiler ("dotty") and a quite different source language (we are using the classic Java-style syntax, not the new Python-style syntax). Occasional INCOMPATIBILITY, see also the official Scala documentation https://docs.scala-lang.org/scala3/guides/migration/compatibility-intro.html
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/57/system_isabelle_scala_is_now_based_on_scala_3/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/57/system_isabelle_scala_is_now_based_on_scala_3/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/ML type Bytes.T and XZ compression</title>
<description>Type Bytes.T supports scalable byte strings, beyond the limit of String.maxSize (approx. 64 MB on 64_32 architecture).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/56/isabelle_ml_type_bytes.t_and_xz_compression/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/56/isabelle_ml_type_bytes.t_and_xz_compression/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tools "isabelle hg_sync" and "isabelle sync"</title>
<description>Command-line tool isabelle hg_sync synchronizes the working directory of a local Mercurial repository with a target directory, using rsync notation for destinations.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/55/command-line_tools_isabelle_hg_sync_and_isabelle_sync/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/55/command-line_tools_isabelle_hg_sync_and_isabelle_sync/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/VSCode as bundled application</title>
<description>Isabelle/VSCode Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/54/isabelle_vscode_as_bundled_application/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/54/isabelle_vscode_as_bundled_application/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotation "instantiate"</title>
<description>ML antiquotation "instantiate" allows to instantiate formal entities (types, terms, theorems) with values given ML. This works uniformly for "typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a keyword after the instantiation. A mode "(schematic)" behind the keyword means that some variables may remain uninstantiated (fixed in the specification and schematic in the result); by default, all variables need to be instantiated.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/52/ml_antiquotation_instantiate/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/52/ml_antiquotation_instantiate/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More robust (and more strict) treatment of abstractions within the context</title>
<description>Term operations under abstractions are now more robust (and more strict) by using the formal proof context in subsequent operations:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/51/more_robust_and_more_strict_treatment_of_abstractions_within_the_context/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/51/more_robust_and_more_strict_treatment_of_abstractions_within_the_context/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Nitpick with external/portable MiniSat</title>
<description>Nitpick: External solver "MiniSat" is available for all supported Isabelle platforms (including Windows and ARM); while "MiniSat_JNI" only works for Intel Linux and macOS.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/50/nitpick_with_external_portable_minisat/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/50/nitpick_with_external_portable_minisat/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improper proof command 'guess' provided by separate theory "Pure-ex.Guess"</title>
<description>The improper proof command guess is no longer part of by Pure, but provided by the separate theory Pure-ex.Guess. INCOMPATIBILITY, existing applications need to import session Pure-ex and theory Pure-ex.Guess. Afterwards it is usually better eliminate the guess command, using explicit obtain instead.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/48/improper_proof_command_guess_provided_by_separate_theory_pure-ex.guess/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/48/improper_proof_command_guess_provided_by_separate_theory_pure-ex.guess/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotations for object-logic judgement</title>
<description>ML antiquotations make_judgment and dest_judgment refer to corresponding functions for the object-logic of the ML compilation context. This supersedes older mk_Trueprop / dest_Trueprop operations.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/47/ml_antiquotations_for_object-logic_judgement/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/47/ml_antiquotations_for_object-logic_judgement/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotations for type constructors and term constants</title>
<description>ML antiquotations for type constructors and term constants:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/46/ml_antiquotations_for_type_constructors_and_term_constants/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/46/ml_antiquotations_for_type_constructors_and_term_constants/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/ML "build" combinators</title>
<description>The build combinators of various data structures help to build content from bottom-up, by applying an add function the empty value. For example:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/45/isabelle_ml_build_combinators/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/45/isabelle_ml_build_combinators/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Scalable operations for Thm.instantiate and Thm.generalize</title>
<description>ML structures TFrees, TVars, Frees, Vars, Names provide scalable operations to accumulate items from types and terms, using a fast syntactic order. The original order of occurrences may be recovered as well, e.g. via TFrees.list_set.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/44/scalable_operations_for_thm.instantiate_and_thm.generalize/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/44/scalable_operations_for_thm.instantiate_and_thm.generalize/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Configuration option "show_results"</title>
<description>Configuration option "show_results" controls output of final results in commands like 'definition' or 'theorem'. Output is normally enabled in interactive mode, but it could occasionally cause unnecessary slowdown. It can be disabled like this:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/43/configuration_option_show_results/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/43/configuration_option_show_results/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Bundles for lattice syntax</title>
<description>Theory HOL-Library.Lattice_Syntax has been superseded by bundle lattice_syntax: it can be used in a local context via include or in a global theory via unbundle. The opposite declarations are bundled as no_lattice_syntax. Minor INCOMPATIBILITY.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/42/bundles_for_lattice_syntax/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/42/bundles_for_lattice_syntax/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Localized commands 'syntax' and 'no_syntax'</title>
<description>Commands syntax and no_syntax now work in a local theory context, but there is no proper way to refer to local entities --- in contrast to notation and no_notation. Local syntax works well with bundle, e.g. see lattice_syntax vs. no_lattice_syntax in theory Main of Isabelle/HOL.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/41/localized_commands_syntax_and_no_syntax/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/41/localized_commands_syntax_and_no_syntax/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Scala improvements</title>
<description>Each Isabelle component may specify a Scala/Java jar module declaratively via etc/build.props (file names are relative to the component directory). E.g. see $ISABELLE_HOME/etc/build.props with further explanations in the system manual.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/40/isabelle_scala_improvements/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/40/isabelle_scala_improvements/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Reactivated ML profiling</title>
<description>ML profiling has been updated and reactivated, after some degration in
Isabelle2021:</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More predefined Isabelle symbols</title>
<description>More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). See also the group "Z Notation" in the Symbols dockable of Isabelle/jEdit.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/38/more_predefined_isabelle_symbols/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/38/more_predefined_isabelle_symbols/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System options short form (e.g. "-o document")</title>
<description>System option system_log specifies an optional log file for internal messages produced by Output.system_message in Isabelle/ML; the value true refers to console progress of the build job. This works for isabelle build or any derivative of it.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/37/system_options_short_form_e.g._-o_document/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/37/system_options_short_form_e.g._-o_document/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>High-quality blackboard-bold symbols</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/36/high-quality_blackboard-bold_symbols/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/36/high-quality_blackboard-bold_symbols/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Remote provers from SystemOnTPTP via Isabelle/Scala</title>
<description>Remote provers from SystemOnTPTP (notably for Sledgehammer) are now managed via Isabelle/Scala instead of perl; the dependency on libwww-perl has been eliminated (notably on Linux). Rare INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/35/remote_provers_from_systemontptp_via_isabelle_scala/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/35/remote_provers_from_systemontptp_via_isabelle_scala/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved LaTeX typesetting of ‹...›</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/34/improved_latex_typesetting_of_%E2%80%B9...%E2%80%BA/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/34/improved_latex_typesetting_of_%E2%80%B9...%E2%80%BA/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Clarified timeouts for Isabelle/ML tools</title>
<description>Timeouts for Isabelle/ML tools are subject to system option timeout_scale --- this already used for the overall session build process before, and allows to adapt to slow machines. The underlying Timeout.apply in Isabelle/ML treats an original timeout specification 0 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY in boundary cases.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/33/clarified_timeouts_for_isabelle_ml_tools/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/33/clarified_timeouts_for_isabelle_ml_tools/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>External bash processes are always managed by Isabelle/Scala</title>
<description>External bash processes are always managed by Isabelle/Scala, in contrast to Isabelle2021 where this was only done for macOS on Apple Silicon.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/32/external_bash_processes_are_always_managed_by_isabelle_scala/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/32/external_bash_processes_are_always_managed_by_isabelle_scala/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved GUI look-and-feel</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/31/improved_gui_look-and-feel/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/31/improved_gui_look-and-feel/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/jEdit action "isabelle.goto-entity"</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/30/isabelle_jedit_action_isabelle.goto-entity/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/30/isabelle_jedit_action_isabelle.goto-entity/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Message logs from session build database</title>
<description>The command-line tool isabelle log prints prover messages from the build database of the given session, following the the order of theory sources, instead of erratic parallel evaluation. Consequently, the session log file is restricted to system messages of the overall build process, and thus becomes more informative.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/29/message_logs_from_session_build_database/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/29/message_logs_from_session_build_database/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Document antiquotation for Isabelle tools</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/27/document_antiquotation_for_isabelle_tools/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/27/document_antiquotation_for_isabelle_tools/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>PDF/HTML presentation in Isabelle/Scala, based on session build database</title>
<description>The command-line tool isabelle build provides option -P DIR to produce PDF/HTML presentation in the specified directory; -P: refers to the standard directory according to ISABELLE_BROWSER_INFO / ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken from the build database -- from this or earlier builds with option document=pdf.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/26/pdf_html_presentation_in_isabelle_scala_based_on_session_build_database/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/26/pdf_html_presentation_in_isabelle_scala_based_on_session_build_database/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Experimental support for arm64-linux platform</title>
<description>Experimental support for arm64-linux platform. The reference platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/25/experimental_support_for_arm64-linux_platform/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/25/experimental_support_for_arm64-linux_platform/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update external prover components for Sledgehammer etc.</title>
<description>Update/rebuild external provers on currently supported OS platforms, notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/24/update_external_prover_components_for_sledgehammer_etc./</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/24/update_external_prover_components_for_sledgehammer_etc./</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Include veriT component for "smt" method</title>
<description>An updated version of the veriT solver is now included as Isabelle component. It can be used in the smt proof method via smt (verit) or via declare [[smt_solver = verit]] in the context; see also session HOL-Word-SMT_Examples.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/23/include_verit_component_for_smt_method/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/23/include_verit_component_for_smt_method/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Document preparation engine updates</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/22/document_preparation_engine_updates/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/22/document_preparation_engine_updates/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session</title>
<description>Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session (instead of an external Java process): this improves reactivity and saves resources. This experimental feature is guarded by system option kodkod_scala (default: false).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/20/nitpick_kodkod_may_be_invoked_directly_within_the_running_isabelle_scala_session/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/20/nitpick_kodkod_may_be_invoked_directly_within_the_running_isabelle_scala_session/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>User-defined Isabelle server commands via isabelle_scala_service</title>
<description>Isabelle server allows user-defined commands via isabelle_scala_service.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/19/user-defined_isabelle_server_commands_via_isabelle_scala_service/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/19/user-defined_isabelle_server_commands_via_isabelle_scala_service/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More systematic support for special directories</title>
<description>The shell function isabelle_directory (within etc/settings of components) augments the list of special directories for persistent symbolic path names. This improves portability of heap images and session databases. It used to be hard-wired for Isabelle + AFP, but other projects may now participate on equal terms.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/18/more_systematic_support_for_special_directories/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/18/more_systematic_support_for_special_directories/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved monitoring for Isabelle/ML and Java</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/17/improved_monitoring_for_isabelle_ml_and_java/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/17/improved_monitoring_for_isabelle_ml_and_java/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML statistics via an external Poly/ML process</title>
<description>ML statistics via an external Poly/ML process: this allows monitoring the runtime system while the ML program sleeps.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/16/ml_statistics_via_an_external_poly_ml_process/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/16/ml_statistics_via_an_external_poly_ml_process/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Theory_Data extend operation is obsolete and needs to be the identity function</title>
<description>Theory_Data extend operation is obsolete and needs to be the identity function; merge should be conservative and not reset to the empty value. Subtle INCOMPATIBILITY and change of semantics (due to Theory.join_theory from Isabelle2020). Special extend/merge behaviour at the begin of a new theory can be achieved via Theory.at_begin.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/15/theory_data_extend_operation_is_obsolete_and_needs_to_be_the_identity_function/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/15/theory_data_extend_operation_is_obsolete_and_needs_to_be_the_identity_function/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System option pide_session is enabled by default</title>
<description>System option "pide_session" is enabled by default, notably for standard "isabelle build": it allows to invoke Isabelle/Scala operations from Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/14/system_option_pide_session_is_enabled_by_default/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/14/system_option_pide_session_is_enabled_by_default/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of Isabelle/jEdit to jedit-5.6pre1</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/13/update_of_isabelle_jedit_to_jedit-5.6pre1/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/13/update_of_isabelle_jedit_to_jedit-5.6pre1/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Antiquotations for Isabelle systems programming</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/12/antiquotations_for_isabelle_systems_programming/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/12/antiquotations_for_isabelle_systems_programming/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of Isabelle/Phabricator setup</title>
<description>Isabelle/Phabricator setup has been updated to follow ongoing development: libphutil has been discontinued. Minor INCOMPATIBILITY: existing server installations should remove libphutil from /usr/local/bin/isabelle-phabricator-upgrade and each installation root directory (e.g. /var/www/phabricator-vcs/libphutil).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/11/update_of_isabelle_phabricator_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/11/update_of_isabelle_phabricator_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle sessions"</title>
<description>The command-line tool "isabelle sessions" explores the structure of Isabelle sessions and prints result names in topological order (on stdout).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/10/command-line_tool_isabelle_sessions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/10/command-line_tool_isabelle_sessions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Slightly improved isabelle build_docker tool</title>
<description>The command-line tool isabelle build_docker has been slightly improved: it is now properly documented in the system manual.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/9/slightly_improved_isabelle_build_docker_tool/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/9/slightly_improved_isabelle_build_docker_tool/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Mixfix annotations may use single-quote-space as documented</title>
<description>Mixfix annotations may use "' " (single quote followed by space) to separate delimiters (as documented in the isar-ref manual), without requiring an auxiliary empty block. A literal single quote needs to be escaped properly. Minor INCOMPATIBILITY.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/8/mixfix_annotations_may_use_single-quote-space_as_documented/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/8/mixfix_annotations_may_use_single-quote-space_as_documented/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Support Java/VM monitoring via jconsole</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/7/support_java_vm_monitoring_via_jconsole/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/7/support_java_vm_monitoring_via_jconsole/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/jEdit actions and shortcuts for tooltips, messages, error positions</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/6/isabelle_jedit_actions_and_shortcuts_for_tooltips_messages_error_positions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/6/isabelle_jedit_actions_and_shortcuts_for_tooltips_messages_error_positions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle scala_project"</title>
<description>The command-line tool "isabelle scala_project" creates a Gradle project configuration for Isabelle/Scala/jEdit, to support Scala IDEs such as IntelliJ IDEA.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/4/command-line_tool_isabelle_scala_project/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/4/command-line_tool_isabelle_scala_project/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle hg_setup"</title>
<description>The command-line tool "isabelle hg_setup" simplifies the setup of Mercurial repositories, with hosting via Phabricator or SSH file server access.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/2/command-line_tool_isabelle_hg_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/2/command-line_tool_isabelle_hg_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Phabricator setup</title>
<description>The command-line tool "isabelle phabricator_setup" facilitates self-hosting of the Phabricator software-development platform, with support for Git, Mercurial, Subversion repositories. This helps to avoid monoculture and to escape the gravity of centralized version control by Github and/or Bitbucket. For further documentation, see chapter "Phabricator server administration" in the "system" manual. A notable example installation is https://isabelle-dev.sketis.net/.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/1/isabelle_phabricator_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/1/isabelle_phabricator_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
</channel>
</rss>http://localhost:1200/isabelle-dev/blog/2 - Success ✔️<?xml version="1.0" encoding="UTF-8"?>
<rss xmlns:atom="http://www.w3.org/2005/Atom" version="2.0">
<channel>
<title>Isabelle Release</title>
<link>https://isabelle-dev.sketis.net/phame/blog/view/2/</link>
<atom:link href="http://localhost:1200/isabelle-dev/blog/2" rel="self" type="application/rss+xml"></atom:link>
<description>Isabelle Release - Made with love by RSSHub(https://github.com/DIYgod/RSSHub)</description>
<generator>RSSHub</generator>
<webMaster>i@diygod.me (DIYgod)</webMaster>
<language>en</language>
<lastBuildDate>Tue, 07 May 2024 04:46:32 GMT</lastBuildDate>
<ttl>5</ttl>
<item>
<title>Release Candidates for Isabelle2024</title>
<description>The official Isabelle2024 release is scheduled for mid May 2024. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2024 release</title>
<description>The next anticipated release is after Isabelle2023 (September 2023) is Isabelle2024 (May 2024). The distance between two releases is usually 8–10 months, but recently this got closer 11 months. To return to regularity, and to accommodate other side-conditions, the hot phase of the release is presently scheduled for 03-Apr..15-May-2024. The detailed plan is as follows:</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/69/plan_for_isabelle2024_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/69/plan_for_isabelle2024_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2023</title>
<description>The official Isabelle2023 release is scheduled for early September 2023. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2022</title>
<description>The official Isabelle2022 release is scheduled for late October 2022. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2021-1</title>
<description>The official Isabelle2021-1 release is scheduled for December 2021. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2021-1 release</title>
<description>The next anticipated release is Isabelle2021-1 (December 2021): as the distance between two releases is usually 8–10 months, there are sometimes 2 releases per year. This explains the slightly odd name tag, but in all other respects, Isabelle-2021-1 should be a perfectly normal official release.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/49/plan_for_isabelle2021-1_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/49/plan_for_isabelle2021-1_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2021</title>
<description>The official Isabelle2021 release is scheduled for February 2021. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the workboard and the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2021 release</title>
<description>The next anticipated release is Isabelle2021 (February 2021). The hot phase with release candidates will presumably be 28-Dec-2020 .. 15-Feb-2020.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/21/plan_for_isabelle2021_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/21/plan_for_isabelle2021_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2020</title>
<description>The official Isabelle2020 release is scheduled for April 2020. This blog entry is dynamically updated to follow the sequence of public release candidates.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2020 release</title>
<description>The next anticipated release is Isabelle2020 (April 2020). The hot phase with release candidates will presumably be 01-Mar-2020 .. 15-Apr-2020.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/3/plan_for_isabelle2020_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/3/plan_for_isabelle2020_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
</channel>
</rss> |
github-actions
bot
added
the
Auto: Route Test Complete
TonyRL
reviewed
May 7, 2024
|
Successfully generated as following: http://localhost:1200/isabelle-dev/blog/1 - Success ✔️<?xml version="1.0" encoding="UTF-8"?>
<rss xmlns:atom="http://www.w3.org/2005/Atom" version="2.0">
<channel>
<title>Isabelle News</title>
<link>https://isabelle-dev.sketis.net/phame/blog/view/1/</link>
<atom:link href="http://localhost:1200/isabelle-dev/blog/1" rel="self" type="application/rss+xml"></atom:link>
<description>Isabelle News - Made with love by RSSHub(https://github.com/DIYgod/RSSHub)</description>
<generator>RSSHub</generator>
<webMaster>i@diygod.me (DIYgod)</webMaster>
<language>en</language>
<lastBuildDate>Tue, 07 May 2024 15:29:24 GMT</lastBuildDate>
<ttl>5</ttl>
<item>
<title>Update to OpenJDK 21</title>
<description>Update to OpenJDK 21: the current long-term support version of Java.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/75/update_to_openjdk_21/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/75/update_to_openjdk_21/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotation for simproc_setup</title>
<description>ML antiquotation simproc_setup inlines an invocation of Simplifier.simproc_setup, using the same concrete syntax as the corresponding Isar command. This allows to introduce a new simproc conveniently within an ML module, and refer directly to its ML value. For example, the simproc Record.eq is defined in ~~/src/HOL/Tools/record.ML as follows:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/74/ml_antiquotation_for_simproc_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/74/ml_antiquotation_for_simproc_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of GHC stack with full support for ARM64 platforms</title>
<description>Update to GHC stack 2.13.1 with support for all platforms, including Apple Silicon.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/73/update_of_ghc_stack_with_full_support_for_arm64_platforms/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/73/update_of_ghc_stack_with_full_support_for_arm64_platforms/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Discontinuation of very old Linux and macOS versions</title>
<description>No longer support for very old versions of macOS and Linux: base-line is Ubuntu Linux 18.04 LTS and macOS 11 Big Sur.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/72/discontinuation_of_very_old_linux_and_macos_versions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/72/discontinuation_of_very_old_linux_and_macos_versions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML: distinguish proper interrupts from Poly/ML RTS breakdown</title>
<description>Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error. Exn.is_interrupt covers all kinds of interrupts as before, but Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/71/ml_distinguish_proper_interrupts_from_poly_ml_rts_breakdown/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/71/ml_distinguish_proper_interrupts_from_poly_ml_rts_breakdown/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Robust handling of program exceptions in Isabelle/ML</title>
<description>ML antiquotation try provides variants of exception handling that avoids accidental capture of physical interrupts (which could affect ML semantics in unpredictable ways):
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/70/robust_handling_of_program_exceptions_in_isabelle_ml/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/70/robust_handling_of_program_exceptions_in_isabelle_ml/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Significantly reduced ML heap usage</title>
<description>ML heap usage and stored heap size has been significantly reduced, especially for applications with a lot of definitions in a locale or class context. The shrink factor is usually in the range 1.1 .. 2.0, but a factor 3 .. 10 has been seen in unusual situations. This often allows big applications to return to the "small" 64_32 memory model with its hard limit of 16 GiB, and thus reduce the heap size by another factor 1.8.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/67/significantly_reduced_ml_heap_usage/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/67/significantly_reduced_ml_heap_usage/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Support for interactive document preparation in PIDE</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/66/support_for_interactive_document_preparation_in_pide/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/66/support_for_interactive_document_preparation_in_pide/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Demo documents for well-known LaTeX styles</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/65/demo_documents_for_well-known_latex_styles/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/65/demo_documents_for_well-known_latex_styles/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Zstd compression for Isabelle/Scala and Isabelle/ML</title>
<description>Operations for Zstd compression (via Isabelle/Scala):
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/64/zstd_compression_for_isabelle_scala_and_isabelle_ml/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/64/zstd_compression_for_isabelle_scala_and_isabelle_ml/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>MLton compiler for x86_64-linux</title>
<description>The MLton compiler for x86_64-linux has been bundled as Isabelle component, since Ubuntu 22.04 no longer provides a suitable package. Note that on macOS, MLton is readily available via Homebrew: https://formulae.brew.sh/formula/mlton
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/63/mlton_compiler_for_x86_64-linux/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/63/mlton_compiler_for_x86_64-linux/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Scala SSH connections use OpenSSH executables</title>
<description>Isabelle/Scala SSH connections now use regular OpenSSH executables from the local system: ssh, scp, sftp; the old ssh-java component has been discontinued. This has various practical consequences:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/62/isabelle_scala_ssh_connections_use_openssh_executables/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/62/isabelle_scala_ssh_connections_use_openssh_executables/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle log" and option "show_states"</title>
<description>Command-line tool isabelle log has been refined to support multiple sessions, and to match messages against regular expressions (using Java Pattern syntax).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/61/command-line_tool_isabelle_log_and_option_show_states/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/61/command-line_tool_isabelle_log_and_option_show_states/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Display of schematic goal instance</title>
<description>The instantiation of schematic goals is now displayed explicitly as a list of variable assignments. This works for proof state output, and at the end of a toplevel proof. In rare situations, a proof command or proof method may violate the intended goal discipline, by not producing an instance of the original goal, but there is only a warning, no hard error.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/60/display_of_schematic_goal_instance/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/60/display_of_schematic_goal_instance/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Session ROOT files support 'chapter_definition' entries</title>
<description>Old-style {* verbatim *} tokens have been discontinued (legacy feature since Isabelle2019). INCOMPATIBILITY, use ‹cartouche› syntax instead.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/59/session_root_files_support_chapter_definition_entries/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/59/session_root_files_support_chapter_definition_entries/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System: Isabelle/Scala is now based on Scala 3</title>
<description>Isabelle/Scala is now based on Scala 3. This is a completely different compiler ("dotty") and a quite different source language (we are using the classic Java-style syntax, not the new Python-style syntax). Occasional INCOMPATIBILITY, see also the official Scala documentation https://docs.scala-lang.org/scala3/guides/migration/compatibility-intro.html
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/57/system_isabelle_scala_is_now_based_on_scala_3/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/57/system_isabelle_scala_is_now_based_on_scala_3/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/ML type Bytes.T and XZ compression</title>
<description>Type Bytes.T supports scalable byte strings, beyond the limit of String.maxSize (approx. 64 MB on 64_32 architecture).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/56/isabelle_ml_type_bytes.t_and_xz_compression/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/56/isabelle_ml_type_bytes.t_and_xz_compression/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tools "isabelle hg_sync" and "isabelle sync"</title>
<description>Command-line tool isabelle hg_sync synchronizes the working directory of a local Mercurial repository with a target directory, using rsync notation for destinations.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/55/command-line_tools_isabelle_hg_sync_and_isabelle_sync/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/55/command-line_tools_isabelle_hg_sync_and_isabelle_sync/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/VSCode as bundled application</title>
<description>Isabelle/VSCode Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/54/isabelle_vscode_as_bundled_application/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/54/isabelle_vscode_as_bundled_application/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotation "instantiate"</title>
<description>ML antiquotation "instantiate" allows to instantiate formal entities (types, terms, theorems) with values given ML. This works uniformly for "typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a keyword after the instantiation. A mode "(schematic)" behind the keyword means that some variables may remain uninstantiated (fixed in the specification and schematic in the result); by default, all variables need to be instantiated.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/52/ml_antiquotation_instantiate/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/52/ml_antiquotation_instantiate/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More robust (and more strict) treatment of abstractions within the context</title>
<description>Term operations under abstractions are now more robust (and more strict) by using the formal proof context in subsequent operations:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/51/more_robust_and_more_strict_treatment_of_abstractions_within_the_context/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/51/more_robust_and_more_strict_treatment_of_abstractions_within_the_context/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Nitpick with external/portable MiniSat</title>
<description>Nitpick: External solver "MiniSat" is available for all supported Isabelle platforms (including Windows and ARM); while "MiniSat_JNI" only works for Intel Linux and macOS.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/50/nitpick_with_external_portable_minisat/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/50/nitpick_with_external_portable_minisat/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improper proof command 'guess' provided by separate theory "Pure-ex.Guess"</title>
<description>The improper proof command guess is no longer part of by Pure, but provided by the separate theory Pure-ex.Guess. INCOMPATIBILITY, existing applications need to import session Pure-ex and theory Pure-ex.Guess. Afterwards it is usually better eliminate the guess command, using explicit obtain instead.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/48/improper_proof_command_guess_provided_by_separate_theory_pure-ex.guess/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/48/improper_proof_command_guess_provided_by_separate_theory_pure-ex.guess/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotations for object-logic judgement</title>
<description>ML antiquotations make_judgment and dest_judgment refer to corresponding functions for the object-logic of the ML compilation context. This supersedes older mk_Trueprop / dest_Trueprop operations.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/47/ml_antiquotations_for_object-logic_judgement/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/47/ml_antiquotations_for_object-logic_judgement/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotations for type constructors and term constants</title>
<description>ML antiquotations for type constructors and term constants:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/46/ml_antiquotations_for_type_constructors_and_term_constants/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/46/ml_antiquotations_for_type_constructors_and_term_constants/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/ML "build" combinators</title>
<description>The build combinators of various data structures help to build content from bottom-up, by applying an add function the empty value. For example:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/45/isabelle_ml_build_combinators/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/45/isabelle_ml_build_combinators/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Scalable operations for Thm.instantiate and Thm.generalize</title>
<description>ML structures TFrees, TVars, Frees, Vars, Names provide scalable operations to accumulate items from types and terms, using a fast syntactic order. The original order of occurrences may be recovered as well, e.g. via TFrees.list_set.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/44/scalable_operations_for_thm.instantiate_and_thm.generalize/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/44/scalable_operations_for_thm.instantiate_and_thm.generalize/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Configuration option "show_results"</title>
<description>Configuration option "show_results" controls output of final results in commands like 'definition' or 'theorem'. Output is normally enabled in interactive mode, but it could occasionally cause unnecessary slowdown. It can be disabled like this:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/43/configuration_option_show_results/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/43/configuration_option_show_results/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Bundles for lattice syntax</title>
<description>Theory HOL-Library.Lattice_Syntax has been superseded by bundle lattice_syntax: it can be used in a local context via include or in a global theory via unbundle. The opposite declarations are bundled as no_lattice_syntax. Minor INCOMPATIBILITY.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/42/bundles_for_lattice_syntax/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/42/bundles_for_lattice_syntax/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Localized commands 'syntax' and 'no_syntax'</title>
<description>Commands syntax and no_syntax now work in a local theory context, but there is no proper way to refer to local entities --- in contrast to notation and no_notation. Local syntax works well with bundle, e.g. see lattice_syntax vs. no_lattice_syntax in theory Main of Isabelle/HOL.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/41/localized_commands_syntax_and_no_syntax/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/41/localized_commands_syntax_and_no_syntax/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Scala improvements</title>
<description>Each Isabelle component may specify a Scala/Java jar module declaratively via etc/build.props (file names are relative to the component directory). E.g. see $ISABELLE_HOME/etc/build.props with further explanations in the system manual.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/40/isabelle_scala_improvements/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/40/isabelle_scala_improvements/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Reactivated ML profiling</title>
<description>ML profiling has been updated and reactivated, after some degration in
Isabelle2021:</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More predefined Isabelle symbols</title>
<description>More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). See also the group "Z Notation" in the Symbols dockable of Isabelle/jEdit.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/38/more_predefined_isabelle_symbols/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/38/more_predefined_isabelle_symbols/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System options short form (e.g. "-o document")</title>
<description>System option system_log specifies an optional log file for internal messages produced by Output.system_message in Isabelle/ML; the value true refers to console progress of the build job. This works for isabelle build or any derivative of it.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/37/system_options_short_form_e.g._-o_document/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/37/system_options_short_form_e.g._-o_document/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>High-quality blackboard-bold symbols</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/36/high-quality_blackboard-bold_symbols/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/36/high-quality_blackboard-bold_symbols/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Remote provers from SystemOnTPTP via Isabelle/Scala</title>
<description>Remote provers from SystemOnTPTP (notably for Sledgehammer) are now managed via Isabelle/Scala instead of perl; the dependency on libwww-perl has been eliminated (notably on Linux). Rare INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/35/remote_provers_from_systemontptp_via_isabelle_scala/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/35/remote_provers_from_systemontptp_via_isabelle_scala/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved LaTeX typesetting of ‹...›</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/34/improved_latex_typesetting_of_%E2%80%B9...%E2%80%BA/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/34/improved_latex_typesetting_of_%E2%80%B9...%E2%80%BA/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Clarified timeouts for Isabelle/ML tools</title>
<description>Timeouts for Isabelle/ML tools are subject to system option timeout_scale --- this already used for the overall session build process before, and allows to adapt to slow machines. The underlying Timeout.apply in Isabelle/ML treats an original timeout specification 0 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY in boundary cases.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/33/clarified_timeouts_for_isabelle_ml_tools/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/33/clarified_timeouts_for_isabelle_ml_tools/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>External bash processes are always managed by Isabelle/Scala</title>
<description>External bash processes are always managed by Isabelle/Scala, in contrast to Isabelle2021 where this was only done for macOS on Apple Silicon.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/32/external_bash_processes_are_always_managed_by_isabelle_scala/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/32/external_bash_processes_are_always_managed_by_isabelle_scala/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved GUI look-and-feel</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/31/improved_gui_look-and-feel/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/31/improved_gui_look-and-feel/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/jEdit action "isabelle.goto-entity"</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/30/isabelle_jedit_action_isabelle.goto-entity/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/30/isabelle_jedit_action_isabelle.goto-entity/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Message logs from session build database</title>
<description>The command-line tool isabelle log prints prover messages from the build database of the given session, following the the order of theory sources, instead of erratic parallel evaluation. Consequently, the session log file is restricted to system messages of the overall build process, and thus becomes more informative.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/29/message_logs_from_session_build_database/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/29/message_logs_from_session_build_database/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Document antiquotation for Isabelle tools</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/27/document_antiquotation_for_isabelle_tools/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/27/document_antiquotation_for_isabelle_tools/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>PDF/HTML presentation in Isabelle/Scala, based on session build database</title>
<description>The command-line tool isabelle build provides option -P DIR to produce PDF/HTML presentation in the specified directory; -P: refers to the standard directory according to ISABELLE_BROWSER_INFO / ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken from the build database -- from this or earlier builds with option document=pdf.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/26/pdf_html_presentation_in_isabelle_scala_based_on_session_build_database/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/26/pdf_html_presentation_in_isabelle_scala_based_on_session_build_database/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Experimental support for arm64-linux platform</title>
<description>Experimental support for arm64-linux platform. The reference platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/25/experimental_support_for_arm64-linux_platform/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/25/experimental_support_for_arm64-linux_platform/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update external prover components for Sledgehammer etc.</title>
<description>Update/rebuild external provers on currently supported OS platforms, notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/24/update_external_prover_components_for_sledgehammer_etc./</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/24/update_external_prover_components_for_sledgehammer_etc./</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Include veriT component for "smt" method</title>
<description>An updated version of the veriT solver is now included as Isabelle component. It can be used in the smt proof method via smt (verit) or via declare [[smt_solver = verit]] in the context; see also session HOL-Word-SMT_Examples.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/23/include_verit_component_for_smt_method/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/23/include_verit_component_for_smt_method/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Document preparation engine updates</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/22/document_preparation_engine_updates/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/22/document_preparation_engine_updates/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session</title>
<description>Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session (instead of an external Java process): this improves reactivity and saves resources. This experimental feature is guarded by system option kodkod_scala (default: false).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/20/nitpick_kodkod_may_be_invoked_directly_within_the_running_isabelle_scala_session/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/20/nitpick_kodkod_may_be_invoked_directly_within_the_running_isabelle_scala_session/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>User-defined Isabelle server commands via isabelle_scala_service</title>
<description>Isabelle server allows user-defined commands via isabelle_scala_service.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/19/user-defined_isabelle_server_commands_via_isabelle_scala_service/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/19/user-defined_isabelle_server_commands_via_isabelle_scala_service/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More systematic support for special directories</title>
<description>The shell function isabelle_directory (within etc/settings of components) augments the list of special directories for persistent symbolic path names. This improves portability of heap images and session databases. It used to be hard-wired for Isabelle + AFP, but other projects may now participate on equal terms.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/18/more_systematic_support_for_special_directories/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/18/more_systematic_support_for_special_directories/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved monitoring for Isabelle/ML and Java</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/17/improved_monitoring_for_isabelle_ml_and_java/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/17/improved_monitoring_for_isabelle_ml_and_java/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML statistics via an external Poly/ML process</title>
<description>ML statistics via an external Poly/ML process: this allows monitoring the runtime system while the ML program sleeps.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/16/ml_statistics_via_an_external_poly_ml_process/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/16/ml_statistics_via_an_external_poly_ml_process/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Theory_Data extend operation is obsolete and needs to be the identity function</title>
<description>Theory_Data extend operation is obsolete and needs to be the identity function; merge should be conservative and not reset to the empty value. Subtle INCOMPATIBILITY and change of semantics (due to Theory.join_theory from Isabelle2020). Special extend/merge behaviour at the begin of a new theory can be achieved via Theory.at_begin.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/15/theory_data_extend_operation_is_obsolete_and_needs_to_be_the_identity_function/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/15/theory_data_extend_operation_is_obsolete_and_needs_to_be_the_identity_function/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System option pide_session is enabled by default</title>
<description>System option "pide_session" is enabled by default, notably for standard "isabelle build": it allows to invoke Isabelle/Scala operations from Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/14/system_option_pide_session_is_enabled_by_default/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/14/system_option_pide_session_is_enabled_by_default/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of Isabelle/jEdit to jedit-5.6pre1</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/13/update_of_isabelle_jedit_to_jedit-5.6pre1/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/13/update_of_isabelle_jedit_to_jedit-5.6pre1/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Antiquotations for Isabelle systems programming</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/12/antiquotations_for_isabelle_systems_programming/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/12/antiquotations_for_isabelle_systems_programming/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of Isabelle/Phabricator setup</title>
<description>Isabelle/Phabricator setup has been updated to follow ongoing development: libphutil has been discontinued. Minor INCOMPATIBILITY: existing server installations should remove libphutil from /usr/local/bin/isabelle-phabricator-upgrade and each installation root directory (e.g. /var/www/phabricator-vcs/libphutil).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/11/update_of_isabelle_phabricator_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/11/update_of_isabelle_phabricator_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle sessions"</title>
<description>The command-line tool "isabelle sessions" explores the structure of Isabelle sessions and prints result names in topological order (on stdout).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/10/command-line_tool_isabelle_sessions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/10/command-line_tool_isabelle_sessions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Slightly improved isabelle build_docker tool</title>
<description>The command-line tool isabelle build_docker has been slightly improved: it is now properly documented in the system manual.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/9/slightly_improved_isabelle_build_docker_tool/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/9/slightly_improved_isabelle_build_docker_tool/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Mixfix annotations may use single-quote-space as documented</title>
<description>Mixfix annotations may use "' " (single quote followed by space) to separate delimiters (as documented in the isar-ref manual), without requiring an auxiliary empty block. A literal single quote needs to be escaped properly. Minor INCOMPATIBILITY.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/8/mixfix_annotations_may_use_single-quote-space_as_documented/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/8/mixfix_annotations_may_use_single-quote-space_as_documented/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Support Java/VM monitoring via jconsole</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/7/support_java_vm_monitoring_via_jconsole/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/7/support_java_vm_monitoring_via_jconsole/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/jEdit actions and shortcuts for tooltips, messages, error positions</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/6/isabelle_jedit_actions_and_shortcuts_for_tooltips_messages_error_positions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/6/isabelle_jedit_actions_and_shortcuts_for_tooltips_messages_error_positions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle scala_project"</title>
<description>The command-line tool "isabelle scala_project" creates a Gradle project configuration for Isabelle/Scala/jEdit, to support Scala IDEs such as IntelliJ IDEA.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/4/command-line_tool_isabelle_scala_project/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/4/command-line_tool_isabelle_scala_project/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle hg_setup"</title>
<description>The command-line tool "isabelle hg_setup" simplifies the setup of Mercurial repositories, with hosting via Phabricator or SSH file server access.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/2/command-line_tool_isabelle_hg_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/2/command-line_tool_isabelle_hg_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Phabricator setup</title>
<description>The command-line tool "isabelle phabricator_setup" facilitates self-hosting of the Phabricator software-development platform, with support for Git, Mercurial, Subversion repositories. This helps to avoid monoculture and to escape the gravity of centralized version control by Github and/or Bitbucket. For further documentation, see chapter "Phabricator server administration" in the "system" manual. A notable example installation is https://isabelle-dev.sketis.net/.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/1/isabelle_phabricator_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/1/isabelle_phabricator_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
</channel>
</rss>http://localhost:1200/isabelle-dev/blog/2 - Success ✔️<?xml version="1.0" encoding="UTF-8"?>
<rss xmlns:atom="http://www.w3.org/2005/Atom" version="2.0">
<channel>
<title>Isabelle Release</title>
<link>https://isabelle-dev.sketis.net/phame/blog/view/2/</link>
<atom:link href="http://localhost:1200/isabelle-dev/blog/2" rel="self" type="application/rss+xml"></atom:link>
<description>Isabelle Release - Made with love by RSSHub(https://github.com/DIYgod/RSSHub)</description>
<generator>RSSHub</generator>
<webMaster>i@diygod.me (DIYgod)</webMaster>
<language>en</language>
<lastBuildDate>Tue, 07 May 2024 15:29:24 GMT</lastBuildDate>
<ttl>5</ttl>
<item>
<title>Release Candidates for Isabelle2024</title>
<description>The official Isabelle2024 release is scheduled for mid May 2024. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2024 release</title>
<description>The next anticipated release is after Isabelle2023 (September 2023) is Isabelle2024 (May 2024). The distance between two releases is usually 8–10 months, but recently this got closer 11 months. To return to regularity, and to accommodate other side-conditions, the hot phase of the release is presently scheduled for 03-Apr..15-May-2024. The detailed plan is as follows:</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/69/plan_for_isabelle2024_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/69/plan_for_isabelle2024_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2023</title>
<description>The official Isabelle2023 release is scheduled for early September 2023. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2022</title>
<description>The official Isabelle2022 release is scheduled for late October 2022. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2021-1</title>
<description>The official Isabelle2021-1 release is scheduled for December 2021. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2021-1 release</title>
<description>The next anticipated release is Isabelle2021-1 (December 2021): as the distance between two releases is usually 8–10 months, there are sometimes 2 releases per year. This explains the slightly odd name tag, but in all other respects, Isabelle-2021-1 should be a perfectly normal official release.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/49/plan_for_isabelle2021-1_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/49/plan_for_isabelle2021-1_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2021</title>
<description>The official Isabelle2021 release is scheduled for February 2021. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the workboard and the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2021 release</title>
<description>The next anticipated release is Isabelle2021 (February 2021). The hot phase with release candidates will presumably be 28-Dec-2020 .. 15-Feb-2020.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/21/plan_for_isabelle2021_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/21/plan_for_isabelle2021_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2020</title>
<description>The official Isabelle2020 release is scheduled for April 2020. This blog entry is dynamically updated to follow the sequence of public release candidates.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2020 release</title>
<description>The next anticipated release is Isabelle2020 (April 2020). The hot phase with release candidates will presumably be 01-Mar-2020 .. 15-Apr-2020.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/3/plan_for_isabelle2020_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/3/plan_for_isabelle2020_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
</channel>
</rss> |
|
Successfully generated as following: http://localhost:1200/isabelle-dev/blog/1 - Success ✔️<?xml version="1.0" encoding="UTF-8"?>
<rss xmlns:atom="http://www.w3.org/2005/Atom" version="2.0">
<channel>
<title>Isabelle News</title>
<link>https://isabelle-dev.sketis.net/phame/blog/view/1/</link>
<atom:link href="http://localhost:1200/isabelle-dev/blog/1" rel="self" type="application/rss+xml"></atom:link>
<description>Isabelle News - Made with love by RSSHub(https://github.com/DIYgod/RSSHub)</description>
<generator>RSSHub</generator>
<webMaster>i@diygod.me (DIYgod)</webMaster>
<language>en</language>
<lastBuildDate>Tue, 07 May 2024 17:53:08 GMT</lastBuildDate>
<ttl>5</ttl>
<item>
<title>Update to OpenJDK 21</title>
<description>Update to OpenJDK 21: the current long-term support version of Java.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/75/update_to_openjdk_21/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/75/update_to_openjdk_21/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotation for simproc_setup</title>
<description>ML antiquotation simproc_setup inlines an invocation of Simplifier.simproc_setup, using the same concrete syntax as the corresponding Isar command. This allows to introduce a new simproc conveniently within an ML module, and refer directly to its ML value. For example, the simproc Record.eq is defined in ~~/src/HOL/Tools/record.ML as follows:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/74/ml_antiquotation_for_simproc_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/74/ml_antiquotation_for_simproc_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of GHC stack with full support for ARM64 platforms</title>
<description>Update to GHC stack 2.13.1 with support for all platforms, including Apple Silicon.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/73/update_of_ghc_stack_with_full_support_for_arm64_platforms/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/73/update_of_ghc_stack_with_full_support_for_arm64_platforms/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Discontinuation of very old Linux and macOS versions</title>
<description>No longer support for very old versions of macOS and Linux: base-line is Ubuntu Linux 18.04 LTS and macOS 11 Big Sur.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/72/discontinuation_of_very_old_linux_and_macos_versions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/72/discontinuation_of_very_old_linux_and_macos_versions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML: distinguish proper interrupts from Poly/ML RTS breakdown</title>
<description>Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error. Exn.is_interrupt covers all kinds of interrupts as before, but Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/71/ml_distinguish_proper_interrupts_from_poly_ml_rts_breakdown/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/71/ml_distinguish_proper_interrupts_from_poly_ml_rts_breakdown/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Robust handling of program exceptions in Isabelle/ML</title>
<description>ML antiquotation try provides variants of exception handling that avoids accidental capture of physical interrupts (which could affect ML semantics in unpredictable ways):
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/70/robust_handling_of_program_exceptions_in_isabelle_ml/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/70/robust_handling_of_program_exceptions_in_isabelle_ml/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Significantly reduced ML heap usage</title>
<description>ML heap usage and stored heap size has been significantly reduced, especially for applications with a lot of definitions in a locale or class context. The shrink factor is usually in the range 1.1 .. 2.0, but a factor 3 .. 10 has been seen in unusual situations. This often allows big applications to return to the "small" 64_32 memory model with its hard limit of 16 GiB, and thus reduce the heap size by another factor 1.8.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/67/significantly_reduced_ml_heap_usage/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/67/significantly_reduced_ml_heap_usage/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Support for interactive document preparation in PIDE</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/66/support_for_interactive_document_preparation_in_pide/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/66/support_for_interactive_document_preparation_in_pide/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Demo documents for well-known LaTeX styles</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/65/demo_documents_for_well-known_latex_styles/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/65/demo_documents_for_well-known_latex_styles/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Zstd compression for Isabelle/Scala and Isabelle/ML</title>
<description>Operations for Zstd compression (via Isabelle/Scala):
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/64/zstd_compression_for_isabelle_scala_and_isabelle_ml/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/64/zstd_compression_for_isabelle_scala_and_isabelle_ml/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>MLton compiler for x86_64-linux</title>
<description>The MLton compiler for x86_64-linux has been bundled as Isabelle component, since Ubuntu 22.04 no longer provides a suitable package. Note that on macOS, MLton is readily available via Homebrew: https://formulae.brew.sh/formula/mlton
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/63/mlton_compiler_for_x86_64-linux/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/63/mlton_compiler_for_x86_64-linux/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Scala SSH connections use OpenSSH executables</title>
<description>Isabelle/Scala SSH connections now use regular OpenSSH executables from the local system: ssh, scp, sftp; the old ssh-java component has been discontinued. This has various practical consequences:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/62/isabelle_scala_ssh_connections_use_openssh_executables/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/62/isabelle_scala_ssh_connections_use_openssh_executables/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle log" and option "show_states"</title>
<description>Command-line tool isabelle log has been refined to support multiple sessions, and to match messages against regular expressions (using Java Pattern syntax).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/61/command-line_tool_isabelle_log_and_option_show_states/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/61/command-line_tool_isabelle_log_and_option_show_states/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Display of schematic goal instance</title>
<description>The instantiation of schematic goals is now displayed explicitly as a list of variable assignments. This works for proof state output, and at the end of a toplevel proof. In rare situations, a proof command or proof method may violate the intended goal discipline, by not producing an instance of the original goal, but there is only a warning, no hard error.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/60/display_of_schematic_goal_instance/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/60/display_of_schematic_goal_instance/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Session ROOT files support 'chapter_definition' entries</title>
<description>Old-style {* verbatim *} tokens have been discontinued (legacy feature since Isabelle2019). INCOMPATIBILITY, use ‹cartouche› syntax instead.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/59/session_root_files_support_chapter_definition_entries/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/59/session_root_files_support_chapter_definition_entries/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System: Isabelle/Scala is now based on Scala 3</title>
<description>Isabelle/Scala is now based on Scala 3. This is a completely different compiler ("dotty") and a quite different source language (we are using the classic Java-style syntax, not the new Python-style syntax). Occasional INCOMPATIBILITY, see also the official Scala documentation https://docs.scala-lang.org/scala3/guides/migration/compatibility-intro.html
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/57/system_isabelle_scala_is_now_based_on_scala_3/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/57/system_isabelle_scala_is_now_based_on_scala_3/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/ML type Bytes.T and XZ compression</title>
<description>Type Bytes.T supports scalable byte strings, beyond the limit of String.maxSize (approx. 64 MB on 64_32 architecture).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/56/isabelle_ml_type_bytes.t_and_xz_compression/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/56/isabelle_ml_type_bytes.t_and_xz_compression/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tools "isabelle hg_sync" and "isabelle sync"</title>
<description>Command-line tool isabelle hg_sync synchronizes the working directory of a local Mercurial repository with a target directory, using rsync notation for destinations.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/55/command-line_tools_isabelle_hg_sync_and_isabelle_sync/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/55/command-line_tools_isabelle_hg_sync_and_isabelle_sync/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/VSCode as bundled application</title>
<description>Isabelle/VSCode Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/54/isabelle_vscode_as_bundled_application/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/54/isabelle_vscode_as_bundled_application/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotation "instantiate"</title>
<description>ML antiquotation "instantiate" allows to instantiate formal entities (types, terms, theorems) with values given ML. This works uniformly for "typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a keyword after the instantiation. A mode "(schematic)" behind the keyword means that some variables may remain uninstantiated (fixed in the specification and schematic in the result); by default, all variables need to be instantiated.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/52/ml_antiquotation_instantiate/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/52/ml_antiquotation_instantiate/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More robust (and more strict) treatment of abstractions within the context</title>
<description>Term operations under abstractions are now more robust (and more strict) by using the formal proof context in subsequent operations:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/51/more_robust_and_more_strict_treatment_of_abstractions_within_the_context/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/51/more_robust_and_more_strict_treatment_of_abstractions_within_the_context/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Nitpick with external/portable MiniSat</title>
<description>Nitpick: External solver "MiniSat" is available for all supported Isabelle platforms (including Windows and ARM); while "MiniSat_JNI" only works for Intel Linux and macOS.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/50/nitpick_with_external_portable_minisat/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/50/nitpick_with_external_portable_minisat/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improper proof command 'guess' provided by separate theory "Pure-ex.Guess"</title>
<description>The improper proof command guess is no longer part of by Pure, but provided by the separate theory Pure-ex.Guess. INCOMPATIBILITY, existing applications need to import session Pure-ex and theory Pure-ex.Guess. Afterwards it is usually better eliminate the guess command, using explicit obtain instead.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/48/improper_proof_command_guess_provided_by_separate_theory_pure-ex.guess/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/48/improper_proof_command_guess_provided_by_separate_theory_pure-ex.guess/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotations for object-logic judgement</title>
<description>ML antiquotations make_judgment and dest_judgment refer to corresponding functions for the object-logic of the ML compilation context. This supersedes older mk_Trueprop / dest_Trueprop operations.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/47/ml_antiquotations_for_object-logic_judgement/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/47/ml_antiquotations_for_object-logic_judgement/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML antiquotations for type constructors and term constants</title>
<description>ML antiquotations for type constructors and term constants:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/46/ml_antiquotations_for_type_constructors_and_term_constants/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/46/ml_antiquotations_for_type_constructors_and_term_constants/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/ML "build" combinators</title>
<description>The build combinators of various data structures help to build content from bottom-up, by applying an add function the empty value. For example:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/45/isabelle_ml_build_combinators/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/45/isabelle_ml_build_combinators/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Scalable operations for Thm.instantiate and Thm.generalize</title>
<description>ML structures TFrees, TVars, Frees, Vars, Names provide scalable operations to accumulate items from types and terms, using a fast syntactic order. The original order of occurrences may be recovered as well, e.g. via TFrees.list_set.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/44/scalable_operations_for_thm.instantiate_and_thm.generalize/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/44/scalable_operations_for_thm.instantiate_and_thm.generalize/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Configuration option "show_results"</title>
<description>Configuration option "show_results" controls output of final results in commands like 'definition' or 'theorem'. Output is normally enabled in interactive mode, but it could occasionally cause unnecessary slowdown. It can be disabled like this:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/43/configuration_option_show_results/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/43/configuration_option_show_results/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Bundles for lattice syntax</title>
<description>Theory HOL-Library.Lattice_Syntax has been superseded by bundle lattice_syntax: it can be used in a local context via include or in a global theory via unbundle. The opposite declarations are bundled as no_lattice_syntax. Minor INCOMPATIBILITY.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/42/bundles_for_lattice_syntax/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/42/bundles_for_lattice_syntax/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Localized commands 'syntax' and 'no_syntax'</title>
<description>Commands syntax and no_syntax now work in a local theory context, but there is no proper way to refer to local entities --- in contrast to notation and no_notation. Local syntax works well with bundle, e.g. see lattice_syntax vs. no_lattice_syntax in theory Main of Isabelle/HOL.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/41/localized_commands_syntax_and_no_syntax/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/41/localized_commands_syntax_and_no_syntax/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Scala improvements</title>
<description>Each Isabelle component may specify a Scala/Java jar module declaratively via etc/build.props (file names are relative to the component directory). E.g. see $ISABELLE_HOME/etc/build.props with further explanations in the system manual.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/40/isabelle_scala_improvements/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/40/isabelle_scala_improvements/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Reactivated ML profiling</title>
<description>ML profiling has been updated and reactivated, after some degration in
Isabelle2021:</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More predefined Isabelle symbols</title>
<description>More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). See also the group "Z Notation" in the Symbols dockable of Isabelle/jEdit.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/38/more_predefined_isabelle_symbols/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/38/more_predefined_isabelle_symbols/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System options short form (e.g. "-o document")</title>
<description>System option system_log specifies an optional log file for internal messages produced by Output.system_message in Isabelle/ML; the value true refers to console progress of the build job. This works for isabelle build or any derivative of it.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/37/system_options_short_form_e.g._-o_document/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/37/system_options_short_form_e.g._-o_document/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>High-quality blackboard-bold symbols</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/36/high-quality_blackboard-bold_symbols/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/36/high-quality_blackboard-bold_symbols/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Remote provers from SystemOnTPTP via Isabelle/Scala</title>
<description>Remote provers from SystemOnTPTP (notably for Sledgehammer) are now managed via Isabelle/Scala instead of perl; the dependency on libwww-perl has been eliminated (notably on Linux). Rare INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/35/remote_provers_from_systemontptp_via_isabelle_scala/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/35/remote_provers_from_systemontptp_via_isabelle_scala/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved LaTeX typesetting of ‹...›</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/34/improved_latex_typesetting_of_%E2%80%B9...%E2%80%BA/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/34/improved_latex_typesetting_of_%E2%80%B9...%E2%80%BA/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Clarified timeouts for Isabelle/ML tools</title>
<description>Timeouts for Isabelle/ML tools are subject to system option timeout_scale --- this already used for the overall session build process before, and allows to adapt to slow machines. The underlying Timeout.apply in Isabelle/ML treats an original timeout specification 0 as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY in boundary cases.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/33/clarified_timeouts_for_isabelle_ml_tools/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/33/clarified_timeouts_for_isabelle_ml_tools/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>External bash processes are always managed by Isabelle/Scala</title>
<description>External bash processes are always managed by Isabelle/Scala, in contrast to Isabelle2021 where this was only done for macOS on Apple Silicon.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/32/external_bash_processes_are_always_managed_by_isabelle_scala/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/32/external_bash_processes_are_always_managed_by_isabelle_scala/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved GUI look-and-feel</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/31/improved_gui_look-and-feel/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/31/improved_gui_look-and-feel/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/jEdit action "isabelle.goto-entity"</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/30/isabelle_jedit_action_isabelle.goto-entity/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/30/isabelle_jedit_action_isabelle.goto-entity/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Message logs from session build database</title>
<description>The command-line tool isabelle log prints prover messages from the build database of the given session, following the the order of theory sources, instead of erratic parallel evaluation. Consequently, the session log file is restricted to system messages of the overall build process, and thus becomes more informative.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/29/message_logs_from_session_build_database/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/29/message_logs_from_session_build_database/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Document antiquotation for Isabelle tools</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/27/document_antiquotation_for_isabelle_tools/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/27/document_antiquotation_for_isabelle_tools/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>PDF/HTML presentation in Isabelle/Scala, based on session build database</title>
<description>The command-line tool isabelle build provides option -P DIR to produce PDF/HTML presentation in the specified directory; -P: refers to the standard directory according to ISABELLE_BROWSER_INFO / ISABELLE_BROWSER_INFO_SYSTEM settings. Generated PDF documents are taken from the build database -- from this or earlier builds with option document=pdf.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/26/pdf_html_presentation_in_isabelle_scala_based_on_session_build_database/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/26/pdf_html_presentation_in_isabelle_scala_based_on_session_build_database/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Experimental support for arm64-linux platform</title>
<description>Experimental support for arm64-linux platform. The reference platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/25/experimental_support_for_arm64-linux_platform/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/25/experimental_support_for_arm64-linux_platform/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update external prover components for Sledgehammer etc.</title>
<description>Update/rebuild external provers on currently supported OS platforms, notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/24/update_external_prover_components_for_sledgehammer_etc./</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/24/update_external_prover_components_for_sledgehammer_etc./</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Include veriT component for "smt" method</title>
<description>An updated version of the veriT solver is now included as Isabelle component. It can be used in the smt proof method via smt (verit) or via declare [[smt_solver = verit]] in the context; see also session HOL-Word-SMT_Examples.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/23/include_verit_component_for_smt_method/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/23/include_verit_component_for_smt_method/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Document preparation engine updates</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/22/document_preparation_engine_updates/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/22/document_preparation_engine_updates/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session</title>
<description>Nitpick/Kodkod may be invoked directly within the running Isabelle/Scala session (instead of an external Java process): this improves reactivity and saves resources. This experimental feature is guarded by system option kodkod_scala (default: false).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/20/nitpick_kodkod_may_be_invoked_directly_within_the_running_isabelle_scala_session/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/20/nitpick_kodkod_may_be_invoked_directly_within_the_running_isabelle_scala_session/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>User-defined Isabelle server commands via isabelle_scala_service</title>
<description>Isabelle server allows user-defined commands via isabelle_scala_service.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/19/user-defined_isabelle_server_commands_via_isabelle_scala_service/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/19/user-defined_isabelle_server_commands_via_isabelle_scala_service/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>More systematic support for special directories</title>
<description>The shell function isabelle_directory (within etc/settings of components) augments the list of special directories for persistent symbolic path names. This improves portability of heap images and session databases. It used to be hard-wired for Isabelle + AFP, but other projects may now participate on equal terms.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/18/more_systematic_support_for_special_directories/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/18/more_systematic_support_for_special_directories/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Improved monitoring for Isabelle/ML and Java</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/17/improved_monitoring_for_isabelle_ml_and_java/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/17/improved_monitoring_for_isabelle_ml_and_java/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>ML statistics via an external Poly/ML process</title>
<description>ML statistics via an external Poly/ML process: this allows monitoring the runtime system while the ML program sleeps.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/16/ml_statistics_via_an_external_poly_ml_process/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/16/ml_statistics_via_an_external_poly_ml_process/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Theory_Data extend operation is obsolete and needs to be the identity function</title>
<description>Theory_Data extend operation is obsolete and needs to be the identity function; merge should be conservative and not reset to the empty value. Subtle INCOMPATIBILITY and change of semantics (due to Theory.join_theory from Isabelle2020). Special extend/merge behaviour at the begin of a new theory can be achieved via Theory.at_begin.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/15/theory_data_extend_operation_is_obsolete_and_needs_to_be_the_identity_function/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/15/theory_data_extend_operation_is_obsolete_and_needs_to_be_the_identity_function/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>System option pide_session is enabled by default</title>
<description>System option "pide_session" is enabled by default, notably for standard "isabelle build": it allows to invoke Isabelle/Scala operations from Isabelle/ML. Big build jobs (e.g. AFP) require extra heap space for the java process, e.g. like this in $ISABELLE_HOME_USER/etc/settings:
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/14/system_option_pide_session_is_enabled_by_default/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/14/system_option_pide_session_is_enabled_by_default/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of Isabelle/jEdit to jedit-5.6pre1</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/13/update_of_isabelle_jedit_to_jedit-5.6pre1/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/13/update_of_isabelle_jedit_to_jedit-5.6pre1/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Antiquotations for Isabelle systems programming</title>
<description>Document preparation ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/12/antiquotations_for_isabelle_systems_programming/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/12/antiquotations_for_isabelle_systems_programming/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Update of Isabelle/Phabricator setup</title>
<description>Isabelle/Phabricator setup has been updated to follow ongoing development: libphutil has been discontinued. Minor INCOMPATIBILITY: existing server installations should remove libphutil from /usr/local/bin/isabelle-phabricator-upgrade and each installation root directory (e.g. /var/www/phabricator-vcs/libphutil).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/11/update_of_isabelle_phabricator_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/11/update_of_isabelle_phabricator_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle sessions"</title>
<description>The command-line tool "isabelle sessions" explores the structure of Isabelle sessions and prints result names in topological order (on stdout).
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/10/command-line_tool_isabelle_sessions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/10/command-line_tool_isabelle_sessions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Slightly improved isabelle build_docker tool</title>
<description>The command-line tool isabelle build_docker has been slightly improved: it is now properly documented in the system manual.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/9/slightly_improved_isabelle_build_docker_tool/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/9/slightly_improved_isabelle_build_docker_tool/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Mixfix annotations may use single-quote-space as documented</title>
<description>Mixfix annotations may use "' " (single quote followed by space) to separate delimiters (as documented in the isar-ref manual), without requiring an auxiliary empty block. A literal single quote needs to be escaped properly. Minor INCOMPATIBILITY.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/8/mixfix_annotations_may_use_single-quote-space_as_documented/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/8/mixfix_annotations_may_use_single-quote-space_as_documented/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Support Java/VM monitoring via jconsole</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/7/support_java_vm_monitoring_via_jconsole/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/7/support_java_vm_monitoring_via_jconsole/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/jEdit actions and shortcuts for tooltips, messages, error positions</title>
<description>Isabelle/jEdit Prover IDE ###
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/6/isabelle_jedit_actions_and_shortcuts_for_tooltips_messages_error_positions/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/6/isabelle_jedit_actions_and_shortcuts_for_tooltips_messages_error_positions/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle scala_project"</title>
<description>The command-line tool "isabelle scala_project" creates a Gradle project configuration for Isabelle/Scala/jEdit, to support Scala IDEs such as IntelliJ IDEA.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/4/command-line_tool_isabelle_scala_project/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/4/command-line_tool_isabelle_scala_project/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Command-line tool "isabelle hg_setup"</title>
<description>The command-line tool "isabelle hg_setup" simplifies the setup of Mercurial repositories, with hosting via Phabricator or SSH file server access.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/2/command-line_tool_isabelle_hg_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/2/command-line_tool_isabelle_hg_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Isabelle/Phabricator setup</title>
<description>The command-line tool "isabelle phabricator_setup" facilitates self-hosting of the Phabricator software-development platform, with support for Git, Mercurial, Subversion repositories. This helps to avoid monoculture and to escape the gravity of centralized version control by Github and/or Bitbucket. For further documentation, see chapter "Phabricator server administration" in the "system" manual. A notable example installation is https://isabelle-dev.sketis.net/.
</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/1/isabelle_phabricator_setup/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/1/isabelle_phabricator_setup/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
</channel>
</rss>http://localhost:1200/isabelle-dev/blog/2 - Success ✔️<?xml version="1.0" encoding="UTF-8"?>
<rss xmlns:atom="http://www.w3.org/2005/Atom" version="2.0">
<channel>
<title>Isabelle Release</title>
<link>https://isabelle-dev.sketis.net/phame/blog/view/2/</link>
<atom:link href="http://localhost:1200/isabelle-dev/blog/2" rel="self" type="application/rss+xml"></atom:link>
<description>Isabelle Release - Made with love by RSSHub(https://github.com/DIYgod/RSSHub)</description>
<generator>RSSHub</generator>
<webMaster>i@diygod.me (DIYgod)</webMaster>
<language>en</language>
<lastBuildDate>Tue, 07 May 2024 17:53:08 GMT</lastBuildDate>
<ttl>5</ttl>
<item>
<title>Release Candidates for Isabelle2024</title>
<description>The official Isabelle2024 release is scheduled for mid May 2024. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2024 release</title>
<description>The next anticipated release is after Isabelle2023 (September 2023) is Isabelle2024 (May 2024). The distance between two releases is usually 8–10 months, but recently this got closer 11 months. To return to regularity, and to accommodate other side-conditions, the hot phase of the release is presently scheduled for 03-Apr..15-May-2024. The detailed plan is as follows:</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/69/plan_for_isabelle2024_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/69/plan_for_isabelle2024_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2023</title>
<description>The official Isabelle2023 release is scheduled for early September 2023. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/68/release_candidates_for_isabelle2023/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2022</title>
<description>The official Isabelle2022 release is scheduled for late October 2022. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/58/release_candidates_for_isabelle2022/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2021-1</title>
<description>The official Isabelle2021-1 release is scheduled for December 2021. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2021-1 release</title>
<description>The next anticipated release is Isabelle2021-1 (December 2021): as the distance between two releases is usually 8–10 months, there are sometimes 2 releases per year. This explains the slightly odd name tag, but in all other respects, Isabelle-2021-1 should be a perfectly normal official release.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/49/plan_for_isabelle2021-1_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/49/plan_for_isabelle2021-1_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2021</title>
<description>The official Isabelle2021 release is scheduled for February 2021. This blog entry is dynamically updated to follow the sequence of public release candidates. See also the workboard and the isabelle-release repository.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2021 release</title>
<description>The next anticipated release is Isabelle2021 (February 2021). The hot phase with release candidates will presumably be 28-Dec-2020 .. 15-Feb-2020.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/21/plan_for_isabelle2021_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/21/plan_for_isabelle2021_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Release Candidates for Isabelle2020</title>
<description>The official Isabelle2020 release is scheduled for April 2020. This blog entry is dynamically updated to follow the sequence of public release candidates.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
<item>
<title>Plan for Isabelle2020 release</title>
<description>The next anticipated release is Isabelle2020 (April 2020). The hot phase with release candidates will presumably be 01-Mar-2020 .. 15-Apr-2020.</description>
<link>https://isabelle-dev.sketis.net/phame/post/view/3/plan_for_isabelle2020_release/</link>
<guid isPermaLink="false">https://isabelle-dev.sketis.net/phame/post/view/3/plan_for_isabelle2020_release/</guid>
<pubDate>Invalid Date</pubDate>
<author>makarius</author>
</item>
</channel>
</rss> |
|
Successfully generated as following: http://localhost:1200/isabelle-dev/blog/1 - Failed ❌http://localhost:1200/isabelle-dev/blog/2 - Failed ❌ |
|
Successfully generated as following: http://localhost:1200/sketis/isabelle-dev/blog/1 - Failed ❌http://localhost:1200/sketis/isabelle-dev/blog/2 - Failed ❌ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Example for the Proposed Route(s) / 路由地址示例
New RSS Route Checklist / 新 RSS 路由检查表
PuppeteerNote / 说明