Comments (1)
Indeed, when you have to wait long before resolution diagnostics have been computed, both clearing them after an edit until they've been recomputed, or not updating them until they've been recomputed, are not ideal.
If resolution emitted events more granularly, such as once per resolved module, then all the modules for which resolution hits the cache would immediately emit their event and we could send the resolution diagnostics that were unaffected by the change. That way, after an edit, only resolution diagnostics that might be affected by the edit would disappear, until resolution of those modules finishes again.
I'm removing the bug label since I consider improving this a feature. There's no documentation that describes what dafny server
should do with resolution diagnostics while it's computing new ones.
from dafny.
Related Issues (20)
- Unable to prove value of map.Values for simple maps
- Unable to prove simple assertion when implementing a trait with a datatype HOT 1
- Test generation cannot find witness for type nat HOT 1
- Test generation produces sequence with elements of wrong type
- Test generation violates preconditions
- Some verification iterations are successful, some fail? HOT 1
- Busy z3 process leaked
- transparent function == verified multiple times? HOT 1
- function transparency vs isolate-assertions vs split_here HOT 2
- Flaky test: ChangedImportAffectsExport
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
- Better path error reporting
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
- [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from dafny.