Feat: Documenting Dafny Entities (Adding Docstring) #3756

MikaelMayer · 2023-03-17T18:50:29Z

We gathered as a team last July to discuss how to add first-class support for Docstring, which is the interpretation of a special comment used for documentation purposes, e.g. hovering a symbol and getting more information about it.

We asked the following questions:

What entities will have docstrings attached to them?. We decided that, for now: fields, methods (also lemmas), functions (also predicates), datatypes, datatype constructors, opaque types, subset types, newtypes, classes, traits and export declarations would have a docstring associated to them.
We did not consider attaching docstring to function parameters yet, nor docstring to requires/ensures clause (but the {:error} attribute can help) so I leave these out of scope for now.
What comment syntax to use for docstring?. We considered //, /* .. */, /// and /** ... */ and concluded that, in places where a comment would never be present except if it were a docstring (see below), all comments would count as docstrings and be concatenated together. In places a comment could be present and might or might not be a docstring (e.g. //TODO...), we would only support /***/ kind of docstring.
From what comments would docstring be extracted?.
Comments can be placed virtually between any two tokens in the code. There were essentially two ways to place comments so that they can be interpreted as doscstring: Either above the entity, or below the entity. It turns out that there was no consensus on which one would be preferred (50%-50% of voices for a quorum of 6). Placing the comment below looks more like a regular definition (here is the entity, here is the definition) and is taken by some languages (Python, Caml...), while placing it above is what some other languages like C# or Java do.
Our collective decision was to interpret comments placed below automatically as docstring first, because they are not ambiguous, and start to use it by default when writing Dafny ourselves. If not below, we would recognize comments above /** ... */ as docstring.
You will find below two same source code with the two different versions.
What syntax do we support for converting docstring?.
By default, we only remove comment signs and properly re-indent the docstring, but we do not process it further.
Because Dafny's currently supported IDE has VSCode whicih displays hover messages in Markdown, we expect users to write their docstring in Markdown though.
We also decided that we would enable a plugin-based rewriting of the docstring so that users can format it the way they want, and that Javadoc could be an example of such a plugin that we would provide as an example but not provide support for it, as users should relatively easily be able to override it.

Implementation

This PR adds a new interface IHasDocstring with the method .GetDocstring(DafnyOptions options)
All nodes implement the method but only a specific subset implement the interface. The docstrings are tested with respect to our decision in DafnyPipeline
The first "*" and space of every long comment is removed, except if there was a line after the first one which did not start with a star. If there is no star at all, multiline comments are left-trimmed to match the space before the /* + two spaces, assuming the /* is the first non-whitespace character of the line.
This PR also adds a small Javadoc-like-to-markdown converter that can be activated with the flag --javadoclike-docstring-plugin, which I hope will be activated by default when using the language server from a future version of VSCode. The goal is to provide a helper for those who are used to this syntax, not support the entire javadoc language
This PR also adds support for the hover handler to actually display docstring when hovering over existing symbols. I left out of scope to add support for more symbol lookup as I saw some were missing.

Screenshots

Additional notes

I can split this PR on demand if necessary.

Appendix

Docstring after/below entities - preferred choice (example)

/// file comments


module A
  // module comment
{
}


method read(x: string, y: string) returns (z: int)
  // reads file in this.buffer
  modifies this`buffer
  ensures z > 0
  ensures z == abs(x + y)
{ … }

var x := 7
// This is docstring about x

// This is just a comment and not a docstring
const C := 8 // This is docstring about C

const C := 8
// This is docstring about C
// On two lines

datatype T0 =  // Docstring for T
  | A(x: int,
      y: int) // Docstring for A
  | B()       /* Docstring for B */ |
    C()       // Docstring for C

datatype T1 =
  // Docstring for T
  | A(x: int,
      y: int)
    // Docstring for A
  /* Still a docstring for A */ | B() // This is for B
  | C() /* Docstring for C */


export
  // This is the eponymous export set intended for most clients
  provides A, B, C


export Friends extends M
  // This export set is for clients who need to know more of the
  // details of the module's definitions.
  reveals A
  provides D

Docstring before/above entities, also supported (example)

/// Not a docstring, can be used as the file comment or for literate programming

/** module comment */
module A {
}


/** reads file in this.buffer */
method read(x: string, y: string) returns (z: string)
  modifies this`buffer
  ensures z > 0
  ensures z == abs(x + y)
{ … }

/** This is docstring about x */
var x := 7
// This is docstring about x part 2


/** This is docstring about x */
var x := 7


/** Docstring for T0*/
datatype T0 =
  | /** Docstring for A */
    A(x: int,
      y: int)
  | /** Docstring for B */
    B()
  | /** Docstring for C */
    C()


/** This is the eponymous export set intended for most clients */
export provides A, B, C

/** This export set is for clients who need to know more of the
  * details of the module's definitions. */
export Friends extends M
  reveals A
  provides D

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

davidcok · 2023-03-20T17:52:12Z

Source/DafnyCore/AST/MemberDecls.cs

+      return EndToken.TrailingTrivia;
+    }
+
+    return GetTriviaContainingDocstringFromStartTokeOrNull();


Suggested change

return GetTriviaContainingDocstringFromStartTokeOrNull();

return GetTriviaContainingDocstringFromStartTokenOrNull();

And anywhere else this name is used

davidcok · 2023-03-20T18:03:09Z

Source/DafnyCore/Generic/Node.cs

+      var match = matches[i];
+      if (match.Groups["multiline"].Success) {
+        // For each line except the first,
+        // we need to remove the indentation up to the first "/" of the comment


I don't understand 'up to the first /'
I would think that if there is initial white space followed by a * and optional space but not a /, that text is removed.
There is initial white space and then one or more * and a / then that is a comment end.

Rephrased to

// we need to remove the indentation on every line. // The length of removed indentation is maximum the space before the first "/*" + 3 characters

davidcok · 2023-03-20T18:11:41Z

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

+
+method test(d: D, t: T, e: Even) {
+//             ^[Rich comment for D]
+ //                   ^[D whose value is even] // Not working yet


not working yet? A later PR?

Yes. It's another mechanism with symbols that needs to be fixed, maybe @keyboardDrummer who implemented jump to definition can figure out why there is no information on hovering the subset type T and Even

davidcok · 2023-03-20T18:14:02Z

Source/DafnyPipeline.Test/DocstringTest.cs

+function Test10(i: int): int
+  /* Test10 computes an int
+      It takes an int and adds 10 to it */
+{ i + 1 }


Suggested change

{ i + 1 }

{ i + 10 }

davidcok · 2023-03-20T18:14:16Z

Source/DafnyPipeline.Test/DocstringTest.cs

+function Test11(i: int): int
+  /** Test11 computes an int
+    *  It takes an int and adds 11 to it */
+{ i + 1 }


Suggested change

{ i + 1 }

{ i + 11 }

davidcok · 2023-03-20T18:16:39Z

Source/DafnyPipeline.Test/DocstringTest.cs

+    public void DocstringWorksForSubsetType() {
+      DocstringWorksFor(@"
+type Odd = x: int | x % 2 == 1 witness 1
+// Type of number that are not divisible by 2 


Suggested change

// Type of number that are not divisible by 2

// Type of numbers that are not divisible by 2

davidcok · 2023-03-20T22:07:21Z

Source/DafnyCore/Generic/Node.cs

+        // we need to remove the indentation up to the first "/" of the comment
+        // Additionally, if there is a "* " or a " *" or a "  * ", we remove it as well
+        // provided it always started with a star.
+        //var startIndex = match.Groups["multiline"].Index;


Should these next two lines be deleted?

davidcok · 2023-03-20T22:13:14Z

Source/DafnyCore/Generic/Node.cs

@@ -21,6 +23,11 @@ public interface ICanFormat : INode {
  bool SetIndent(int indentBefore, TokenNewIndentCollector formatter);
 }

+// A node that can have a docstring attached to it
+public interface IHasDocstring : INode {
+  string GetDocstring(DafnyOptions options);


Should we also have a method call GetDocstringSummary that produces a summary (e.g. the first sentence) of the docstring. Certainly a dafny doc tool would need such, though it could be defined in that tool if you don't think other tools would need it.

To extract the first sentence, you need to do something non-trivial, such as detecting a period in the docstring, which seems arbitrary. We haven't discussed that the docstring should have one sentence first that indicates the summary (for example a good docstring could also be an example of API usage) hence I would prefer a dafny doc tool to define it by itself for the format of docstring it wants to support.

davidcok

I'll likely have more comments when I actually use it.

MikaelMayer and others added 11 commits March 16, 2023 14:23

Feat: Docstring

0900197

Added remaining failing tests

fe9d93e

Method, const, module docstring

244c8dc

docstring for classes, consts

46a693e

Docstring for iterators, datatypes and their constructors

de568fd

All hover tests to pass

e3de3d5

Refactored the code + towncrier

5c56c79

Support for export sets and newtypes

71a1bba

Adopted the consensus

98e5691

Fixed the CI error

86c77d4

Merge branch 'master' into feat-docstring

6be4481

MikaelMayer mentioned this pull request Mar 20, 2023

Feat: Hover in language server display documentation #2364

Closed

MikaelMayer requested a review from davidcok March 20, 2023 20:48

davidcok requested changes Mar 20, 2023

View reviewed changes

davidcok reviewed Mar 20, 2023

View reviewed changes

MikaelMayer added 2 commits March 21, 2023 09:38

Merge branch 'master' into feat-docstring

f726c62

Merge remote-tracking branch 'origin/feat-docstring' into feat-docstring

80538fd

MikaelMayer requested a review from davidcok March 21, 2023 14:40

davidcok previously approved these changes Mar 21, 2023

View reviewed changes

Review comments

11b6f6b

MikaelMayer dismissed davidcok’s stale review via 11b6f6b March 21, 2023 19:01

Merge branch 'master' into feat-docstring

18a72c8

davidcok approved these changes Mar 22, 2023

View reviewed changes

MikaelMayer merged commit 0ef835d into master Mar 22, 2023

MikaelMayer deleted the feat-docstring branch March 22, 2023 15:52

tchajed mentioned this pull request May 10, 2023

dafny 4.1.0 Homebrew/homebrew-core#130682

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat: Documenting Dafny Entities (Adding Docstring) #3756

Feat: Documenting Dafny Entities (Adding Docstring) #3756

MikaelMayer commented Mar 17, 2023 •

edited by wilcoxjay

Loading

davidcok Mar 20, 2023

davidcok Mar 20, 2023

MikaelMayer Mar 21, 2023

davidcok Mar 20, 2023

MikaelMayer Mar 21, 2023

davidcok Mar 20, 2023

davidcok Mar 20, 2023

davidcok Mar 20, 2023

davidcok Mar 20, 2023

davidcok Mar 20, 2023

MikaelMayer Mar 21, 2023

davidcok left a comment

	return GetTriviaContainingDocstringFromStartTokeOrNull();
	return GetTriviaContainingDocstringFromStartTokenOrNull();

	// Type of number that are not divisible by 2
	// Type of numbers that are not divisible by 2

Feat: Documenting Dafny Entities (Adding Docstring) #3756

Feat: Documenting Dafny Entities (Adding Docstring) #3756

Conversation

MikaelMayer commented Mar 17, 2023 • edited by wilcoxjay Loading

Implementation

Screenshots

Additional notes

Appendix

Docstring after/below entities - preferred choice (example)

Docstring before/above entities, also supported (example)

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

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

davidcok left a comment

Choose a reason for hiding this comment

MikaelMayer commented Mar 17, 2023 •

edited by wilcoxjay

Loading