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,23 @@
 # Changelog
 
+## [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 +32,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/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.