cmake: enable debug in bundled LuaJIT #77
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: Proofs | |
| on: | |
| push: | |
| concurrency: | |
| # Update of a developer branch cancels the previously scheduled workflow | |
| # run for this branch. However, the 'main' branch and tag workflow runs | |
| # are never canceled. | |
| # | |
| # We use a trick here: define the concurrency group as 'workflow run ID' + | |
| # 'workflow run attempt' because it is a unique combination for any run. | |
| # So it effectively discards grouping. | |
| # | |
| # Important: we cannot use `github.sha` as a unique identifier because | |
| # pushing a tag may cancel a run that works on a branch push event. | |
| group: ${{ ( | |
| github.ref == 'refs/heads/main' || | |
| startsWith(github.ref, 'refs/tags/')) && | |
| format('{0}-{1}', github.run_id, github.run_attempt) || | |
| format('{0}-{1}', github.workflow, github.ref) }} | |
| cancel-in-progress: true | |
| jobs: | |
| cbmc: | |
| if: | | |
| github.event_name == 'push' || | |
| github.event_name == 'pull_request' && | |
| github.event.pull_request.head.repo.full_name != github.repository | |
| strategy: | |
| matrix: | |
| LUA: | |
| - "lua" | |
| fail-fast: false | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Setup common packages | |
| run: | | |
| sudo apt install -y cmake make cbmc | |
| - name: Running CMake (PUC Rio Lua -current) | |
| run: | | |
| cmake -DCMAKE_C_COMPILER=goto-cc -DENABLE_CBMC_PROOFS=ON \ | |
| -DUSE_LUA=ON -DCMAKE_BUILD_TYPE=Debug \ | |
| -S . -B build | |
| if: ${{ matrix.LUA == 'lua' }} | |
| - name: Building | |
| run: | | |
| cmake --build build --parallel $(nproc) --target build_cbmc_proofs |