backport #380 (#381)

Author: khieta

.github/workflows/run_integration_tests_reusable.yml

@@ -49,9 +49,8 @@ jobs:
       - name: Prepare Rust build
         run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
       - name: Build Lean libraries
-        working-directory: ./cedar-spec
-        shell: bash
-        run: source ~/.profile && ./build.sh
+        working-directory: ./cedar-spec/cedar-lean
+        run: source ~/.profile && ../cedar-drt/build_lean_lib.sh
       - name: Run integration tests
         working-directory: ./cedar-spec/cedar-drt
         shell: bash

README.md

@@ -14,8 +14,9 @@ This repository contains the formalization of Cedar and infrastructure for perfo
 To build the Lean formalization and proofs:
 
 * Install Lean, following the instructions [here](https://leanprover.github.io/lean4/doc/setup.html).
-* `source cedar-drt/set_env_vars.sh`
-* `cd cedar-lean && lake build Cedar`
+* `cd cedar-lean`
+* `source ../cedar-drt/set_env_vars.sh` (only required if running on AL2)
+* `lake build Cedar`
 
 To build the DRT framework: