-
Notifications
You must be signed in to change notification settings - Fork 261
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 script to run Boogie with the args Dafny uses #4492
base: master
Are you sure you want to change the base?
Conversation
Also create a single source for these arguments, now used in all other cases of Boogie execution, and update the version of Boogie used as a dotnet tool. The list of arguments does still need to be manually updated when the set of options Dafny directly sets (without using the option parser) changes.
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.
Nice, this would have been so useful in my last PR. :)
One blocking easy fix, and some less blocking questions around rigor.
dotnet-tools.json
Outdated
@@ -15,10 +15,10 @@ | |||
] | |||
}, | |||
"boogie": { | |||
"version": "2.16.0", | |||
"version": "3.0.1", |
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.
(blocking) Should be 3.0.0 to match the actual dependency: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/DafnyCore.csproj#L35
Ideally we'd at least have a test that asserts they are the same somehow, if not an actual way of keeping them in sync automatically.
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.
Oh, oops. I was using 3.0.1 in my proof dependency PR and forgot it wasn't merged yet. :)
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.
I'll see if I can construct a test that compares the versions without too much effort.
Test/boogie-args.cfg
Outdated
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.
I think this deserves to be under Source
somewhere rather than hidden under Test
, since it's an alternate expression of how Dafny configures Boogie.
On that note, is there any way to assert that these are equivalent to what options Dafny actually sets through the library interface?
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.
I would really like to be able to guarantee that they're equivalent. I haven't thought of a good way to do it yet, but that doesn't mean there isn't one!
Until there is one, it feels weird to put it under Source
when nothing in that directory uses it, but stuff in Test
does.
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.
Does this fix issue 2800, or would a slight addition to this PR fix it?
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.
There's still some more work we'd need to do to ensure that's correct. We could add some code to copy the contents of this new file to the top of the generated Boogie file, but there's currently no guarantee that that would match what Dafny uses.
And add a check that the tool and library are always in sync
That way it can be tested locally.
I'm mystified as to why this is causing a failure to capture test coverage from the lit-style integration tests, but somehow it is. |
I think an alternative solution would be to print the equivalent Boogie CLI invocation at the top of Boogie files created by Secondly, could consider adding a hidden command to Dafny, |
In some ways I like that approach better, but it's also a lot more difficult. I think it would require traversing every one of the options available in Boogie and identifying which command-line option could lead to it. In some cases, it would be necessary to look at the relationship between multiple internal options to identify which command-line option could have produced that combination. It would be both time-consuming and error-prone to do at first, and would require diligent maintenance to ensure that it stayed up-to-date as options are changed or added. I'm not sure whether the tradeoff is worth it. Of course, if Boogie was using the CLI infrastructure you created for Dafny, it would be easy. :)
I imagine you mean that it would execute the CLI interface of the Boogie library, rather than a separate Boogie CLI process? That would be a nice approach in some ways, and would avoid the need for keeping the library and tool versions in sync. However, the main reason I typically find that I want to run Boogie on something produced by Dafny is to debug Boogie itself (and eventually produce a regression test that runs with standalone Boogie after fixing something). To do that, being able to run Boogie independently (which means using the CLI flags) is essential. |
I was thinking you would let Dafny insert a line into the .bpl file that says how you should run it, so the Boogie command line arguments are sourced from Dafny and the implementation complexity would be similar to what you have now.
It wouldn't be a separate process but it would behave as if you called the Boogie CLI directly.
I suggested |
Merge queue setting changed
Also create a single source for these arguments, now used in all other cases of Boogie execution, and update the version of Boogie used as a dotnet tool.
The list of arguments does still need to be manually updated when the set of options Dafny directly sets (without using the option parser) changes.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.