Completing and restructuring the user docs a bit

Author: mattulbrich

Makefile

@@ -2,7 +2,7 @@ prepare:
 	pip install --user -r requirements.txt 
 
 serve:
-	mkdocs serve
+	mkdocs serve --livereload
 
 build:
 	mkdocs build

docs/extra.css

@@ -0,0 +1,3 @@
+.md-nav__item--section > .md-nav__link[for] {
+    color: var(--md-typeset-color) !important;
+}

docs/user/index.md

@@ -0,0 +1,24 @@
+# Welcome to KeY Documentation
+
+Welcome to the **KeY user documentation index**. Use the navigation sidebar on the left to explore the available resources. This site provides information you need to get started with KeY, delve into detailed topics regarding user interactions, and learn about the proof script technology built into KeY.
+
+Whether you're new to KeY or an experienced user, this documentation is designed to support your workflow—from interactive proving to advanced automated proof scripting.
+
+## What Can You Find Here?
+
+If you're just starting with KeY, the **User Guide** section will help you begin your journey. Check out the **Changelog** for recent updates, and find answers to common questions in the **FAQ**.
+
+- The **Topics** section dives deeper into various aspects of using KeY, including
+- **User Interface Features**: Explore KeY’s unique UI capabilities
+- Dive into KeY’s **Proof Scripts** section to learn about proof scripts
+
+
+## Learn More
+
+Additional information is available on the [KeY Project homepage](https://key-project.org) or on our [GitHub repository](https://github.com/KeYProject/key/), where you can find the source code, development updates, and contribute to the project.
+
+We hope you find this documentation helpful and informative. Happy proving!
+
+## Disclaimer
+
+Some content of theses pages has been co-produced by AI agents, mainly as summaries of other pages, publications or other sources.

docs/workbench/Proof Scripts/commands.md

@@ -1,16 +1,54 @@
 # Scripting Interactive Proofs
 
-To persist interactions performed during proof contsruction in KeY and to replay these
-interactions, KeY allows users to use proof scripts.
 
-In this documentation the scripts that allow for branching statements are eplained. (see [Explanation
-of linear scripts](./linearScripts.md) for the other version of scripts in KeY)
+### Motivation for Proof Scripts in KeY
 
-The three main building blocks of the scripting language are mutators, control-flow
-structures, and selectors for proof goals. We describe the general concepts in the
-following. 
+Formal verification in KeY often requires revisiting and refining
+intermediate specifications like loop invariants through a highly
+iterative process. However, even small adjustments to the program or
+its specification can invalidate entire proofs, necessitating complete
+reconstruction. Although KeY's current mechanism can replay proofs
+from fine-grained rule applications, it is brittle and vulnerable to
+minor changes. Especially in low-automation contexts, where many steps
+are performed manually, repeating those steps is time-consuming and
+error-prone.
 
-##Mutators. 
-Mutators are the most basic building blocks of the proof
-script. When executed a mutator may change the proof script state by changing
-variables and the underlying proof state by adding nodes to the proof tree.
+**Proof scripts offer a solution** by capturing the essential and complex reasoning steps, while delegating routine proof search tasks to the automatic engine. This significantly improves maintainability and usability of proofs as code or specifications evolve.
+
+### Benefits of Proof Scripts in KeY
+
+-  **Robustness to Changes**: Scripts focus on core proof decisions rather than low-level steps, making them resilient to small changes in the code or specification.
+-  **Increases Comprehensibility**: Proof scripts can convey the high-level proof ideas that allow users to understand the reasoning.
+-  **Maintains Manual Effort**: Records manual proof actions (e.g., quantifier instantiations or definition expansions) so that they don't need to be repeated after specification changes.
+-  **Improved Automation Synergy**: Proof scripts guide the prover through the difficult parts while letting the automated search handle simpler steps.
+-  **Scalability to Complex Proofs**: Handles proof branching more effectively, applying scripts only where user interaction is needed.
+-  **Better Usability over Previous Scripting**: Avoids complex top-level goal selection required in earlier global script mechanisms.
+-  **Facilitates Proof Reuse**: Allows key insights and strategies to persist across code revisions, supporting iterative verification workflows.
+
+Proof scripts are textual representations of rule applications,
+settings changes and macro invocations. They are notated in linear
+order. The target of a script command is usually the first open goal
+in the proof tree, i.e., the first reached when traversing the proof
+tree (not necessarily the first in the Goal pane in the GUI).
+
+## Proof Script Languages
+
+There are two flavours of proof script languages. One more low-level
+for the interaction on the level of JavaDL and one for more high-level
+interaction on the level of JML annotated to Java code.
+
+### Linear Proof Scripts[^1]
+
+[Documentation of Linear Proof Scripts](linearScripts)
+
+Linear scripts are added to entire JavaDL proof obligations. They can
+be loaded interactively or stored in `.key` files.
+
+### JML Proof Scripts
+
+[Documentation of JML Proof Scripts](jml)
+
+JML scripts are added to individual assertions of a Java method. They
+are annotated as JML comments in `.java` files.
+
+[^1]: That is a working title name – might be subject to change.

docs/workbench/Proof Scripts/index.md

@@ -1,4 +1,4 @@
-# Proof Scripts in JML
+# Proof Scripts in JML 
 
 !!! note
     This describes proof scripts from JML as opposed to [linear scripts](../linearScripts)
@@ -149,3 +149,7 @@ Here are some examples of proof scripts in JML:
 ### Proof of Boyer-More using JML proof scripts
 
 see https://github.com/KeYProject/key/blob/96a6a98328bb9dbaadfb5b54e11b29230e77dfe9/key.ui/examples/heap/BoyerMoore/src/BoyerMoore.java
+
+### Proof of the [IPS4O sorting algorithm](https://doi.org/10.1007/978-3-031-57246-3_15) (partially) using scripts
+
+see https://github.com/KeYProject/ips4o-verify/blob/pfeifer/STTT/src/main/java/de/wiesler/Sorter.java

docs/workbench/Proof Scripts/jml.md

@@ -1,4 +1,4 @@
-# Linear Proof Scripts
+# Linear Proof Scripts[^1]
 
 !!! note
     This covers linear scripts. Scripts can also be attached to [JML assertions with scripts](../jml).
@@ -122,3 +122,4 @@ in the KeY repository:
 * https://github.com/KeYProject/key/blob/main/key.ui/examples/heap/quicksort/sort.key
 * https://github.com/KeYProject/key/blob/main/key.ui/examples/heap/quicksort/sort.script
 
+[^1]: "Linear Scripts" is a working title name – might be subject to change.

docs/workbench/Proof Scripts/linearScripts.md

@@ -2,8 +2,10 @@
 
 *Mattias Ulbrich <[email protected]>, 2015*
 
-!!! note
+!!! warning 
     This is the original announcement and probably a bit outdated.
+
+!!! note
     Experimental feature: Proof scripts are currently only visible in the GUI if KeY
     is launched with the `--experimental` option. Concrete syntax is subject to
     change.

docs/workbench/Proof Scripts/original.md

@@ -90,15 +90,17 @@ nav:
 #      - quicktour/proving.md
 #      - quicktour/appendix.md
   - User Guide:
+      - user/index.md
       - changelog.md
       - user/FAQ.md
-      - user/ADTs.md
-      - user/Classpath.md
-      - user/Interactive.md
-      - user/JavaDLinJML.md
-      - user/RemoveGenerics.md
-      - user/Polarity.md
-      - user/JavaGrammar.md
+      - Topics:
+          - user/ADTs.md
+          - user/Classpath.md
+          - user/Interactive.md
+          - user/JavaDLinJML.md
+          - user/RemoveGenerics.md
+          - user/Polarity.md
+          - user/JavaGrammar.md
       - UI Features:
           - user/UiFeatures/index.md
           - user/Exploration.md
@@ -160,6 +162,8 @@ nav:
           - devel/Testing/parserMessageTest.md
       - Write Documentation: "devel/howtodoc/index.md"
 
+extra_css:
+  - extra.css
 
 
 #  nav_style: dark