Warn about outdated content & misc. housekeeping & slicing/caching docs

.gitignore

@@ -1,4 +1,5 @@
 site/
+/public
 
 .DS_Store
 *.out

Makefile

@@ -1,5 +1,5 @@
 prepare:
-	pip install --user mkdocs mkdocs-material pymdown-extensions pygments markdown-blockdiag mkdocs-bibtex markdown-aafigure==v201904.0004 mkdocs-build-plantuml-plugin 'Pillow<10' 'Markdown<3.4'
+	pip install --user mkdocs mkdocs-material pymdown-extensions pygments markdown-blockdiag mkdocs-bibtex markdown-aafigure==v202104.1011 mkdocs-build-plantuml-plugin Pillow Markdown
 
 serve:
 	mkdocs serve

README.md

@@ -40,8 +40,8 @@ Install the necessary libraries locally:
 
 ```
 $ pip install --user mkdocs mkdocs-material pymdown-extensions pygments \
-                     markdown-blockdiag mkdocs-bibtex markdown-aafigure==v201904.0004 \
-                     mkdocs-build-plantuml-plugin 'Pillow<10' 'Markdown<3.4'
+                     markdown-blockdiag mkdocs-bibtex markdown-aafigure==v202104.1011 \
+                     mkdocs-build-plantuml-plugin Pillow Markdown
 ```
 
 You can start development web-server, which automatically rerender and refresh

docs/changelog.md

@@ -1,5 +1,36 @@
 # Changelog
 
+## [2.12.2](https://github.com/KeYProject/key/releases/tag/KeY-2.12.2) (2023-11-10)
+This release contains bug fixes and performance enhancements.
+
+### Performance: 
+  - Z3 is now configurable to use the QF (quantifier-free) theory for problems without quantifiers.
+
+### Bug Fixes:
+  - The pretty printer no longer throws a ClassCastException when printing taclets using schema variables of an array type.
+  - Nullable and non-null modifiers attached to model methods are no longer lost.
+  - Term rule indices are now always up-to-date, preventing potential prover crashes.
+  - The counter-example dialog no longer freezes the GUI, if the example generation fails.
+  - The actual proof status and proof status icon in the task overview are now  consistent after pruning without requiring a manual refresh.
+
+## [2.12.1](https://github.com/KeYProject/key/releases/tag/KEY-2.12.1) (2023-10-13)
+
+### Bug fixes
+
+- SMT solvers are properly terminated on timeout
+- Proof Macro statistics are kept visible and only count the newly applied rules
+- Stop button is disabled after use, re-enabled after stop completes (this is to avoid double activation)
+- Fully disable origin tracking if it is disabled
+- Proof slicing works even if a cut introduced no new formulas in any branch
+- When marking goal(s) as interactive/automatic, proof tree no longer loses expansion state
+- Fix proof tree behaviour when toggling goals
+- Fix branch selection in caching
+- Fix gradle detection of git branch
+- Fix unit test
+- Fix environments not disposed in tests, keep strategy info visible after applying
+- Proof macro: record statistics correctly
+- Fix: KeY files with errors cannot be edited
+
 ## [2.12.0](https://github.com/KeYProject/key/releases/tag/KeY-2.12.0) (2023-08-18)
 
 ### Breaking changes
