website: minor improvements and add search

website/docs/heyvl/README.md

@@ -9,24 +9,10 @@ The main innovation is that it supports _quantitative_ reasoning via its constru
 Refer to our [publications](../publications.md) for details on the theory.
 
 A HeyVL file consists of a sequence of declarations: [procedure](./procs.md) and [domain declarations](./domains.md).
+Refer to those for more information.
 
 ```mdx-code-block
 import DocCardList from '@theme/DocCardList';
 
 <DocCardList />
 ```
-
-## Use the source, Luke
-
-We do not formally describe the syntax of HeyVL in this documentation.
-You can find a more formal definition in the [`src/front/parser/grammar.lalrpop`](https://github.com/moves-rwth/caesar/blob/main/src/front/parser/grammar.lalrpop) file that specifies the syntax used to generate Caesar's parser.
-It is written in the [LALRPOP language](https://lalrpop.github.io/lalrpop/tutorial/index.html).
-
-## Examples
-
-The [`pgcl/examples-heyvl`](https://github.com/moves-rwth/caesar/tree/main/pgcl/examples-heyvl) directory contains the machine-translated HeyVL code for our pGCL examples.
-Note that they are just sequences of HeyVL statements without wrapping procedure declarations.
-Refer to the page on the [pGCL frontend](../pgcl.md) for more information.
-
-Caesar's integration tests in [`tests/`](https://github.com/moves-rwth/caesar/tree/main/tests) can also serve as a reference.
-Refer to the [development guide](../devguide.md#caesar) for more information about these tests.

website/docs/heyvl/procs.md

@@ -48,7 +48,9 @@ Let us decompose the example into its parts:
  3. We have one **output parameter** `x` of type [`UInt`](../stdlib/numbers.md#uint).
     - There may be multiple parameters (input and output), which can be separated by commas (e.g. `init_x: UInt, init_y: UInt`).
  4. The `pre` declares the **pre-expectation** `init_x + 0.5`. It is evaluated in the *initial state* (when calling the proc). This is why it is called "pre" (= before running the proc).
+    - The `pre` is an expression of type [`EUReal`](../stdlib/numbers.md#eureal) over the input parameters.
  5. The `post` is the **post-expectation** `x` and evaluated in the final states of the proc (post = after running the proc). We always compare its expected value against the pre.
+    - The `post` is an expression of type [`EUReal`](../stdlib/numbers.md#eureal) over the input and output parameters.
  6. The **body of the proc** assigns `init_x` to `x`. We then do a [probabilistic coin flip](../stdlib/distributions.md#symbolic-with-probabilities) and assign `true` to `prob_choice` with probability `0.5` (and `false` with probability `0.5`). It determines the expected value ($\mathbb{E}$) we look at.
     - See [documentation on statements](./statements.md) for more information.
     - [The body is optional](#procs-without-body).

website/docusaurus.config.js

@@ -173,6 +173,11 @@ const config = {
         darkTheme: prismThemes.nightOwl,
         additionalLanguages: ['bash', 'shell-session'],
       },
+      algolia: {
+        appId: 'Q93W1TPDIE',
+        apiKey: '8dc15a6ca0d7a01e9f7ab673468d63a1',
+        indexName: 'caesarverifier',
+      }
     }),
 };
 

website/src/css/custom.css

@@ -41,15 +41,15 @@
 }
 
 /* Link decorations */
-p a, .markdown ul a {
+.markdown p a, .markdown ul a {
   --ifm-link-decoration: underline;
 }
 
-p a:hover, .markdown ul a:hover {
+.markdown p a:hover, .markdown ul a:hover {
   text-decoration: none;
 }
 
-a.button {
+.markdown a.button {
   text-decoration: none;
 }