update doc-gen4 version (#430)

.github/workflows/ci.yml

@@ -30,18 +30,27 @@ jobs:
         run: |
               wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
               bash elan-init.sh -y
-      - name: Build
+      - name: Download dependencies
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake -R -Kenv=dev update
+      - name: Build proofs
         working-directory: ./cedar-lean
         shell: bash
         run: source ~/.profile && lake build Cedar
-      - name: Test
+      - name: Run unit tests
         working-directory: ./cedar-lean
         shell: bash
         run: source ~/.profile && lake exe CedarUnitTests
       - name: Test CLI
         working-directory: ./cedar-lean
         shell: bash
         run: source ~/.profile && ./test_cli.sh
+      - name: Build docs
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake -R -Kenv=dev build Cedar:docs
+
 
   build_and_test_drt:
     needs: get-branch-name

.github/workflows/deploy_docs.yml

@@ -34,14 +34,14 @@ jobs:
         run: |
               wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
               bash elan-init.sh -y
-      - name: Download doc-gen4
+      - name: Download dependencies
         working-directory: ./cedar-lean
         shell: bash
-        run: source ~/.profile && sed -i '/^meta if get_config? env = some "dev" then/d' lakefile.lean && lake update doc-gen4
+        run: source ~/.profile && lake -R -Kenv=dev update
       - name: Build docs
         working-directory: ./cedar-lean
         shell: bash
-        run: source ~/.profile && lake -Kenv=dev build Cedar:docs
+        run: source ~/.profile && lake -R -Kenv=dev build Cedar:docs
       - name: Move documentation to `docs/docs`
         run: |
               mkdir docs

README.md

@@ -22,6 +22,7 @@ See the README in each directory for more information.
 * Install Lean, following the instructions [here](https://leanprover.github.io/lean4/doc/setup.html).
 * `cd cedar-lean`
 * `source ../cedar-drt/set_env_vars.sh` (only required if running on AL2)
+* `lake update`
 * `lake build Cedar`
 
 ### DRT framework

cedar-drt/build_lean_lib.sh

@@ -14,4 +14,5 @@
 # limitations under the License.
 
 # Build command needed for linking Lean lib with Rust code
+lake update
 lake build Cedar:static DiffTest:static Batteries:static

cedar-lean/.gitignore

@@ -1,7 +1,6 @@
 .DS_Store
 /.lake/*
 *.json
-!lake-manifest.json
 *.olean
 lake-packages
 

cedar-lean/README.md

@@ -16,6 +16,7 @@ To build code and proofs from the command line:
 
 ```shell
 cd cedar-lean
+lake update
 lake build Cedar
 ```
 
@@ -34,14 +35,10 @@ lake exe Cli validate Cli/json-inputs/validate/example2a.json
 
 ## Updating the Lean toolchain
 
-Cedar depends on [`std4`](https://github.com/leanprover/std4), and it is configured to use the same version of Lean as `std4`.
-
-Follow these instructions to update to the latest version of `std4` and Lean:
+To change the version of Lean used, you will need to update two files:
 
-```shell
-curl https://raw.githubusercontent.com/leanprover/std4/main/lean-toolchain -o lean-toolchain
-lake update
-```
+* `lean-toolchain` controls the Lean version. You can find all available versions [here](https://github.com/leanprover/lean4/releases).
+* `lakefile.lean` lists the project dependencies. Make sure that `batteries` and `doc-gen4` are pinned to commits that match the Lean version.
 
 ## Contributing
 

cedar-lean/lakefile.lean

@@ -18,9 +18,9 @@ import Lake
 open Lake DSL
 
 meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "c7f4ac84b973b6efd8f24ba2b006cad1b32c9c53"
+require "leanprover" / "doc-gen4" @ git "v4.10.0"
 
-require "leanprover-community" / "batteries"
+require "leanprover-community" / "batteries" @ git "v4.10.0"
 
 package Cedar