support non-compressed proofs in axiom_use.rs #595
This file contains 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: verify | |
| on: [push, pull_request, workflow_dispatch] | |
| # Verify software. | |
| jobs: | |
| # Skipping duplicate jobs doesn't work well with matrix (!!), | |
| # so we'll just do excess work. | |
| ########################################################### | |
| # skip_dups: | |
| # name: Check for duplicate jobs to avoid duplication | |
| # # continue-on-error: true # Uncomment once integration is finished | |
| # runs-on: ubuntu-latest | |
| # # Map a step output to a job output | |
| # outputs: | |
| # should_skip: ${{ steps.skip_check.outputs.should_skip }} | |
| # steps: | |
| # - id: skip_check | |
| # uses: fkirc/skip-duplicate-actions@master | |
| # with: | |
| # github_token: ${{ github.token }} | |
| # paths_ignore: '["**/README.md", "**/docs/**"]' | |
| ########################################################### | |
| test: | |
| name: Rebuild and test | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [ubuntu-20.04, ubuntu-latest, windows-latest, macOS-latest] | |
| rust: [stable] # [stable, nightly] | |
| # needs: skip_dups | |
| # if: ${{ needs.skip_dups.outputs.should_skip != 'true' }} | |
| steps: | |
| - uses: actions/checkout@v2 | |
| - name: Install rust | |
| uses: hecrj/setup-rust-action@v1 | |
| with: | |
| rust-version: ${{ matrix.rust }} | |
| components: clippy, rustfmt | |
| # TODO(David): Add more static tests, perhaps eventually fail on warnings | |
| # (or disable those warnings, preferably as specifically as we can). | |
| - name: Run tests | |
| run: cargo test --verbose | |
| - name: Clippy | |
| run: cargo clippy --all-targets --all-features -- -D warnings | |
| - name: Format | |
| run: cargo fmt -- --check | |
| - name: Docs | |
| run: cargo doc --lib --no-deps | |
| - name: Verify official set.mm | |
| run: | | |
| curl -s -G https://raw.githubusercontent.com/metamath/set.mm/develop/set.mm > set.mm | |
| cargo run -- --jobs 8 set.mm --verify --grammar --parse-stmt --verify-parse-stmt --verify-markup --parse-typesetting |