Merge branch 'main' into stdlib

.github/workflows/build.yml

@@ -8,10 +8,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Install OCaml compiler
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: 4.11
           dune-cache: true

.github/workflows/changelog.yml

@@ -12,7 +12,7 @@ jobs:
     if: ${{ !contains(github.event.pull_request.labels.*.name, 'no-changelog-needed') }}
 
     steps:
-    - uses: actions/checkout@v1
+    - uses: actions/checkout@v4
 
     - name: git diff
       env:

.github/workflows/documentation.yml

@@ -14,10 +14,10 @@ jobs:
     if: github.event_name != 'push'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v1
-      - uses: actions/setup-node@v1
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v4
         with:
-          node-version: '16.14'
+          node-version: '20.18'
       - name: Test Build
         run: |
           cd docs/
@@ -33,11 +33,11 @@ jobs:
     if: github.event_name != 'pull_request'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v1
-      - uses: actions/setup-node@v1
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v4
         with:
           node-version: '16.14'
-      - uses: webfactory/ssh-agent@v0.5.0
+      - uses: webfactory/ssh-agent@v0.9.0
         with:
           ssh-private-key: ${{ secrets.GH_PAGES_DEPLOY }}
       - name: Deploy to GitHub Pages

.github/workflows/localdoc.yml

@@ -13,12 +13,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up node
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
-          node-version: '16.14'
+          node-version: '20.18'
 
       - name: Build documentation
         run: |
@@ -35,7 +35,7 @@ jobs:
           mv build ../documentation/gospel
 
       - name: Upload documentation artifact
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           path: documentation
           name: documentation

CHANGES.md

@@ -2,25 +2,27 @@
 
 ## Added
 
-- Add support for mutualy recursive ghost types
-  [#403] (https://github.com/ocaml-gospel/gospel/pull/403)
+- Add support for mutually recursive ghost types
+  [\#403](https://github.com/ocaml-gospel/gospel/pull/403)
 
 ## Improved
 
 - Rewrote the Gospel standard library to focus on the definition of
   mathematical objects.
   [\#423] (https://github.com/ocaml-gospel/gospel/pull/423)
+- Remove support for the record update syntax
+  [\#428](https://github.com/ocaml-gospel/gospel/pull/428)
 - Fix typing of expression with inlined record
-  [#420] (https://github.com/ocaml-gospel/gospel/pull/420)
+  [\#420](https://github.com/ocaml-gospel/gospel/pull/420)
 - Improve error message for unbound record fields
-  [#419] (https://github.com/ocaml-gospel/gospel/pull/419)
+  [\#419](https://github.com/ocaml-gospel/gospel/pull/419)
 - Collect all the missing fields in a record definition and don't accept
   incomplete record pattern syntax that OCaml consider incorrect
-  [#418] (https://github.com/ocaml-gospel/gospel/pull/418)
+  [\#418](https://github.com/ocaml-gospel/gospel/pull/418)
 - Display proper error message for a number of unsupported construction
-  [#406] (https://github.com/ocaml-gospel/gospel/pull/406)
+  [\#406](https://github.com/ocaml-gospel/gospel/pull/406)
 - Display an error message when encountering a Functor application
-  [#404] (https://github.com/ocaml-gospel/gospel/pull/404)
+  [\#404](https://github.com/ocaml-gospel/gospel/pull/404)
 - Changed the gospel typechecker to use bool as the type of logical formulae
   [\#391](https://github.com/ocaml-gospel/gospel/pull/391)
 
@@ -30,7 +32,7 @@
 
 - Created a gallery of Gospel examples that might serve as a working ground
   to experiment with Gospel syntax and future extensions of the language.
-  [#361] (https://github.com/ocaml-gospel/gospel/pull/361)
+  [\#361](https://github.com/ocaml-gospel/gospel/pull/361)
 
 ## Improved
 
@@ -126,7 +128,7 @@
 ## Fixed
 
 - Fix the performance issues in the preprocessor
-  [\353](https://github/ocaml-gospel/gospel/pull/353)
+  [\#353](https://github/ocaml-gospel/gospel/pull/353)
 - Gospel preprocessor support documentation for ghost declaration
   [\#331](https://github/ocaml-gospel/gospel/pull/331)
 - Consider comments as spaces while preprocessing (to ensure specification can

docs/docs/language/expressions.md

@@ -4,10 +4,6 @@ sidebar_position: 3
 
 # Expressions
 
-Gospel expression can be either a term (e.g. `x+1`) or a formula (e.g.
-`forall i. i > 2 -> f i > 0`). This distinction is made during type checking,
-and not at the syntax level.
-
 The syntax for Gospel expressions is largely OCaml's syntax.
 The main differences are:
 

docs/package.json

@@ -27,6 +27,7 @@
     "rehype-katex": "5",
     "remark-definition-list": "^1.2.0",
     "remark-math": "3",
+    "to-fast-properties": "^4.0.0",
     "url-loader": "^4.1.1"
   },
   "browserslist": {