[Test Generation] Deprecate support for old command line interface #4385
Conversation
| dafnyOptions.CompilerName = "cs"; | ||
| dafnyOptions.Compile = true; | ||
| dafnyOptions.RunAfterCompile = false; | ||
| dafnyOptions.ForceCompile = false; | ||
| dafnyOptions.DeprecationNoise = 0; | ||
| dafnyOptions.ForbidNondeterminism = true; | ||
| dafnyOptions.DefiniteAssignmentLevel = 2; | ||
| dafnyOptions.TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates; |
There was a problem hiding this comment.
I hope it's possible eventually to use the same encoding as verification does, but this seems fine for now.
There was a problem hiding this comment.
Yes, I will hope to revert this change. The one test failing on Windows with the arguments encoding is still a mystery to me as I wasn't able to reproduce it with Boogie alone... But I will try to dig deeper into that.
| public static readonly Option<bool> DisablePrune = new("--no-prune", | ||
| "Disable axiom pruning that Dafny uses to speed up verification.") { | ||
| public static readonly Option<bool> ForcePrune = new("--force-prune", | ||
| "Enable axiom pruning that Dafny uses to speed up verification. This may negatively affect the quality of tests.") { |
There was a problem hiding this comment.
Do you have a summary of why pruning negatively affects tests?
There was a problem hiding this comment.
It used to be the case that Boogie would not print the {:uses} attributes when saving an AST to file causing pruning to be way to aggressive if you then run Boogie on the same file. But I just discovered a recent PR to Boogie that might have fixed it. I will look into it and remove the --ForcePrune flag once the newer Boogie is merged if this is the case .
…afny-lang#4385) This PR deprecates support for old command line interface in test generation. Test generation hardcodes some non-standard command-line-options ("predicates" type encoding, enforced determinism, disabled axiom pruning), which is much more easier to enforce via the new command line interface. This also removes quite a bit of code and makes test generation easier to maintain. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]>
…4385) This PR deprecates support for old command line interface in test generation. Test generation hardcodes some non-standard command-line-options ("predicates" type encoding, enforced determinism, disabled axiom pruning), which is much more easier to enforce via the new command line interface. This also removes quite a bit of code and makes test generation easier to maintain. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]>
This PR deprecates support for old command line interface in test generation. Test generation hardcodes some non-standard command-line-options ("predicates" type encoding, enforced determinism, disabled axiom pruning), which is much more easier to enforce via the new command line interface. This also removes quite a bit of code and makes test generation easier to maintain.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.