search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Updating the original files in libraries to Dafny 4. #91

Closed davidcok closed 1 year ago

davidcok commented 1 year ago

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

robin-aws commented 1 year ago

Nit: Mention in the PR body/commit message that you're also adding the autoformatter. I was about to ask if you got the PR title wrong because there are so few changes for Dafny 4.0 compatibility, I wasn't even sure that part was happening. :D

davidcok commented 1 year ago

Using lit made it very easy to setup and update the testing though.

robin-aws commented 1 year ago

Dismissed my earlier Request Changes as I'm okay with not testing in Dafny 4.0 mode for now, since it will be easier to do that once 4.0 is released. I still don't want the CI to be put in a broken state temporarily but I will let other reviewers help address that.

atomb commented 1 year ago

I think the current test failures may be due to changing the path to be verified from . to src, since that may have led to the test results being stored in a different directory. I think it makes sense to include the examples in verification, too, which would suggest leaving the target directory as ..

davidcok commented 1 year ago

Agree that the path should be ., not src. Thanks for spotting that.

atomb commented 1 year ago

Hmm. Still failing. If you run the lit command locally, do you get any .trx files generated?

davidcok commented 1 year ago

PR shifted to #97 for a continuing branch