diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml index ffd7d211f552e..38b128826e07d 100644 --- a/.github/workflows/book.yml +++ b/.github/workflows/book.yml @@ -11,9 +11,11 @@ on: pull_request: paths: - 'doc/**' + - '.github/workflows/book.yml' push: paths: - 'doc/**' + - '.github/workflows/book.yml' jobs: build: @@ -27,8 +29,9 @@ jobs: cargo install mdbook --version "^0.4" --locked echo "${HOME}/.cargo/bin" >> $GITHUB_PATH + # Removed --locked for now since it is broken due to old proc_macro feature. - name: Install linkchecker - run: cargo install mdbook-linkcheck --version "^0.7" --locked + run: cargo install mdbook-linkcheck --version "^0.7" - name: Build Documentation run: mdbook build doc diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml new file mode 100644 index 0000000000000..4b710bf900163 --- /dev/null +++ b/.github/workflows/kani.yml @@ -0,0 +1,52 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# This workflow is responsible for verifying the standard library with Kani. + +name: Kani +on: + workflow_dispatch: + pull_request: + paths: + - 'library/**' + - '.github/workflows/kani.yml' + push: + paths: + - 'library/**' + - '.github/workflows/kani.yml' + +defaults: + run: + shell: bash + +jobs: + build: + runs-on: ubuntu-latest + steps: + - name: Checkout Library + uses: actions/checkout@v4 + with: + path: verify-rust-std + submodules: true + + # We currently build Kani from a branch that tracks a rustc version compatible with this library version. + - name: Checkout `Kani` + uses: actions/checkout@v4 + with: + repository: model-checking/kani + path: kani + ref: features/verify-rust-std + + - name: Build `Kani` + working-directory: kani + run: | + cargo build-dev --release + echo "$(pwd)/scripts" >> $GITHUB_PATH + + - name: Run tests + working-directory: verify-rust-std + env: + RUST_BACKTRACE: 1 + run: | + kani verify-std -Z unstable-options ./library --target-dir "target" + diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml new file mode 100644 index 0000000000000..e943244a08d6e --- /dev/null +++ b/.github/workflows/rustc.yml @@ -0,0 +1,67 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# This workflow is responsible for building the standard library using the bootstrap script +# and executing the Rust regression. + +name: Rust Tests +on: + workflow_dispatch: + pull_request: + paths: + - 'library/**' + - 'rust-toolchain.toml' + - '.github/workflows/rustc.yml' + push: + paths: + - 'library/**' + - 'rust-toolchain.toml' + - '.github/workflows/rustc.yml' + +defaults: + run: + shell: bash + +jobs: + build: + runs-on: ${{ matrix.os }} + strategy: + matrix: + # Note windows-latest is currently failing. + os: [ubuntu-latest, macos-latest] + steps: + - name: Checkout Library + uses: actions/checkout@v4 + with: + path: head + submodules: true + + - name: Checkout `upstream/master` + uses: actions/checkout@v4 + with: + repository: rust-lang/rust + path: upstream + fetch-depth: 0 + submodules: true + + # Run rustc twice in case the toolchain needs to be installed. + # Retrieve the commit id from the `rustc --version`. Output looks like: + # `rustc 1.80.0-nightly (84b40fc90 2024-05-27)` + - name: Checkout matching commit + run: | + cd head + rustc --version + COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/") + cd ../upstream + git checkout ${COMMIT_ID} + + - name: Copy Library + run: | + rm -rf upstream/library + cp -r head/library upstream + + - name: Run tests + working-directory: upstream + run: | + ./configure --set=llvm.download-ci-llvm=true + ./x test --stage 0 library/std diff --git a/rust-toolchain.toml b/rust-toolchain.toml new file mode 100644 index 0000000000000..31b1f7dd8e678 --- /dev/null +++ b/rust-toolchain.toml @@ -0,0 +1,9 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# This version should be updated whenever we update the version of the Rust +# standard library we currently track. + +[toolchain] +channel = "nightly-2024-05-23" +components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]