-
Notifications
You must be signed in to change notification settings - Fork 256
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?
Changes from 1 commit
363efe3
595a779
708035a
4673b2a
2cf5cae
9881e38
5ffb627
05b00e2
2fb6f87
035767a
08520f8
46c9355
575e8f1
f986ba0
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
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.
- Loading branch information
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
#!/bin/bash | ||
ROOT=$(dirname $(dirname "${BASH_SOURCE[0]}")) | ||
BOOGIE_ARGS=$(sed -e 's|^|-|' "${ROOT}"/Test/boogie-args.cfg | sed -e "s|{ROOT}|$ROOT|") | ||
dotnet tool run boogie $BOOGIE_ARGS "$@" |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
infer:j | ||
normalizeDeclarationOrder:1 | ||
normalizeNames:1 | ||
typeEncoding:a | ||
prune | ||
proverOpt:O:auto_config=false | ||
proverOpt:O:type_check=true | ||
proverOpt:O:smt.case_split=3 | ||
proverOpt:O:smt.qi.eager_threshold=100 | ||
proverOpt:O:smt.delay_units=true | ||
proverOpt:O:smt.arith.solver=2 | ||
proverOpt:PROVER_PATH:{ROOT}/Binaries/z3/bin/z3-4.12.1 |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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 commentThe 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 commentThe 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 commentThe 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. |
||
"commands": [ | ||
"boogie" | ||
] | ||
} | ||
} | ||
} | ||
} |
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 underTest
, 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 inTest
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.