lean-update/.github/workflows/test.yaml at dev · argumentcomputer/lean-update · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
name: Other Tests

on:
  push:
    branches:
      - dev
  pull_request:
    types:
      - opened
      - synchronize
      - reopened
      - ready_for_review
      - converted_to_draft
      - edited
    branches:
      - dev
  workflow_dispatch:

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"
          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"
          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"
          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"
          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"
          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"