Merge pull request #1610 from moonbitlang/Yu-zh/fix-verification-test #7226
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
| # moon: The build system and package manager for MoonBit. | |
| # Copyright (C) 2024 International Digital Economy Academy | |
| # | |
| # This program is free software: you can redistribute it and/or modify | |
| # it under the terms of the GNU Affero General Public License as published by | |
| # the Free Software Foundation, either version 3 of the License, or | |
| # (at your option) any later version. | |
| # | |
| # This program is distributed in the hope that it will be useful, | |
| # but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| # GNU Affero General Public License for more details. | |
| # | |
| # You should have received a copy of the GNU Affero General Public License | |
| # along with this program. If not, see <https://www.gnu.org/licenses/>. | |
| # | |
| # For inquiries, you can contact us via e-mail at jichuruanjian@idea.edu.cn. | |
| name: CI | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| branches: | |
| - main | |
| schedule: | |
| - cron: '0 20 * * *' | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| CARGO_TERM_COLOR: always | |
| RUST_BACKTRACE: 0 | |
| CARGO_TARPAULIN_VERSION: 0.30.0 | |
| jobs: | |
| CCAA-check: | |
| runs-on: ubuntu-latest | |
| if: github.event_name == 'pull_request' | |
| outputs: | |
| CCAA-signed: ${{ steps.CCAA-check-step.outputs.CCAA-signed }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: CCAA check | |
| id: CCAA-check-step | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| run: | | |
| PR_AUTHOR=$(curl -s -H "Authorization: token $GITHUB_TOKEN" \ | |
| https://api.github.com/repos/${{ github.repository }}/pulls/${{ github.event.number }} \ | |
| | jq -r '.user.login') | |
| echo "The PR author is $PR_AUTHOR" | |
| # Allow GitHub Copilot bot to bypass CLA check | |
| if [ "$PR_AUTHOR" = "Copilot" ]; then | |
| echo "GitHub Copilot bot detected. Skipping CCAA check." | |
| echo "CCAA-signed=true" >> $GITHUB_ENV | |
| exit 0 | |
| fi | |
| EMAIL=$(git log -1 --pretty=format:'%ae') | |
| echo "Commit author email: $EMAIL" | |
| CCAA_RESPONSE=$(curl -s "https://mooncakes.io/api/v0/cla/check_with_repo?gh_username=$PR_AUTHOR&repo=moon&email=$EMAIL") | |
| echo "CCAA check response: $CCAA_RESPONSE" | |
| SIGNED=$(echo $CCAA_RESPONSE | jq -r '.signed') | |
| echo "CCAA-signed=$SIGNED" >> $GITHUB_ENV | |
| echo "If you have any questions about the CCAA result, please contact us." | |
| if [ "$SIGNED" != "true" ]; then | |
| echo "CCAA is not signed. Please read the document at https://github.com/moonbitlang/moon/tree/main/docs/dev" | |
| exit 1 | |
| else | |
| echo "CCAA is signed." | |
| fi | |
| license-header-check: | |
| name: license header check | |
| runs-on: ubuntu-latest | |
| env: | |
| HAWKEYE_VERSION: v5.6.0 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Download HawkEye | |
| run: curl --proto '=https' --tlsv1.2 -LsSf https://github.com/korandoru/hawkeye/releases/download/$HAWKEYE_VERSION/hawkeye-installer.sh | sh | |
| - name: License Header Check | |
| run: hawkeye check | |
| typo-check: | |
| name: typo-check | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| env: | |
| FORCE_COLOR: 1 | |
| TYPOS_VERSION: v1.18.0 | |
| steps: | |
| - name: download typos | |
| run: curl -LsSf https://github.com/crate-ci/typos/releases/download/$TYPOS_VERSION/typos-$TYPOS_VERSION-x86_64-unknown-linux-musl.tar.gz | tar zxf - -C ${CARGO_HOME:-~/.cargo}/bin | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| - name: check for typos | |
| run: typos | |
| mdbook-check: | |
| name: mdBook Check | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| - name: Setup mdBook | |
| uses: peaceiris/actions-mdbook@v2 | |
| with: | |
| mdbook-version: 'latest' | |
| - name: Build and Check mdBook | |
| run: | | |
| mdbook build docs/manual | |
| mdbook build docs/manual-zh | |
| nightly-test: | |
| needs: [typo-check, license-header-check] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: | |
| - ubuntu-latest | |
| - macos-latest | |
| - windows-latest | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Configure git | |
| run: git config --global core.autocrlf false | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - uses: dtolnay/rust-toolchain@1.90.0 | |
| with: | |
| components: rustfmt, clippy | |
| - name: Cargo cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: install MoonBit(Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: | | |
| curl -fsSL https://cli.moonbitlang.com/install/unix.sh | bash -s nightly | |
| echo "$HOME/.moon/bin" >> $GITHUB_PATH | |
| echo "$GITHUB_WORKSPACE/target/debug" >> $GITHUB_PATH | |
| - name: install MoonBit(Windows) | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| run: | | |
| $env:MOONBIT_INSTALL_VERSION="nightly" | |
| Set-ExecutionPolicy RemoteSigned -Scope CurrentUser; irm https://cli.moonbitlang.com/install/powershell.ps1 | iex | |
| "$env:USERPROFILE\.moon\bin" | Out-File -FilePath $env:GITHUB_PATH -Append | |
| "$env:GITHUB_WORKSPACE\target\debug" | Out-File -FilePath $env:GITHUB_PATH -Append | |
| - name: Setup MSVC | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| uses: ilammy/msvc-dev-cmd@v1 | |
| - name: Build | |
| run: cargo build | |
| - name: Set built binary to PATH (Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: echo "$GITHUB_WORKSPACE/target/debug" >> $GITHUB_PATH | |
| - name: Set built binary to PATH (Windows) | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| run: Add-Content $env:GITHUB_PATH "$env:GITHUB_WORKSPACE\target\debug" | |
| - name: Versions | |
| run: cargo run --bin moon -- version --all | |
| - name: Bundle core (Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: cargo run --bin moon -- -C ~/.moon/lib/core bundle --all | |
| - name: Bundle core (Windows) | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| run: cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" bundle --all | |
| - name: moon update | |
| run: | | |
| cargo run --bin moon -- update | |
| - name: Build xtask | |
| run: cargo build -p xtask | |
| - name: Run tests | |
| run: cargo test | |
| - name: Auxiliary checks | |
| if: matrix.os == 'ubuntu-latest' | |
| run: cargo xtask ci | |
| - name: Test core (Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: | | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target wasm-gc | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target js | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target wasm | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target native | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target wasm-gc | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target js | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target wasm | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target native | |
| # LLVM is currently disabled because it doesn't exist on non-bleeding channels. | |
| # TODO: Add this back when we add LLVM to nightly | |
| # - name: Test core on llvm backend (Unix) | |
| # if: ${{ (matrix.os != 'windows-latest') }} | |
| # run: | | |
| # cargo run --bin moon -- -C ~/.moon/lib/core test --target llvm | |
| # cargo run --bin moon -- -C ~/.moon/lib/core test --target llvm --release | |
| nightly-test-core-windows: | |
| needs: [typo-check, license-header-check] | |
| runs-on: windows-latest | |
| steps: | |
| - name: Configure git | |
| run: git config --global core.autocrlf false | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - uses: dtolnay/rust-toolchain@1.90.0 | |
| with: | |
| components: rustfmt, clippy | |
| - name: Cargo cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: install MoonBit(Windows) | |
| run: | | |
| $env:MOONBIT_INSTALL_VERSION="nightly" | |
| Set-ExecutionPolicy RemoteSigned -Scope CurrentUser; irm https://cli.moonbitlang.com/install/powershell.ps1 | iex | |
| "$env:USERPROFILE\.moon\bin" | Out-File -FilePath $env:GITHUB_PATH -Append | |
| "$env:GITHUB_WORKSPACE\target\debug" | Out-File -FilePath $env:GITHUB_PATH -Append | |
| - name: Setup MSVC | |
| uses: ilammy/msvc-dev-cmd@v1 | |
| - name: Build | |
| run: cargo build | |
| - name: Set built binary to PATH (Windows) | |
| run: Add-Content $env:GITHUB_PATH "$env:GITHUB_WORKSPACE\target\debug" | |
| - name: Versions | |
| run: cargo run --bin moon -- version --all | |
| - name: Bundle core (Windows) | |
| run: cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" bundle --all | |
| - name: Test core (Windows) | |
| run: | | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target wasm-gc | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target js | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target wasm | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target native | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target wasm-gc | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target js | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target wasm | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target native | |
| # LLVM is currently disabled because it doesn't exist on non-bleeding channels. | |
| # TODO: Add this back when we add LLVM to nightly | |
| # - name: Test core on llvm backend (Windows) | |
| # run: | | |
| # cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target llvm | |
| # cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target llvm --release | |
| verification-test: | |
| needs: [typo-check, license-header-check] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: | |
| - ubuntu-latest | |
| - macos-latest | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Configure git | |
| run: git config --global core.autocrlf false | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - uses: dtolnay/rust-toolchain@1.90.0 | |
| with: | |
| components: rustfmt, clippy | |
| - name: Cargo cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: Setup opam | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: 4.14.2 | |
| - name: install MoonBit | |
| run: | | |
| curl -fsSL https://cli.moonbitlang.com/install/unix.sh | bash -s nightly | |
| echo "$HOME/.moon/bin" >> $GITHUB_PATH | |
| - name: Install verification dependencies (Ubuntu) | |
| if: ${{ matrix.os == 'ubuntu-latest' }} | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y z3 | |
| echo "Z3PATH=$(command -v z3)" >> $GITHUB_ENV | |
| - name: Install verification dependencies (macOS) | |
| if: ${{ matrix.os == 'macos-latest' }} | |
| run: | | |
| brew install z3 | |
| echo "Z3PATH=$(command -v z3)" >> $GITHUB_ENV | |
| - name: Install Why3 1.7.2 via opam | |
| run: | | |
| opam install -y why3.1.7.2 | |
| echo "WHY3DATA=$(opam exec -- why3 --print-datadir)" >> $GITHUB_ENV | |
| echo "WHY3LIB=$(opam exec -- why3 --print-libdir)" >> $GITHUB_ENV | |
| - name: Build | |
| run: cargo build | |
| - name: Set built binary to PATH | |
| run: echo "$GITHUB_WORKSPACE/target/debug" >> $GITHUB_PATH | |
| - name: Versions | |
| run: cargo run --bin moon -- version --all | |
| - name: Bundle core | |
| run: cargo run --bin moon -- -C ~/.moon/lib/core bundle --all | |
| - name: Run verification tests | |
| env: | |
| VERIFICATION_TESTS: 1 | |
| Z3PATH: ${{ env.Z3PATH }} | |
| WHY3DATA: ${{ env.WHY3DATA }} | |
| WHY3LIB: ${{ env.WHY3LIB }} | |
| run: opam exec -- cargo test -p moon moon_prove -- --nocapture | |
| stable-test: | |
| needs: [typo-check, license-header-check] | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: | |
| - ubuntu-latest | |
| - macos-latest | |
| - windows-latest | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Configure git | |
| run: git config --global core.autocrlf false | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: true | |
| - uses: dtolnay/rust-toolchain@1.90.0 | |
| with: | |
| components: rustfmt, clippy | |
| - name: Cargo cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: install MoonBit(Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: | | |
| curl -fsSL https://cli.moonbitlang.com/install/unix.sh | bash | |
| echo "$HOME/.moon/bin" >> $GITHUB_PATH | |
| - name: install MoonBit(Windows) | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| run: | | |
| Set-ExecutionPolicy RemoteSigned -Scope CurrentUser; irm https://cli.moonbitlang.com/install/powershell.ps1 | iex | |
| "C:\Users\runneradmin\.moon\bin" | Out-File -FilePath $env:GITHUB_PATH -Append | |
| - name: Setup MSVC | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| uses: ilammy/msvc-dev-cmd@v1 | |
| - name: Build | |
| run: cargo build | |
| - name: Set built binary to PATH (Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: echo "$GITHUB_WORKSPACE/target/debug" >> $GITHUB_PATH | |
| - name: Set built binary to PATH (Windows) | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| run: Add-Content $env:GITHUB_PATH "$env:GITHUB_WORKSPACE\target\debug" | |
| - name: Versions | |
| run: cargo run --bin moon -- version --all | |
| - name: Bundle core (Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: cargo run --bin moon -- -C ~/.moon/lib/core bundle --all | |
| - name: Bundle core (Windows) | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| run: cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" bundle --all | |
| - name: moon update | |
| run: | | |
| cargo run --bin moon -- update | |
| - name: Build xtask | |
| run: cargo build -p xtask | |
| - name: Run tests | |
| run: cargo test | |
| - name: Auxiliary checks | |
| if: matrix.os == 'ubuntu-latest' | |
| run: cargo xtask ci | |
| - name: Test core (Unix) | |
| if: ${{ matrix.os != 'windows-latest' }} | |
| run: | | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target wasm-gc | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target js | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target wasm | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --target native | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target wasm-gc | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target js | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target wasm | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --release --target native | |
| cargo run --bin moon -- -C ~/.moon/lib/core test --doc | |
| - name: Test core (Windows) | |
| if: ${{ matrix.os == 'windows-latest' }} | |
| run: | | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target wasm-gc | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target js | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target wasm | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --target native | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target wasm-gc | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target js | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target wasm | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --release --target native | |
| cargo run --bin moon -- -C "$env:USERPROFILE\.moon\lib\core" test --doc | |
| # coverage: | |
| # needs: bleeding-test | |
| # runs-on: macos-latest | |
| # steps: | |
| # - name: Checkout repository | |
| # uses: actions/checkout@v4 | |
| # with: | |
| # submodules: true | |
| # - uses: dtolnay/rust-toolchain@1.90.0 | |
| # - name: Checkout moonc-version | |
| # uses: actions/checkout@v4 | |
| # with: | |
| # ref: moonc-version-dont-delete | |
| # path: moonc-version-dont-delete | |
| # - name: Copy moonc-version file to workspace | |
| # run: | | |
| # cp moonc-version-dont-delete/moonc-version . | |
| # - name: install MoonBit(Unix) | |
| # run: | | |
| # curl https://cli.moonbitlang.com/moon-ci/$(uname -s)-$(uname -m).tar.gz --output moonbit.tar.gz | |
| # mkdir -p ~/.moon/bin | |
| # mkdir -p ~/.moon/lib | |
| # tar xf moonbit.tar.gz --directory ~/.moon/ | |
| # curl https://cli.moonbitlang.com/moon-ci/$(uname -s)-$(uname -m)/moonrun --output ~/.moon/bin/moonrun | |
| # curl https://cli.moonbitlang.com/moon-ci/$(uname -s)-$(uname -m)/mooncake --output ~/.moon/bin/mooncake | |
| # chmod +x ~/.moon/bin/moon* | |
| # chmod +x ~/.moon/bin/internal/tcc | |
| # git clone --depth 1 https://github.com/moonbitlang/core.git ~/.moon/lib/core | |
| # echo "$HOME/.moon/bin" >> $GITHUB_PATH | |
| # echo "$GITHUB_WORKSPACE/target/debug" >> $GITHUB_PATH | |
| # - name: install cargo-tarpaulin ${{ env.CARGO_TARPAULIN_VERSION }} | |
| # run: | | |
| # cd "${CARGO_HOME}/bin" | |
| # curl -sL https://github.com/xd009642/tarpaulin/releases/download/${CARGO_TARPAULIN_VERSION}/cargo-tarpaulin-aarch64-apple-darwin.tar.gz | tar zxf - -C ${CARGO_HOME:-~/.cargo}/bin | |
| # - name: Build | |
| # run: cargo build | |
| # - name: Set built binary to PATH (Unix) | |
| # run: echo "$GITHUB_WORKSPACE/target/debug" >> $GITHUB_PATH | |
| # - name: Versions | |
| # run: cargo run --bin moon -- version --all | |
| # - name: Bundle core (Unix) | |
| # run: cargo run --bin moon -- -C ~/.moon/lib/core bundle --all | |
| # - name: Generate code coverage | |
| # run: cargo tarpaulin --ignore-tests --out Xml | |
| # - name: Upload coverage reports to Codecov | |
| # if: github.ref == 'refs/heads/main' | |
| # uses: codecov/codecov-action@v4.0.1 | |
| # with: | |
| # token: ${{secrets.CODECOV_TOKEN}} | |
| # fail_ci_if_error: true |