Skip to content

Commit

Permalink
Fix "assertion batch" anchor (dafny-lang#5096)
Browse files Browse the repository at this point in the history
### Description
This is a fix for the broken "assertion batch" anchor -- an example use
of it is below:


![assertion-batch-link](https://github.com/dafny-lang/dafny/assets/12002672/e34d1c7e-e5d9-4314-806e-41e3294f0a1e)

The anchor was originally
`#sec-verification-attributes-on-assert-statements` which currently
doesn't exist. The closest existing anchor appears to be
[`#sec-verification-attributes-on-assertions`](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-verification-attributes-on-assertions)
but I think linking to the section for the anchor
[`#sec-assertion-batches`](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-assertion-batches)
is better since that section introduces the _assertion batch_ concept.

### How has this been tested?
I have not compiled the Dafny VSCode extension locally, but this PR
changes tests and the CI should be green.

----

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
kazarmy authored Feb 16, 2024
1 parent 73fcdf3 commit af84d77
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ await AssertVerificationHoverMatches(documentItem, (0, 36),
@"**Verification performance metrics for method `f`**:
- Total resource usage: ??? RU
- Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-attributes-on-assert-statements):
- Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches):
- #???/??? with 1 assertion at line ???, ??? RU
- #???/??? with 1 assertion at line ???, ??? RU "
);
Expand Down Expand Up @@ -223,7 +223,7 @@ await AssertVerificationHoverMatches(documentItem, (0, 36),
@"**Verification performance metrics for function `f`**:
- Total resource usage: ??? RU
- Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-attributes-on-assert-statements):
- Most costly [assertion batches](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches):
- #???/2 with 2 assertions at line ???, ??? RU
- #???/2 with 2 assertions at line ???, ??? RU"
);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
Original file line number Diff line number Diff line change
Expand Up @@ -441,7 +441,7 @@ public static string FormatResourceCount(long nodeResourceCount) {
}

private static string AddAssertionBatchDocumentation(string batchReference) {
return $"[{batchReference}](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-verification-attributes-on-assert-statements)";
return $"[{batchReference}](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-assertion-batches)";
}

private static Hover CreateMarkdownHover(string information) {
Expand Down

0 comments on commit af84d77

Please sign in to comment.