Updated documentation

.github/workflows/pchatbot-contract-tests.yml

@@ -0,0 +1,58 @@
+name: PeasyAI Tests
+
+on:
+  push:
+    paths:
+      - "Src/PeasyAI/**"
+      - ".github/workflows/pchatbot-contract-tests.yml"
+  pull_request:
+    paths:
+      - "Src/PeasyAI/**"
+      - ".github/workflows/pchatbot-contract-tests.yml"
+
+jobs:
+  unit-tests:
+    name: Unit Tests
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: Src/PeasyAI
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          python -m pip install -r requirements.txt
+
+      - name: Run unit tests
+        run: make test-unit
+
+  contract-tests:
+    name: Contract Tests
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: Src/PeasyAI
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          python -m pip install -r requirements.txt
+
+      - name: Run MCP contract tests
+        run: make test-contracts

.github/workflows/peasyai-release.yml

@@ -0,0 +1,73 @@
+name: PeasyAI Release
+
+on:
+  push:
+    tags:
+      - "peasyai-v*"
+
+permissions:
+  contents: write
+
+jobs:
+  build-and-release:
+    name: Build wheel & attach to GitHub Release
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: Src/PeasyAI
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      - name: Install build tools
+        run: python -m pip install --upgrade pip build
+
+      - name: Extract version from tag
+        id: version
+        run: |
+          TAG="${GITHUB_REF#refs/tags/peasyai-v}"
+          echo "version=$TAG" >> "$GITHUB_OUTPUT"
+
+      - name: Set version in pyproject.toml
+        run: |
+          sed -i "s/^version = .*/version = \"${{ steps.version.outputs.version }}\"/" pyproject.toml
+
+      - name: Build wheel and sdist
+        run: python -m build
+
+      - name: Run tests
+        run: |
+          python -m pip install -r requirements.txt
+          make test
+
+      - name: Create GitHub Release
+        uses: softprops/action-gh-release@v2
+        with:
+          name: "PeasyAI v${{ steps.version.outputs.version }}"
+          body: |
+            ## PeasyAI v${{ steps.version.outputs.version }}
+
+            ### Install
+
+            ```bash
+            pip install https://github.com/${{ github.repository }}/releases/download/peasyai-v${{ steps.version.outputs.version }}/peasyai_mcp-${{ steps.version.outputs.version }}-py3-none-any.whl
+            ```
+
+            Then configure:
+
+            ```bash
+            peasyai-mcp init        # creates ~/.peasyai/settings.json
+            peasyai-mcp config      # verify setup
+            ```
+
+            See the [README](https://github.com/${{ github.repository }}/blob/main/Src/PeasyAI/README.md) for full setup instructions.
+          files: |
+            Src/PeasyAI/dist/*.whl
+            Src/PeasyAI/dist/*.tar.gz
+          fail_on_unmatched_files: true

.github/workflows/publishdocs.yml

@@ -10,14 +10,14 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v2
-      - name: Install pip
-        run: python3 -m pip install --upgrade pip setuptools wheel
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+          cache: 'pip'
+          cache-dependency-path: Docs/requirements.txt
       - name: Install MkDocs
-        run: |
-          pip install mkdocs
-          pip install mkdocs-macros-plugin
-          pip install mkdocs-material
+        run: pip install -r Docs/requirements.txt
       - name: MkDocs build
         working-directory: ./Docs
         run: mkdocs build

Docs/docs/advanced/PProject.md

@@ -1,30 +1,41 @@
+## P Project File
 
-The current project file interface is a simple mechanism to provide all the required inputs to the compiler in XML format.
+The P project file (`.pproj`) is a simple XML mechanism to provide all the required inputs to the compiler.
 
-The P project file below is taken from the [TwoPhaseCommit](https://github.com/p-org/P/blob/master/Tutorial/2_TwoPhaseCommit/TwoPhaseCommit.pproj) example in Tutorials.
+---
 
-``` xml
+### Example
+
+The project file below is from the [TwoPhaseCommit](https://github.com/p-org/P/blob/master/Tutorial/2_TwoPhaseCommit/TwoPhaseCommit.pproj) example:
+
+```xml
 <!-- P project file for the Two Phase Commit example -->
 <Project>
-<ProjectName>TwoPhaseCommit</ProjectName>
-<InputFiles>
-	<PFile>./PSrc/</PFile>
-	<PFile>./PSpec/</PFile>
-	<PFile>./PTst/</PFile>
-	<PFile>./PForeign/</PFile>
-</InputFiles>
-<OutputDir>./PGenerated/</OutputDir>
-<!-- Add the dependencies for the Timer machine -->
-<IncludeProject>../Common/Timer/Timer.pproj</IncludeProject>
-<!-- Add the dependencies for the FailureInjector machine -->
-<IncludeProject>../Common/FailureInjector/FailureInjector.pproj</IncludeProject>
+  <ProjectName>TwoPhaseCommit</ProjectName>
+  <InputFiles>
+    <PFile>./PSrc/</PFile>
+    <PFile>./PSpec/</PFile>
+    <PFile>./PTst/</PFile>
+    <PFile>./PForeign/</PFile>
+  </InputFiles>
+  <OutputDir>./PGenerated/</OutputDir>
+  <!-- Add the dependencies for the Timer machine -->
+  <IncludeProject>../Common/Timer/Timer.pproj</IncludeProject>
+  <!-- Add the dependencies for the FailureInjector machine -->
+  <IncludeProject>../Common/FailureInjector/FailureInjector.pproj</IncludeProject>
 </Project>
 ```
 
-The `<InputFiles>` block provides all the P files that must be compiled together for this project.
-In `<PFile>`, you can either specify the path to the P file or to a folder and the P compiler includes all the files in the folder during compilation.
-The `<ProjectName>` block provides the name for the project which is used as the output file name.
-The `<OutputDir>` block provides the output directory for the generated code.
-Finally, `<IncludeProject>` block provides path to other P projects that must be included as dependencies during compilation.
-The P compiler simply recursively copies all the P files in the dependency projects and compiles them together.
-This feature provides a way to split the P models for a large system into subprojects that can share models.
+---
+
+### Project File Reference
+
+| Element | Description |
+|---------|-------------|
+| **`<ProjectName>`** | Name for the project, used as the output file name |
+| **`<InputFiles>` / `<PFile>`** | P files or folders to compile. When a folder is specified, all `*.p` files in it are included |
+| **`<OutputDir>`** | Output directory for the generated code |
+| **`<IncludeProject>`** | Path to other `.pproj` files to include as dependencies. The compiler recursively copies all P files from dependency projects and compiles them together |
+
+!!! tip ""
+    The `<IncludeProject>` feature provides a way to split P models for a large system into subprojects that can share models.

Docs/docs/advanced/PVerifierLanguageExtensions/announcement.md

@@ -1,3 +1,5 @@
+## PVerifier: Formal Proofs for P Programs
+
 # Announcing the New Verification Backend for P
 
 We are excited to announce the release of a new verification backend as part of the 3.0 release of the P programming language! This backend, which we call the P Verifier, allows you to prove that your systems behave correctly under all possible scenarios. The P Verifier is based on Mora et al. ([OOPSLA '23](https://dl.acm.org/doi/10.1145/3622876)) and uses UCLID5 (Polgreen et al., [CAV '22](https://dl.acm.org/doi/10.1007/978-3-031-13185-1_27)).
@@ -8,12 +10,16 @@ The new verification backend allows users to **prove** that their system design
 
 Formal verification is important to AWS’s software correctness program (Brooker and Desai, [Queue '25](https://doi.org/10.1145/3712057)). Several formal tools have had successful applications within AWS in their respective domains. The new verification backend in P gives users the benefits of correctness proofs for the domain of distributed systems design, all while preserving the existing benefits of systematic testing.
 
+---
+
 ## Getting Started and Tutorial
 
 To start using the P Verifier, you must install P along with the verification dependencies (UCLID5 and an SMT solver like Z3). Detailed installation instructions are available [here](install-pverifier.md); simple usage instructions are available [here](using-pverifier.md).
 
 To help you get acquainted with the new verification features, we have prepared a comprehensive tutorial that walks you through the formal verification of a simplified two-phase commit (2PC) protocol. This tutorial covers the key concepts and steps of using the verification backend. You can find the tutorial [here](twophasecommitverification.md).
 
+---
+
 ## Industrial Application Inside Amazon Web Services
 
 The two-phase commit protocol described in the tutorial is deliberately simplified to help new users get started. In that protocol, one coordinator works with a fixed set of participants to agree on a single boolean value. Industrial systems, however, call for a number of generalizations. 

Docs/docs/advanced/PVerifierLanguageExtensions/init-condition.md

@@ -1,3 +1,5 @@
+## Init Conditions
+
 # Initialization Conditions
 
 Initialization conditions let us constrain the kinds of systems that we consider for formal verification. You can think of these as constraints that P test harnesses have to satisfy to be considered valid.

Docs/docs/advanced/PVerifierLanguageExtensions/install-pverifier.md

@@ -1,10 +1,14 @@
+## Installing PVerifier
+
 # Install Instructions for Amazon Linux
 
 PVerifier requires several dependencies to be installed. Follow the steps below to set up your environment.
 
 !!! success ""
     After each step, please use the troubleshooting check to ensure that each installation step succeeded.
 
+---
+
 ### [Step 1] Install Java 11
 
 ```sh
@@ -20,6 +24,8 @@ sudo yum install java-11-amazon-corretto-devel maven
 
     If you get `java` command not found error, most likely, you need to add the path to `java` in your `PATH`.
 
+---
+
 ### [Step 2] Install SBT
 
 ```sh
@@ -36,6 +42,8 @@ sudo yum install sbt
 
     If you get `sbt` command not found error, most likely, you need to add the path to `sbt` in your `PATH`.
 
+---
+
 ### [Step 3] Install .NET 8.0
 
 Install .NET 8.0 from Microsoft:
@@ -60,6 +68,8 @@ The purpose of copying the .NET distribution into `/usr/share/dotnet` is to make
 export DOTNET_ROOT=$HOME/.dotnet
 ```
 
+---
+
 ### [Step 4] Install Z3
 
 ```sh
@@ -103,6 +113,8 @@ Note:
 
     to install gcc10-gcc and gcc10-g++ and replace the string `gcc` with `gcc10-` in `config.mk`.
 
+---
+
 ### [Step 5] Install UCLID5
 
 ```sh
@@ -130,6 +142,8 @@ Note:
 
     If you get `uclid` command not found error, most likely, you need to add the path to `uclid` in your `PATH`.
 
+---
+
 ### [Step 6] Install PVerifier
 
 The following steps will build P with PVerifier by running the regular P build on the PVerifier branch of the repository.

Docs/docs/advanced/PVerifierLanguageExtensions/outline.md

@@ -1,3 +1,5 @@
+## PVerifier Outline
+
 !!! tip ""
     **We recommend that you start with the [Tutorials](../../tutsoutline.md) to get familiar with
     the P language and its tool chain.**

Docs/docs/advanced/PVerifierLanguageExtensions/proof.md

@@ -1,3 +1,5 @@
+## Lemmas and Proofs
+
 # Lemmas and Proof Scripts
 
 Lemmas and proof scripts go hand in hand in the P Verifier. Lemmas allow you to decompose specifications and proof scripts allow you to relate lemmas to write larger proofs.
@@ -90,6 +92,8 @@ Where `targetN` are the names of lemmas or invariants to verify, and `helper` is
     }
     ```
 
+---
+
 ### Benefits of Proof Scripts
 
 1. **Organization**: Break down complex proofs into manageable parts

Docs/docs/advanced/PVerifierLanguageExtensions/pure.md

@@ -1,3 +1,5 @@
+## Pure Functions
+
 ??? note "P Pure Function Declaration Grammar"
 
     ```

Docs/docs/advanced/PVerifierLanguageExtensions/specification.md

@@ -1,3 +1,5 @@
+## Specifications
+
 # Specifications
 
 The P verifier adds three kinds of specifications: global invariants, loop invariants, and function contracts. We cover each type in its own subsection below.
@@ -83,6 +85,8 @@ P provides special predicates for specifying message state:
 - `inflight e`: True if message `e` has been sent but not yet received
 - `sent e`: True if message `e` has been sent (regardless of whether it has been received)
 
+---
+
 ### Quantifiers
 
 P supports several quantifier expressions for specifying properties over collections: