Add script to automate build & running kani #78
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -9,7 +9,7 @@ on: | |
| paths: | ||
| - 'library/**' | ||
| - '.github/workflows/kani.yml' | ||
| - 'scripts/run-kani.sh' | ||
|
|
||
| defaults: | ||
| run: | ||
|
|
@@ -35,4 +35,11 @@ jobs: | |
| submodules: true | ||
|
|
||
| - name: Run Kani Script | ||
|
There was a problem hiding this comment. Should this be named "Test Kani Script?" There was a problem hiding this comment. I think this first step is in fact checking the standard library with Kani, right? There was a problem hiding this comment. Yes, i shall separate the steps into test kani, following which I shall run kani on the standard library on the whole. |
||
| run: head/scripts/run-kani.sh --path ${{github.workspace}}/head | ||
|
|
||
| - name: Run Kani Script with --kani-args and -p | ||
| run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut | ||
|
There was a problem hiding this comment. I would suggest that you change the arguments to be something that doesn't depend on the harnesses configuration, or something very generic, like |
||
|
|
||
| - name: Run Kani Script without -p | ||
| working-directory: ${{github.workspace}}/head | ||
|
Comment on lines
+43
to
+44
There was a problem hiding this comment. Couldn't the testing of the script itself be done in a separate job? There was a problem hiding this comment. I'd initially put it in a separate job, but merged it all into one based on this comment #78 (comment) There was a problem hiding this comment. Hmm, but given it's testing the script itself, shouldn't we have a workflow that doest just the script testing, and that workflow should only execute when any of the files relating to the script (the script itself plus toml files perhaps) change? There was a problem hiding this comment. Just to clarify, I wasn't saying they had to be merged in the same job. It just wasn't clear to me what each workflow was doing. I would suggest that you test the script as a separate job of this workflow. But make it clear what each step is testing, so people are not confused. Maybe add some comments explaining what this is testing. |
||
| run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -19,7 +19,9 @@ Session.vim | |
| ## Build | ||
| /book/ | ||
| /build/ | ||
| /kani_build/ | ||
| /target | ||
| /library/target | ||
| *.rlib | ||
| *.rmeta | ||
| *.mir | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since you are changing this file. Can you please rename line 19 (build) or give the workflow a nice name? 😊