Skip to content

Make DRT compatible to arbitrary 1.4 #1128

Make DRT compatible to arbitrary 1.4

Make DRT compatible to arbitrary 1.4 #1128

Workflow file for this run

name: Build and Test cedar-spec
on:
pull_request:
jobs:
get-branch-name:
runs-on: ubuntu-latest
steps:
- name: Get branch name
shell: bash
# The workflow is triggered by pull_request so we use `GITHUB_BASE_REF`
run: echo "branch_name=${GITHUB_BASE_REF}" >> $GITHUB_OUTPUT
id: get_branch_name
outputs:
branch_name: ${{ steps.get_branch_name.outputs.branch_name }}
build_and_test_lean:
name: Build and test Lean
runs-on: ubuntu-latest
strategy:
matrix:
toolchain:
- stable
steps:
- name: Checkout cedar-spec
uses: actions/checkout@v4
- name: Install Lean
shell: bash
run: |
wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
bash elan-init.sh -y
- 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: Lint for uncheckd theorems
working-directory: ./cedar-lean
shell: bash
run: source ~/.profile && lake lint
- 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
uses: ./.github/workflows/build_and_test_drt_reusable.yml
with:
cedar_spec_ref: ${{ github.ref }}
cedar_policy_ref: ${{ needs.get-branch-name.outputs.branch_name }}
test_docker_build:
name: Test Docker build
runs-on: ubuntu-latest
steps:
- name: Set up Docker Buildx
uses: docker/setup-buildx-action@v3
- name: Build Docker image
uses: docker/build-push-action@v5
with:
push: false
tags: cedar-drt:latest
run-integration-tests:
needs: get-branch-name
uses: ./.github/workflows/run_integration_tests_reusable.yml
with:
cedar_spec_ref: ${{ github.ref }}
cedar_policy_ref: ${{ needs.get-branch-name.outputs.branch_name }}
cedar_integration_tests_ref: ${{ needs.get-branch-name.outputs.branch_name }}