Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add scripts for local subtree update #46

Merged
merged 9 commits into from
Aug 12, 2024

Conversation

jaisnan
Copy link

@jaisnan jaisnan commented Jul 30, 2024

The CI job for subtree update timesout because it takes more than 6hrs. While we figure out how to solve that problem, this process makes sure there's an automated way for anyone to update the repo's subtree hosted library, with a one click script/command.

The structure of this process follows the (would-be) CI workflow closely i.e

  1. Call scripts/run_update_with_checks.sh
  2. This script in turn calls the other scripts in order
  3. Pull and update local subtree/library with updates from rust-lang
  4. Merge subtree/library onto local SYNC-{DATE} where {DATE} is the date tracked by Kani's features/verify-rust-std branch.
  5. Update toolchain to the date tracked by kani's features/verify-rust-std branch and commit.
  6. Test this branch with check_rustc which checks for compilation compatibility of the updated library and check_kani which checks that Kani's injected harnesses verify as expected.

Call-out

This currently only automates the process of updating the subtree and running all checks on it. After that, the process of issuing a PR from the SYNC-DATE branch of the local repo is still in the responsibility of the dev running the script.

There is ongoing work to automate the process of writing/pushing branches as well.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

jaisnan added 5 commits July 30, 2024 15:21
add pull_request just for testing

add push permission for testing

Test without updating subtree

Try within kani dir

Use kani as workdir

Change parsing

Parse regex with path

Check for toolchain file

Get toolchain date

Use correct hash and date

Use commit hash instead

make upstream pull explicit

Add origin for pulling

set working directory to head

Fix working directory

Update subtree

Add --quiet

Update with --quiet

Add pull_from_upstream.sh

Add scripts -1

Add explicit commit pull

Add temp home dir

Add clone from temp

Add base repo

Update comments

clone into tempdir

Add working tests
@jaisnan jaisnan requested a review from a team as a code owner July 30, 2024 15:31
Copy link

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's great! Thanks @jaisnan

I think we should update our CI to use check_kani.sh and check_rustc.sh scripts, so we don't have 2 different sources of truth.

@jaisnan
Copy link
Author

jaisnan commented Jul 30, 2024

That's great! Thanks @jaisnan

I think we should update our CI to use check_kani.sh and check_rustc.sh scripts, so we don't have 2 different sources of truth.

Let me update this PR itself with that change.
Edit: Done!

jaisnan added 3 commits July 31, 2024 01:10
Test with github workspace

Try with bash

Run ls

Try with path expanded

Fix path to script

Fix path to library

Fix script

Check with verify-rst-std

Check workflow

Check path

Fix path

change path to head
@jaisnan jaisnan merged commit ec6d98e into model-checking:main Aug 12, 2024
8 checks passed
szlee118 pushed a commit to stogaru/verify-rust-std that referenced this pull request Oct 17, 2024
The CI job for subtree update timesout because it takes more than 6hrs.
While we figure out how to solve that problem, this process makes sure
there's an automated way for anyone to update the repo's subtree hosted
library, with a one click script/command.

The structure of this process follows the (would-be) CI workflow closely
i.e

1. Call `scripts/run_update_with_checks.sh` 
2. This script in turn calls the other scripts in order
3. Pull and update local `subtree/library` with updates from
[rust-lang](https://github.com/rust-lang/rust)
4. Merge `subtree/library` onto local `SYNC-{DATE}` where {DATE} is the
date tracked by Kani's `features/verify-rust-std` branch.
5. Update toolchain to the date tracked by kani's
`features/verify-rust-std` branch and commit.
6. Test this branch with `check_rustc` which checks for compilation
compatibility of the updated library and `check_kani` which checks that
Kani's injected harnesses verify as expected.

## Call-out

This currently only automates the process of updating the subtree and
running all checks on it. After that, the process of issuing a PR from
the SYNC-DATE branch of the local repo is still in the responsibility of
the dev running the script.

There is ongoing work to automate the process of writing/pushing
branches as well.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants