Use `dafny:` Uris for standard library files #4832

keyboardDrummer · 2023-12-01T14:17:18Z

Description

For Dafny content that is embedded in the Dafny CLI, such as the standard library, expose their URIs using the dafny: scheme. This can be used by the LSP client to implement custom behavior for opening these files.

How has this been tested?

Added the test StandardLibraryTest.GotoDefinition

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

keyboardDrummer · 2023-12-01T15:26:27Z

Source/DafnyCore/DafnyFile.cs

@@ -23,6 +24,13 @@ public class DafnyFile {

  public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
    DafnyOptions options, Uri uri, IToken origin) {
+
+    if (uri.Scheme == "doo") {


VSCode only allows you to have custom handlers for custom schemes, which seems fair to me, but it means we have to introduce a doo: scheme, which is at odds with that we already handle the .doo extension as being special, even if no doo: scheme is used. That's why the code looks a bit funky now.

If we were more strict, only allowing doo files being used as libraries, and only allowing dfy files being used as sources, then we wouldn't need to rely on the extension checking, but that seems like something to consider for the future.

Yeah, this seems wrong enough to me to not do it at all - it really is abusing the URI scheme concept. It seems like letting VSCode understand the dllresource: scheme is part of the solution, but it also needs to understand that .doo is different content format independently.

Could we have a custom handler for dllresource: that says "if the URI ends with .doo ... else open like a normal Dafny file"? That would at least handle the standard libraries, even if we'll need to make more changes to handle doo files in general.

robin-aws · 2023-12-01T17:41:20Z

Source/DafnyCore/DafnyFile.cs

@@ -23,6 +24,13 @@ public class DafnyFile {

  public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fileSystem,
    DafnyOptions options, Uri uri, IToken origin) {
+
+    if (uri.Scheme == "doo") {


Yeah, this seems wrong enough to me to not do it at all - it really is abusing the URI scheme concept. It seems like letting VSCode understand the dllresource: scheme is part of the solution, but it also needs to understand that .doo is different content format independently.

…afny into differentUriForDooFile

robin-aws

Thanks for the change, I definitely like the dafny: version better. Just some questions.

robin-aws · 2023-12-05T16:38:25Z

Source/DafnyCore/DafnyFile.cs

@@ -16,13 +18,30 @@ public class DafnyFile {
  public string BaseName { get; private set; }
  public bool IsPreverified { get; set; }
  public bool IsPrecompiled { get; set; }
-  public bool IsPrerefined { get; private set; }


Off topic but when did this appear and what was it used for?

It was needed when .doo files still contained resolved code instead of just parsed code.

Okay good, I figured it was related but wasn't sure if was actually in sync before.

robin-aws · 2023-12-05T16:41:14Z

Source/DafnyCore/DooFile.cs

@@ -131,7 +130,7 @@ public class ManifestData {
    }

    var success = true;
-    var relevantOptions = currentCommand.Options.ToHashSet();
+    var relevantOptions = options.Options.OptionArguments.Keys.ToHashSet();


Is this still correct, given the comment immediately below? i.e. is OptionArguments.Keys the set of valid parameters for the current command, or just the options explicitly provided on the CLI or in project files?

This is still correct, yes

robin-aws · 2023-12-05T16:49:55Z

Source/DafnyCore/DafnyFile.cs

+  private static readonly Dictionary<Uri, Uri> ExternallyVisibleEmbeddedFiles = new();
+
+  public static Uri ExposeInternalUri(string externalName, Uri internalUri) {
+    var externalUri = new Uri("dafny:" + externalName);


Why not just use $"dafny:{internalUri}"? That would be simpler and leaves the door open for other schemes. AFAICT attaching a fake Dafny file name doesn't help the IDE but perhaps I'm missing something.

Because I didn't want to expose the implementation details of internalUri. Is there are a downside to having this mapping, except for it being slightly more work?

No real objection to the complexity/work, but a little worried about exposing "DafnyStandardLibraries.dfy" when that string/file name isn't actually meaningful. Eventually I expect the IDE will be able to actually open the doo file, and we shouldn't hide the fact that the source is coming from a doo file (especially to be clear it's read-only)

Actually I added the dot dfy at the end so the IDE can recognize it's Dafny code and provide ide tooling on it.

I think from the user perspective, opening a dotdfy file to view the sources inside a dotdoo file, seems good

Okay, I can live with it :)

We can still change the part after the dafny: in a follow-up PR, so let's not get hung up on this

I think, as part of adding .doo files, we should have added IDE navigation for .doo files as well, and then we would have already solved this. I think it would help with correctly designing .doo files as well. For example, we could have considered not making dotdoo a compressed file and instead having it be a single text file, so the IDE can open it directly, without the need for a dafny doo/library source command. Not saying we should have gone for that option, but at least we would have had a reason to consider it.

Thinking about dotdoo support in the IDE more, and given the way dotdoo files are currently structured, the dafny doo/library source command should support both on-disk files and files internal to the CLI, so it does need to take a URI, and then the dafny: uris exposed to the IDE should probably contain a URI after the dafny:. The IDE will chop off the dafny: part and pass the rest to dafny doo source

For example, we could have considered not making dotdoo a compressed file and instead having it be a single text file, so the IDE can open it directly, without the need for a dafny doo/library source command.

I definitely intended to iterate on the file format as we added features, and hence why the manifest has a doo_file_version property. :) But I don't think I'd want to make it a single text file, since then the manifest information would have to be embedded in comments or something like that, which would make it a bit tougher to read robustly and harder to hide that implementation detail from users.

Thinking about dotdoo support in the IDE more, and given the way dotdoo files are currently structured, the dafny doo/library source command should support both on-disk files and files internal to the CLI, so it does need to take a URI, and then the dafny: uris exposed to the IDE should probably contain a URI after the dafny:. The IDE will chop off the dafny: part and pass the rest to dafny doo source

Yup, this is one of the reasons I thought $"dafny:{internalUri}" would be smart, but you expressed it better than I managed at the time. :)

robin-aws · 2023-12-06T16:42:45Z

Source/DafnyCore/Rewriters/PrecedenceLinter.cs

    // Don't perform linting on doo files in general, since the source has already been processed.
    internal override void PostResolve(ModuleDefinition moduleDefinition) {
-      if (moduleDefinition.tok.Uri != null && moduleDefinition.tok.Uri.LocalPath.EndsWith(".doo")) {
+      if (moduleDefinition.tok.Uri != null && !moduleDefinition.ShouldVerify(compilation)) {


For the record I think this is a step backwards in terms of accuracy: not linting doo files is more about the fact that the content is read-only to consumers and not their responsibility to lint, nothing to do with verification.

I don't want to block this change on it, but perhaps we could at least add a comment in the next related PR.

I'm wondering whether ShouldVerify should be renamed to ShouldCheck.

The reasoning behind not verifying a file seem to apply to other correctness checks as well.

keyboardDrummer added 2 commits November 21, 2023 15:01

Use a doo:// scheme for contents from .doo files

c4805a9

Merge remote-tracking branch 'origin/master' into differentUriForDooFile

8ce5fb0

keyboardDrummer requested a review from robin-aws December 1, 2023 14:17

keyboardDrummer added 2 commits December 1, 2023 16:05

Do not write snippets for empty Uris

788ef9f

Allow reading the doo:// scheme files

e38e097

keyboardDrummer commented Dec 1, 2023

View reviewed changes

robin-aws requested changes Dec 1, 2023

View reviewed changes

keyboardDrummer added 4 commits December 4, 2023 15:25

Use dafny: as the externally visible scheme for standard library content

88e721d

Merge branch 'master' into differentUriForDooFile

c769a16

Add .dfy extension

f7004a3

Merge branch 'differentUriForDooFile' of github.com:keyboardDrummer/d…

72ff748

…afny into differentUriForDooFile

keyboardDrummer requested a review from robin-aws December 4, 2023 14:46

keyboardDrummer changed the title ~~Different uri for doo file~~ Use dafny: Uris for standard library files Dec 4, 2023

Merge branch 'master' into differentUriForDooFile

1a0d9d0

keyboardDrummer enabled auto-merge (squash) December 5, 2023 11:07

Small fixes

a05bc07

robin-aws reviewed Dec 5, 2023

View reviewed changes

robin-aws previously approved these changes Dec 5, 2023

View reviewed changes

keyboardDrummer added 2 commits December 6, 2023 12:29

Merge branch 'master' into differentUriForDooFile

f12acb6

Fix precendence linter exception

b5878f4

keyboardDrummer dismissed robin-aws’s stale review via b5878f4 December 6, 2023 14:50

Merge branch 'master' into differentUriForDooFile

97bd28c

robin-aws reviewed Dec 6, 2023

View reviewed changes

robin-aws approved these changes Dec 6, 2023

View reviewed changes

keyboardDrummer merged commit c90c6b4 into dafny-lang:master Dec 6, 2023
20 checks passed

keyboardDrummer deleted the differentUriForDooFile branch December 6, 2023 17:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use `dafny:` Uris for standard library files #4832

Use `dafny:` Uris for standard library files #4832

keyboardDrummer commented Dec 1, 2023 •

edited

Loading

keyboardDrummer Dec 1, 2023

robin-aws Dec 1, 2023

robin-aws Dec 1, 2023

robin-aws Dec 1, 2023

robin-aws left a comment

robin-aws Dec 5, 2023

keyboardDrummer Dec 5, 2023

robin-aws Dec 5, 2023

robin-aws Dec 5, 2023

keyboardDrummer Dec 5, 2023

robin-aws Dec 5, 2023

keyboardDrummer Dec 5, 2023 •

edited

Loading

robin-aws Dec 5, 2023

keyboardDrummer Dec 5, 2023

robin-aws Dec 5, 2023

keyboardDrummer Dec 6, 2023 •

edited

Loading

robin-aws Dec 6, 2023

robin-aws Dec 6, 2023

keyboardDrummer Dec 6, 2023

Use dafny: Uris for standard library files #4832

Use dafny: Uris for standard library files #4832

Conversation

keyboardDrummer commented Dec 1, 2023 • edited Loading

Description

How has this been tested?

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Dec 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Dec 6, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Use `dafny:` Uris for standard library files #4832

Use `dafny:` Uris for standard library files #4832

keyboardDrummer commented Dec 1, 2023 •

edited

Loading

keyboardDrummer Dec 5, 2023 •

edited

Loading

keyboardDrummer Dec 6, 2023 •

edited

Loading