@@ -14,8 +45,8 @@
 * [Support for floating points](https://git.key-project.org/key/key/-/merge_requests/403)
 * [Support for JML asserts/assumes as standalone construct (instead of transforming into blockcontracts)](https://git.key-project.org/key/key/-/merge_requests/494), [Support of \old() in JML asserts](https://git.key-project.org/key/key/-/merge_requests/533)
 * [Support for JML math mode specifiers (and changed default semantics to spec_bigint_math)](https://github.com/KeYProject/key/pull/3014)
-* [Proof Slicing](user/ProofSlicing.md) system ([#3026](https://github.com/KeYProject/key/pull/3026))
-* [Proof Caching](user/ProofCaching.md) system
+* [Proof Slicing](../user/ProofSlicing/) system ([#3026](https://github.com/KeYProject/key/pull/3026))
+* [Proof Caching](../user/ProofCaching/) system
 * [Run the Javac compiler when loading Java code](https://git.key-project.org/key/key/-/merge_requests/581)
 * Migration to GitHub
     * [Files for Github Actions](https://git.key-project.org/key/key/-/merge_requests/634)

docs/devel/How2ExtRecoder.md

@@ -1,10 +1,10 @@
 # How to extend recoder
 
-*Schmitt, XXXX*
+*Schmitt*
 
-!!! abstract
+!!! danger
 
-    Here should be a short abstract.
+    Recoder is planned to be removed. See [PR #3120](https://github.com/KeYProject/key/pull/3120).
 
 These notes explain the changes to the existing code of the KeY system that are
 necessary to add a new data type to JML. If the new data type is only used in

docs/user/HowToTaclet.md → docs/devel/HowToTaclet.md

@@ -1,4 +1,4 @@
-# How to write a Taclet
+# How to write new taclets
 
 New prover rules in KeY can be added in form of built-in rules[^1] written in plain
 Java code and as so-called "taclets" ("schematic theory-specific rules").
@@ -8,15 +8,14 @@ schematic parts are displayed to the user, making the rule application more
 transparent. Almost all rules implemented for KeY are defined as taclets (with
 the exception of special rules like method contract application, loop invariant
 application (so far) and one-step-simplification). For information about
-taclets, please consult the [book chapter "Proof Search with
-Taclets"](https://link.springer.com/chapter/10.1007/978-3-319-49812-6_4) of the
+taclets, please consult the [book chapter "Proof Search with Taclets"](https://link.springer.com/chapter/10.1007/978-3-319-49812-6_4) of the
 2nd KeY book.
 
 This article covers the necessary basics for adding new taclets to the KeY
 system. In particular, the following topics are discussed:
 
 
-##  How to add new taclets
+##  How to add a taclet
 
 The standard location for `.key` files containing taclets is in the `key.core`
 project, location `resources/de/uka/ilkd/key/proof/rules` (*note*: unless stated
@@ -39,6 +38,10 @@ heuristics. Default rule sets are defined in the file
 
 ## How to extend the taclet language
 
+!!! danger
+
+    This section does not reflect recent KeY developments. [The parser was recently rewritten](../../devel/NewKeyParser/).
+
 Sometimes, especially when one wants to introduce new symbolic execution
 concepts, the existing taclet language is not expressive enough and has to be
 extended. There are four things one might have to extend to support new taclet

docs/devel/Listeners.md

@@ -47,7 +47,7 @@ When in "auto mode", the KeY interface (except for the stop button) will not res
 
 ### InteractionListener
 
-Listener for interactions done by the user: settings changed, macro started, rule applied, ...
+Listener for interactions done by the user: settings changed, macro started, rule applied, proof pruned, ...
 
 ## Proof
 
@@ -103,4 +103,4 @@ Receives an event whenever a value in the Lookup instance changes.
 
 ### MergeRuleProgressListener
 
-When applying a merge rule, this listener will be notified for each merged branch.
+When applying a merge rule, this listener will be notified for each merged branch.

docs/devel/NewKeyParser.md

@@ -10,7 +10,7 @@
 
 ## Background
 
-With the MR !278, a new lexer and parser for the KeY language is introduced. The KeY language is used to parse the `*.key` and `*.proof`, and is also used as the input language for entering terms in the user interface. 
+With the MR [!278](https://git.key-project.org/key/key/-/merge_requests/278), a new lexer and parser for the KeY language is introduced. The KeY language is used to parse the `*.key` and `*.proof`, and is also used as the input language for entering terms in the user interface. 
 
 In general, this parser was hard to maintain and extend over the years.
 The old parser was a traditional ANTLR3 parser, where the grammar and the source code are mixed up. It also some lookahead were required.  KeY files are interpreted on different levels: The first level are the basic notions (e.g. sorts and choice options), second level are the functions, predicates and transformers, and the third level are the axioms, contracts and rules. These parsing level are required due to the dependencies between these logical entities, e.g. a rule requires certain functions and sorts during its interpretation. In the old KeY-Parser, each file is parsed (and read) on a specific level. Hence, to interpret a KeY file, multiple parse passes are required. 

docs/devel/Testing/RunAllProves.md

@@ -56,6 +56,10 @@ test runs.
 
 ### Syntax of the Proof Collection/Index File
 
+!!! danger
+
+    This section does not reflect recent KeY developments. In particular, this list is now defined in code.
+
 There is an proof collection (or index) file containing the
 declaration the sets of .key files that will be tested during
 RunAllProofs test run. This file is currently located in KeY