Exclude dir #22
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Other Tests | |
| on: | |
| push: | |
| branches: | |
| - dev | |
| pull_request: | |
| types: | |
| - opened | |
| - synchronize | |
| - reopened | |
| - ready_for_review | |
| - converted_to_draft | |
| - edited | |
| branches: | |
| - dev | |
| workflow_dispatch: | |
| # Every job asserts on the action's outputs inside the runner's own checkout and never | |
| # writes back, so a read-only token is all they need. | |
| permissions: | |
| contents: read | |
| jobs: | |
| has_dependency_output_test_true: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v6 | |
| - name: Update Lean package | |
| id: update | |
| uses: ./ | |
| with: | |
| on_update_succeeds: "silent" | |
| on_update_fails: "silent" | |
| lake_package_directory: "./Fixtures/HasDep" | |
| - name: The result should be success | |
| if: steps.update.outputs.has_dependency != 'true' | |
| run: exit 1 | |
| has_dependency_output_test_false: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v6 | |
| - name: Update Lean package | |
| id: update | |
| uses: ./ | |
| with: | |
| on_update_succeeds: "silent" | |
| on_update_fails: "silent" | |
| lake_package_directory: "./Fixtures/SmokeSuccess" | |
| - name: The result should be no dependency | |
| if: steps.update.outputs.has_dependency != 'false' | |
| run: exit 1 | |
| output_test: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v6 | |
| - name: Update Lean package | |
| id: update | |
| uses: ./ | |
| with: | |
| on_update_succeeds: "silent" | |
| on_update_fails: "silent" | |
| lake_package_directory: "./Fixtures/SmokeSuccess" | |
| - name: output assertion of latest_lean | |
| run: | | |
| echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}" | |
| if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^v ]]; then | |
| echo "Error: The latest_lean output should start with 'v'" | |
| exit 1 | |
| fi | |
| echo "latest_lean output test passed" | |
| - name: output assertion of notify | |
| run: | | |
| echo "Notify status: ${{ steps.update.outputs.notify }}" | |
| if [[ "${{ steps.update.outputs.notify }}" != "true" ]]; then | |
| echo "Error: The notify output should be 'true' for this test case" | |
| echo "This test should have updates available with a successful build" | |
| exit 1 | |
| fi | |
| echo "notify output test passed" | |
| latest_lean_output_test_with_dependencies: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v6 | |
| - name: Update Lean package | |
| id: update | |
| uses: ./ | |
| with: | |
| on_update_succeeds: "silent" | |
| on_update_fails: "silent" | |
| lake_package_directory: "./Fixtures/HasDep" | |
| - name: output assertion of latest_lean | |
| run: | | |
| echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}" | |
| if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^v ]]; then | |
| echo "Error: The latest_lean output should start with 'v' even when dependencies are present" | |
| exit 1 | |
| fi | |
| echo "latest_lean output test with dependencies passed" | |
| latest_lean_output_test_with_update_lean_toolchain_never: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v6 | |
| - name: Record original lean-toolchain | |
| id: original-toolchain | |
| run: echo "content=$(cat Fixtures/SmokeSuccess/lean-toolchain)" >> "$GITHUB_OUTPUT" | |
| - name: Update Lean package | |
| id: update | |
| uses: ./ | |
| with: | |
| on_update_succeeds: "silent" | |
| on_update_fails: "silent" | |
| lake_package_directory: "./Fixtures/SmokeSuccess" | |
| update_lean_toolchain: "never" | |
| - name: output assertion of latest_lean | |
| run: | | |
| echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}" | |
| if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^v ]]; then | |
| echo "Error: The latest_lean output should start with 'v' even when update_lean_toolchain is never" | |
| exit 1 | |
| fi | |
| echo "latest_lean output test with update_lean_toolchain=never passed" | |
| - name: lean-toolchain should not be updated | |
| run: | | |
| CURRENT_TOOLCHAIN=$(cat Fixtures/SmokeSuccess/lean-toolchain) | |
| ORIGINAL_TOOLCHAIN="${{ steps.original-toolchain.outputs.content }}" | |
| echo "Original lean-toolchain: $ORIGINAL_TOOLCHAIN" | |
| echo "Current lean-toolchain: $CURRENT_TOOLCHAIN" | |
| if [[ "$CURRENT_TOOLCHAIN" != "$ORIGINAL_TOOLCHAIN" ]]; then | |
| echo "Error: lean-toolchain should not be updated when update_lean_toolchain is never" | |
| exit 1 | |
| fi | |
| echo "lean-toolchain unchanged test passed" |