Codebase Improvements

This page collects possible improvements to the Dafny VSCode codebase and current shortcomings.

Note: for new Features, please got to the Feature Wishlist.

General

• Smart verify queueing on file changes
• Handling of larger workspaces and cross-file references (also see #18)
  • When multiple files are involved, the underlining many times appear in the wrong file.
  • 0 references is no useful information.
• Support for single files outside of workspaces (also see #5)
• Configuration hot reloading (#43)
• Status bar (also see #15)
• Improve VSCode error handling
• Clean up unused files

Client (VSCode Editor Window)

• Dafny Runner is currently not safe for paths with some special characters
• It would be great to try to find a way to make the green squigglies less prominent.

VSCode Language Server

• Rewrite Symbol Server / Table
• Much string/regex parsing to find positions in code (also used for refactorings)
• Process management of dafny verifier (also see #25, #15)
• Clean Interface and Parsing of dafny verifier output (currently distributed in multiple files; possibly also see #46)
• Handle Dafny Version Management better #29

Tests

(See CI Tipps for Azure DevOps)

• Unit (Currently none available)
  • TODO: Lots of server side features. Currently difficult due to high coupling.
• Integration (client ↔️ server)
  • Test simple verification call
  • Test counter model call with errors
  • Test counter model call without errors
  • ...
• e2e tests (vscode integration)
  • Language Detection, and Backend Startup test.
  • Check that errors are reported / highlighted
  • Check that counter model data is displayed
  • Editing / Queueing
  • References
  • Compile
  • Compile & Run
  • Dafny install / uninstall / (server restart)