Go to Definition in IDE on standard library references produces error

[robin-aws]

Love that resolution/verification works after #4770! I got greedy and tried to Go to Definition on DafnyStdLibs.Wrappers and got "The editor could not be opened due to an unexpected error: Unable to resolve resource dllresource://dafnypipeline/DafnyStandardLibraries.doo"

The simplest fix is probably just to block opening .doo files in general and fail cleanly for now. I'd love to be able to browse the source code from the libraries eventually, but .doo files currently don't include any documentation/comments so we probably shouldn't enable it just yet.

[keyboardDrummer]

It's not just go to def that doesn't work properly, it's also diagnostics that link to .doo files that can't be opened. For example, if you do not satisfy a requires clause that's inside a .doo file, the diagnostics will give you a broken link to it.

[keyboardDrummer]

Seems like the VSCode extension should register a textDocumentContentProvider:

https://code.visualstudio.com/api/references/vscode-api#TextDocumentContentProvider

A text document content provider allows to add readonly documents to the editor, such as source from a dll or generated html from md.

Content providers are registered for a uri-scheme. When a uri with that scheme is to be loaded the content provider is asked.

[keyboardDrummer]

Another little IDE leak:

[keyboardDrummer]

The simplest fix is probably just to block opening .doo files in general and fail cleanly for now.

I'm not sure how to do that ! There's no single location where you can tell the Dafny server not to let any Uris that end in .doo be sent to the client. You would have to go through various APIs and filter out results based on Uris. Also, you can't tell the client not to open certain Uris.

From the client side, the best I have managed to get is:

---

To do better, one solution I can think of is to add another Dafny command, dafny get-source or some such, that can be passed a doo://<actualScheme>.<actualPath>, which returns the source of the doo file that the Uri points to, which also supports Uris like doo://dllresource.dafnypipeline/DafnyStandardLibraries.doo.

I'd like to implement this but I would like some +1's from others before I do that.

[jtristan]

@keyboardDrummer If I run dafny get-source, would I then be able to go to a definition and have proper diagnostics without broken links? If so, it is a +1 for me.

[keyboardDrummer]

@keyboardDrummer If I run dafny get-source, would I then be able to go to a definition and have proper diagnostics without broken links? If so, it is a +1 for me.

You wouldn't need to run anything, dafny get-source would be called by the Dafny VSCode extension to load the contents of Dafny files that don't directly exist on disk, and then yes nothing would be broken.

I would mark the get-source command as hidden since I'm not sure whether it's the right API.

[robin-aws]

To do better, one solution I can think of is to add another Dafny command, dafny get-source or some such, that can be passed a doo://., which returns the source of the doo file that the Uri points to, which also supports Uris like doo://dllresource.dafnypipeline/DafnyStandardLibraries.doo.

I'm not sure about this kind of thing since it really makes these URIs part of the API surface area, whereas up until now they have been internal detail (although they definitely leak occasionally, and more than I initially thought). Similarly if you use --input you might see a stdin:/// URI printed in error messages.

I honestly hadn't really intended to pull IDE support for the standard libraries into scope for 4.4. Would we be in a better state if we just reverted #4770 for now?

[robin-aws]

As per offline conversation, my preference would be:

1. Make the change to have a cleaner error message when the IDE tries to open a .doo file as in the screen shot above, before releasing. That makes the experience a little nicer and hides the dllresource://... URIs that are intended to be internal.
2. Implement dafny get-source later on, after also making some improvements to ensuring the source stored in a doo file is more usable (e.g. there are known issues here I need to log, such as losing all newlines in expressions, making them harder to read and even flagged with formatter warnings, and not preserving any comments)

[robin-aws]

More work to do to actually support reading doo file source in the IDE, but the release blocker is addressed by dafny-lang/ide-vscode#454