compare branches #3
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
) Multiple class filters must be passed in as a single argument. See: https://github.com/danielpalme/ReportGenerator#usage--command-line-parameters), but previously they were passed as multiple `-classfilters:` of which only the first was actually applied. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
…afny-lang#4212) This PR fixes dafny-lang#4139 I'm not sure of the fix right now, need to see if it works on other tests. I suspect it will fail and we might need another way to separate the TopLevelDecls order for verification as well. But let's see. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <rwillems@amazon.com>
…g#4207) This PR fixes dafny-lang#4205 I added the corresponding test. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Adds a compiler plugin to implement support for a class-level
`{:benchmarks}` attribute. See `DafnyBenchmarkingPlugin/README.md` for
details.
Since the existing plugin interface didn't support this use case, and
we'd like it to so other similar features like `{:test}` and coverage
instrumentation can also be plugins in the future, I also added a new
`CompilerInstrumenter` plugin interface similar to `Rewriter`.
The integration test for this plugin is also a negative test for
dafny-lang#1454, which will be fixed in
a separate pending PR.
<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---------
Co-authored-by: Remy Willems <rwillems@amazon.com>
Attempting verification directly from Dafny using `/typeEncoding:m` sometimes leads to invalid declaration errors in existing integration tests. The issue does not happen when printing to a Boogie file first, then verifying that file directly with Boogie. This PR tries to fix this. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
…ng#4282) This reverts commit cabd236. Fixes nightly build <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Redoes dafny-lang#4215, which had to be reverted. Weakens the test that caused trouble due to the non-determinism of benchmarking (see second commit). <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <rwillems@amazon.com>
### Changes
- All calls to `IServiceProvider.GetRequiredService<T>()` are now done
at startup, which prevents `ObjectDisposedException` and
`ContainerException` when tests are winding down, which would create
noise in our logs
Example of a noisy log line:
```
fail: Microsoft.Dafny.LanguageServer.Workspace.TelemetryPublisher[0]
exception occurred
DryIoc.ContainerException: code: Error.ContainerIsDisposed;
message: Container is disposed and should not be used: "container without scope has been DISPOSED!
You may include Dispose stack-trace into the message via:
container.With(rules => rules.WithCaptureContainerDisposeStackTrace())"
at DryIoc.Throw.It(Int32 error, Object arg0, Object arg1, Object arg2, Object arg3)
at DryIoc.Container.ThrowIfContainerDisposed()
at DryIoc.Container.ResolveAndCache(Int32 serviceTypeHash, Type serviceType, IfUnresolved ifUnresolved)
at DryIoc.Container.DryIoc.IResolver.Resolve(Type serviceType, IfUnresolved ifUnresolved)
at Microsoft.Extensions.DependencyInjection.ServiceProviderServiceExtensions.GetRequiredService(IServiceProvider provider, Type serviceType)
at Microsoft.Extensions.DependencyInjection.ServiceProviderServiceExtensions.GetRequiredService[T](IServiceProvider provider)
at Microsoft.Dafny.LanguageServer.Workspace.CompilationAfterTranslation..ctor(IServiceProvider services, CompilationAfterResolution compilationAfterResolution, IReadOnlyDictionary`2 diagnostics, IReadOnlyList`1 verificationTasks, List`1 counterexamples, Dictionary`2 implementationIdToView, VerificationTree verificationTree) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer/Workspace/Documents/CompilationAfterTranslation.cs:line 34
at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.PrepareVerificationTasksAsync(CompilationAfterResolution loaded, CancellationToken cancellationToken) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer/Workspace/CompilationManager.cs:line 163
at Microsoft.Dafny.LanguageServer.Workspace.CompilationManager.TranslateAsync() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyLanguageServer/Workspace/CompilationManager.cs:line 117
```
Taken from
https://github.com/dafny-lang/dafny/actions/runs/5541261307/jobs/10114441465?pr=3902
- `IFilesystem` has been removed as a field for classes where it wasn't
needed
- `VerificationProgressReporter` is now a service instead of an instance
that was created for every compilation, which matches better with its
name
### Testing
Since this a refactoring, no additional testing is needed.
<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
This PR fixes dafny-lang#4269 and fixes dafny-lang#4270 I first added unit tests for the cases that were failing. What really solved the issue was that I had to implement proper cloning for - methods, that were not keeping BodyStartTok - formals, that were not keeping RangeToken Then I also added for all formatting test a case when it tries to clone all members before formatting, like VSCode does, which unveiled 3 more formatting issues: ``` method Test() { g := new ClassName.ConstructorName( argument1b, // Two extra spaces argument2b, argument3b ); var g := new ClassName.ConstructorName( argument1, // Missing two extra spaces (when block mode activated) argument2, argument3 ); ... && unchanged( this, c ) && old( // Extra undesired space here c.c ) == c.c && fresh( c.c ) ``` I also solved the above issues by: * Ensuring the `RangeToken` of `TypeRHS` is preserved after cloning by modifying its topmost cloning parent `AssignmentRHS` * Ensure we iterate on pre resolved children to get `OwnedToken` (otherwise some cloned expressions were crashing) * Ensure `UnchangedExpr` is cloned with the same pattern as everyone else (otherwise the `RangeToken` wasn't kept) <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
…eeded (dafny-lang#4286) Reduces memory usage by closing more Z3 processes and creating fewer <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer
force-pushed
the
projectAwareIDE
branch
from
514bd47
to
15f8222
Compare
keyboardDrummer
force-pushed
the
projectAwareIDE
branch
from
15f8222
to
c5d1624
Compare
…mization (dafny-lang#4294) Fixes dafny-lang#1454. Uses the same technique as the C# runtime, the only wrinkle being finding the left-most node in order to call `newCopied(length)` on it. This allows us to actually assert success in the multithreaded benchmark for this case. This required being able to install the Java runtime to Maven local, so I've also applied the same changes @alex-chew had queued up for publishing this package. Also added support for a `{:benchmarkTearDown}` attribute in the plugin, for once-per-benchmark cleanup, statistics reporting, etc. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.