Update ci.yml (#144)

.github/workflows/ci.yml

@@ -101,3 +101,30 @@ jobs:
              source ./set_env_vars.sh
              export LD_LIBRARY_PATH=${LD_LIBRARY_PATH+$LD_LIBRARY_PATH:}$JAVA_HOME/lib/server
              cargo test --verbose
+
+  build_cedar_lean:
+    name: Build cedar-lean
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        toolchain:
+          - stable
+
+    steps:
+      - name: Checkout cedar-spec
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Install Lean
+        shell: bash
+        run: |
+              wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
+              bash elan-init.sh -y
+      - name: Build
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake build Cedar
+      - name: Test
+        working-directory: ./cedar-lean
+        shell: bash
+        run: source ~/.profile && lake exe CedarUnitTests

cedar-lean/UnitTest/Decimal.lean

@@ -61,4 +61,4 @@ def tests := [testsForValidStrings, testsForInvalidStrings]
 -- Uncomment for interactive debugging
 -- #eval TestSuite.runAll tests
 
-end UnitTest.Decimal
+end UnitTest.Decimal

cedar-lean/UnitTest/Main.lean

@@ -19,5 +19,5 @@ import UnitTest.IPAddr
 
 open UnitTest
 
-def main : IO Unit := do
+def main : IO UInt32 := do
   TestSuite.runAll (Decimal.tests ++ IPAddr.tests)

cedar-lean/UnitTest/Run.lean

@@ -71,12 +71,13 @@ def TestSuite.run (suite : TestSuite) : IO Nat := do
 /--
 Runs all the given test suites and prints the stats.
 -/
-def TestSuite.runAll (suites : List TestSuite) : IO Unit := do
+def TestSuite.runAll (suites : List TestSuite) : IO UInt32 := do
   let outcomes ← suites.mapM TestSuite.run
   let total := suites.foldl (fun n ts => n + ts.tests.length) 0
   let failures := outcomes.foldl (· + ·) 0
   let successes := total - failures
   IO.println "====== TOTAL ======="
   IO.println s!"{successes} success(es) {failures} failure(s) {total} test(s) run"
+  pure (UInt32.ofNat failures)
 
-end UnitTest
+end UnitTest