Fix PVerifier pages not showing up on P wiki

Author: Christine Zhou

Docs/docs/advanced/PVerifierLanguageExtensions/announcement.md

@@ -10,9 +10,9 @@ Formal verification is important to AWS’s software correctness program (Brooke
 
 ## 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](https://github.com/p-org/P/blob/major/P3.0/Docs/docs/advanced/PVerifierLanguageExtensions/install-pverifier.md); simple usage instructions are available [here](https://github.com/p-org/P/blob/major/P3.0/Docs/docs/advanced/PVerifierLanguageExtensions/using-pverifier.md).
+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](https://github.com/p-org/P/blob/major/P3.0/Docs/docs/advanced/PVerifierLanguageExtensions/twophasecommitverification.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
 

Docs/docs/advanced/PVerifierLanguageExtensions/outline.md

@@ -1,5 +1,5 @@
 !!! tip ""
-    **We recommend that you start with the [Tutorials](tutsoutline.md) to get familiar with
+    **We recommend that you start with the [Tutorials](../../tutsoutline.md) to get familiar with
     the P language and its tool chain.**
 
 ??? note "PVerifier Extension Top Level Declarations Grammar"

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

@@ -2,7 +2,7 @@
     Before moving forward, we assume that you have successfully installed
     the [PVerifier](install-pverifier.md).
 
-In this section, we provide an overview of the steps involved in verifying a P program using the [two-phase commit](../tutorial/twophasecommit.md) example in Tutorials.
+In this section, we provide an overview of the steps involved in verifying a P program using the [two-phase commit](../../tutorial/twophasecommit.md) example in Tutorials.
 
 ??? info "Get the Two-Phase Commit Example Locally"
     We will use the [TwoPhaseCommit](https://github.com/p-org/P/tree/master/Tutorial/2_TwoPhaseCommit) example from Tutorial folder in P repository to describe the process of verifying a P program. Please clone the P repo and navigate to the
@@ -24,7 +24,7 @@ To verify a P program using the PVerifier, you need to:
 1. Configure your project to use PVerifier as the target in your `.pproj` file
 2. Compile the project using the P compiler
 
-This process follows the same workflow described in [Using P](../../getstarted/usingp.md), except that we specify `PVerifier` as the backend instead of other targets like `CSharp` or `Java`.
+This process follows the same workflow described in [Using P](../../getstarted/usingP.md), except that we specify `PVerifier` as the backend instead of other targets like `CSharp` or `Java`.
 
 #### Executing the verification
 

Docs/mkdocs.yml

@@ -74,6 +74,16 @@ nav:
 #        - Installing PSym: advanced/psym/install.md
 #        - Using PSym: advanced/psym/usingPSym.md
       - P Exhaustive Mode: advanced/pex.md
+      - PVerifier:
+        - Announcement: advanced/PVerifierLanguageExtensions/announcement.md
+        - Outline: advanced/PVerifierLanguageExtensions/outline.md
+        - Installation: advanced/PVerifierLanguageExtensions/install-pverifier.md
+        - Using PVerifier: advanced/PVerifierLanguageExtensions/using-pverifier.md
+        - Pure Functions: advanced/PVerifierLanguageExtensions/pure.md
+        - Init Conditions: advanced/PVerifierLanguageExtensions/init-condition.md
+        - Specifications: advanced/PVerifierLanguageExtensions/specification.md
+        - Lemmas and Proofs: advanced/PVerifierLanguageExtensions/proof.md
+        - Two Phase Commit Verification: advanced/PVerifierLanguageExtensions/twophasecommitverification.md
   - Language Manual:
       - P Program (Outline): manualoutline.md
       - P DataTypes: manual/datatypes.md