Add script to run Boogie with the args Dafny uses

[atomb]

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.

[robin-aws]

Nice, this would have been so useful in my last PR. :)

One blocking easy fix, and some less blocking questions around rigor.

[robin-aws]

(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.

[atomb]

Oh, oops. I was using 3.0.1 in my proof dependency PR and forgot it wasn't merged yet. :)

[atomb]

I'll see if I can construct a test that compares the versions without too much effort.

[robin-aws]

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?

[atomb]

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.

[davidcok]

Does this fix issue 2800, or would a slight addition to this PR fix it?

[atomb]

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.

[atomb]

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.

[keyboardDrummer]

I think an alternative solution would be to print the equivalent Boogie CLI invocation at the top of Boogie files created by
Dafny. It would also allow you to let Boogie automatically detect which arguments to use based on a directive found inside the .bpl file.

Secondly, could consider adding a hidden command to Dafny, dafny boogie, that redirects to the Boogie CLI of the Boogie version used by Dafny, so you might not need Scripts/compare_boogie_versions.sh

[atomb]

I think an alternative solution would be to print the equivalent Boogie CLI invocation at the top of Boogie files created by Dafny. It would also allow you to let Boogie automatically detect which arguments to use based on a directive found inside the .bpl file.

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. :)

Secondly, could consider adding a hidden command to Dafny, dafny boogie, that redirects to the Boogie CLI of the Boogie version used by Dafny, so you might not need Scripts/compare_boogie_versions.sh

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.

[keyboardDrummer]

I think an alternative solution would be to print the equivalent Boogie CLI invocation at the top of Boogie files created by Dafny. It would also allow you to let Boogie automatically detect which arguments to use based on a directive found inside the .bpl file.

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.

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.

I imagine you mean that it would execute the CLI interface of the Boogie library, rather than a separate Boogie CLI process?

It wouldn't be a separate process but it would behave as if you called the Boogie CLI directly.

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 suggested dafny boogie idea as an alternative for Scripts/compare_boogie_versions.sh, for the use-case of wanting to run something against the same version of Boogie as Dafny is using. If you want to run against Boogie HEAD, then I think you would not need either of those.