Skip to content

Commit

Permalink
Set options in IDE to more closely match CLI (dafny-lang#4374)
Browse files Browse the repository at this point in the history
This makes IDE and CLI resource counts more likely to match. In
particular, it makes it so that the Boogie file generated when running
the language server with the `--bprint` flag matches the Boogie file
generated when running the CLI with the `/print` Boogie flag, except for
some comments that don't seem to affect RU counts.

This does not, unfortunately, always make the RU counts presented in the
IDE match those given by the CLI. I'm not yet sure where the additional
discrepancy is coming from.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.
  • Loading branch information
atomb authored and keyboardDrummer committed Sep 15, 2023
1 parent e1ad567 commit 8de3395
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ public async Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(
cancellationToken.ThrowIfCancellationRequested();

var translated = await DafnyMain.LargeStackFactory.StartNew(() => Translator.Translate(program, errorReporter, new Translator.TranslatorFlags(errorReporter.Options) {
InsertChecksums = true,
InsertChecksums = 0 < engine.Options.VerifySnapshots,
ReportRanges = true
}).ToList(), cancellationToken);

Expand Down

0 comments on commit 8de3395

Please sign in to comment.