Updating the original files in libraries to Dafny 4 (#2) #97
Conversation
…an and now warned by dafny, because it is what makes the proof fail
| run: find . -name '*.csv' -print0 | xargs -0 --verbose dafny-reportgenerator summarize-csv-results --max-duration-seconds 10 | ||
|
|
||
| - uses: actions/upload-artifact@v2 # upload test results | ||
| if: success() || failure() # run this step even if previous step failed | ||
| if: always() && steps.withlog.conclusion != 'skipped' |
There was a problem hiding this comment.
What's the point of the extraneous always() &&?
There was a problem hiding this comment.
So that the step runs even if the previous steps fail
There was a problem hiding this comment.
Because if we (intentionally) run with an old version of dafny that does not support logging with new CLI (i.e. 3.11.0) then we don't want this step to run (and fail) if we have not produced any log files.
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| # nightly-latest to catch anything that breaks these tests in current development |
There was a problem hiding this comment.
Definitely happy with the solution of also using a specific nightly build to use the logging! But "nightly-latest" should only be used in the scheduled build, since otherwise the mainline CI can break spontaneously.
Here's how I set it up on the reportgenerator, which I intend to be the template for other projects: https://github.com/dafny-lang/dafny-reportgenerator/pull/17/files You should be able to do something similar, the only difference being that you have to make the matrix variable conditional instead, something like:
version: ${{ github.event_name == 'schedule' && ['nightly-latest'] || ['nightly-2023-02-18-ef4f346', '3.11.0'] }}There was a problem hiding this comment.
OK. But are you comfortable with that tweaking of the test scheduling after this PR is merged, so the changes to the script can be properly tested on master-branch files?
There was a problem hiding this comment.
Sure, it's only going to be a maintenance pain for us if we don't fix it quickly. :)
There was a problem hiding this comment.
Put in the next PR. I learn new Github action syntax every day.
There was a problem hiding this comment.
Actually, this syntax does not work with lists -- tried numerous variations. So for now left out the nightly-latest from the CI build and made a separate nightly build. But this cries out for a reusable workflow that I'll figure out later.
README-TESTING.md
Outdated
| macros `%verify` and `%run` and the like. | ||
|
|
||
| The versions of dafny being run are set in the `tests.yml` file. The versions tested | ||
| must be recent enough to support the new CLI syntax, so 3.11ff. Also, if |
There was a problem hiding this comment.
Odd. Its OK in the Files view. I'll check the rendering again after pushing these changes.
README-TESTING.md
Outdated
| The latter is important for those cases (e.g. FileIO) where the implementations | ||
| are custom external code for each target programming language. | ||
| Runtime tests are also a check that dafny compiled the (verified) dafny code correctly. |
There was a problem hiding this comment.
(minor) I'd be slightly happier reversing the order of these two motivations, just because all Dafny code needs tests because of the second reason, whereas the first is just emphasizing the code most likely to be among the riskiest inside the trusted computing base.
There was a problem hiding this comment.
There's also the reason of making sure we watch out for any code that isn't currently supported for all compilation targets (but we can leave that for now in this PR, since we're not yet claiming anything about this)
There was a problem hiding this comment.
Switched the order.
Co-authored-by: Robin Salkeld <[email protected]>
There was a problem hiding this comment.
I think making the change to latest-nightly on another PR (soon) is reasonable, but I'd also like to hear whether @robin-aws has any concerns.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.