-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: Document outline for functions and methods without body #1536
Merged
keyboardDrummer
merged 6 commits into
master
from
camrein/fix-symbols-for-bodyless-declarations
Oct 25, 2021
Merged
fix: Document outline for functions and methods without body #1536
keyboardDrummer
merged 6 commits into
master
from
camrein/fix-symbols-for-bodyless-declarations
Oct 25, 2021
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
keyboardDrummer
approved these changes
Oct 25, 2021
keyboardDrummer
deleted the
camrein/fix-symbols-for-bodyless-declarations
branch
October 25, 2021 11:54
prvshah51
added a commit
to prvshah51/dafny
that referenced
this pull request
Oct 25, 2021
* fix: Const initializations problems dafny-lang#1111 (dafny-lang#1509) Fixed dafny-lang#1111 * Only emit captureState when debugging with /mv (dafny-lang#1465) ### Changes - Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation. ### Testing - A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify. * Separate document verification from load (dafny-lang#1516) * Extracted the text change migration into a new service * Added cancellation token to the position resolution * Added the possible exceptions to the XML doc. * Extracted the symbol relocation into a dedicated service * Removed the default token argument * Moved document updates to database to make it fully responsible of cancellation * Added integration tests for OnSave/Never verification status messages * Made document opening more self-descriptive * Moved the verification responsibility to the document database * Removed the SerializedCounterExamples from the document constructor * Restructured code * Reduce the TPL stress by mutually exclude verification asynchronously * Moved verification back to the document loader * Fixed doc typos * Now verifying documents on the large stack thread Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Enhance `Import` printer (dafny-lang#1487) This commit optimises `Import M = M` to `Import M`, and `Import M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests for module insertion. Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Counterexamples from Command Line (dafny-lang#1511) * Move position extraction to DafnyModelState * Move DafnyModel parsing to DafnyModel class * Add /extractCounterExample option * Add a lit Test * Update option description * Change source location reporting Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore(version): Bump version for pre-release (dafny-lang#1524) * Bump version for pre-release * Allow PR title to satisfy semantic PRs app * chore: Fix version number in attributes (dafny-lang#1525) * Add document symbols to support outline (dafny-lang#1483) Enable support for document outlines and the breadcrumb navigation at the top of the editor. Co-authored-by: Remy Willems <rgv.willems@gmail.com> * chore: xUnit-based lit test runner (dafny-lang#680) Adds an xUnit-based test runner for all of the lit tests under Test. The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite. Where this alternate runner really shines is in IDEs that support .NET test frameworks: Getting a tree of test results in the UI Being able to re-run/debug individual tests by right-clicking on them Filtering by test name (e.g. dotnet test --filter DisplayName~allocated) (Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.) This change adds two new .NET packages: XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter. IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory. Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package. There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory. Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged). Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Update Boogie to 2.9.4 (dafny-lang#1531) Co-authored-by: Remy Willems <> * No more `assume 2 < 2;` (dafny-lang#1354) * Add test file * Don't remove Lit brackets when assert/assume By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`. * Refactor Assert helper methods This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway. * Redo changes lost in the merge Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * fix: Document outline for functions and methods without body (dafny-lang#1536) This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature). The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1. Co-authored-by: Remy Willems <rgv.willems@gmail.com> Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com> Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com> Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Rustan Leino <leino@amazon.com>
prvshah51
added a commit
that referenced
this pull request
Nov 17, 2021
* fix: Const initializations problems #1111 (#1509) Fixed #1111 * Only emit captureState when debugging with /mv (#1465) ### Changes - Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation. ### Testing - A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify. * Separate document verification from load (#1516) * Extracted the text change migration into a new service * Added cancellation token to the position resolution * Added the possible exceptions to the XML doc. * Extracted the symbol relocation into a dedicated service * Removed the default token argument * Moved document updates to database to make it fully responsible of cancellation * Added integration tests for OnSave/Never verification status messages * Made document opening more self-descriptive * Moved the verification responsibility to the document database * Removed the SerializedCounterExamples from the document constructor * Restructured code * Reduce the TPL stress by mutually exclude verification asynchronously * Moved verification back to the document loader * Fixed doc typos * Now verifying documents on the large stack thread Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Enhance `Import` printer (#1487) This commit optimises `Import M = M` to `Import M`, and `Import M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests for module insertion. Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Counterexamples from Command Line (#1511) * Move position extraction to DafnyModelState * Move DafnyModel parsing to DafnyModel class * Add /extractCounterExample option * Add a lit Test * Update option description * Change source location reporting Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore(version): Bump version for pre-release (#1524) * Bump version for pre-release * Allow PR title to satisfy semantic PRs app * chore: Fix version number in attributes (#1525) * Add document symbols to support outline (#1483) Enable support for document outlines and the breadcrumb navigation at the top of the editor. Co-authored-by: Remy Willems <rgv.willems@gmail.com> * chore: xUnit-based lit test runner (#680) Adds an xUnit-based test runner for all of the lit tests under Test. The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite. Where this alternate runner really shines is in IDEs that support .NET test frameworks: Getting a tree of test results in the UI Being able to re-run/debug individual tests by right-clicking on them Filtering by test name (e.g. dotnet test --filter DisplayName~allocated) (Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.) This change adds two new .NET packages: XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter. IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory. Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package. There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory. Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged). Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Update Boogie to 2.9.4 (#1531) Co-authored-by: Remy Willems <> * No more `assume 2 < 2;` (#1354) * Add test file * Don't remove Lit brackets when assert/assume By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`. * Refactor Assert helper methods This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway. * Redo changes lost in the merge Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * fix: Document outline for functions and methods without body (#1536) This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature). The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1. Co-authored-by: Remy Willems <rgv.willems@gmail.com> Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com> Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com> Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Rustan Leino <leino@amazon.com>
prvshah51
added a commit
that referenced
this pull request
Nov 17, 2021
* fix: Const initializations problems #1111 (#1509) Fixed #1111 * Only emit captureState when debugging with /mv (#1465) - Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation. - A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify. * Separate document verification from load (#1516) * Extracted the text change migration into a new service * Added cancellation token to the position resolution * Added the possible exceptions to the XML doc. * Extracted the symbol relocation into a dedicated service * Removed the default token argument * Moved document updates to database to make it fully responsible of cancellation * Added integration tests for OnSave/Never verification status messages * Made document opening more self-descriptive * Moved the verification responsibility to the document database * Removed the SerializedCounterExamples from the document constructor * Restructured code * Reduce the TPL stress by mutually exclude verification asynchronously * Moved verification back to the document loader * Fixed doc typos * Now verifying documents on the large stack thread Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Enhance `Import` printer (#1487) This commit optimises `Import M = M` to `Import M`, and `Import M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests for module insertion. Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Counterexamples from Command Line (#1511) * Move position extraction to DafnyModelState * Move DafnyModel parsing to DafnyModel class * Add /extractCounterExample option * Add a lit Test * Update option description * Change source location reporting Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore(version): Bump version for pre-release (#1524) * Bump version for pre-release * Allow PR title to satisfy semantic PRs app * chore: Fix version number in attributes (#1525) * Add document symbols to support outline (#1483) Enable support for document outlines and the breadcrumb navigation at the top of the editor. Co-authored-by: Remy Willems <rgv.willems@gmail.com> * chore: xUnit-based lit test runner (#680) Adds an xUnit-based test runner for all of the lit tests under Test. The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite. Where this alternate runner really shines is in IDEs that support .NET test frameworks: Getting a tree of test results in the UI Being able to re-run/debug individual tests by right-clicking on them Filtering by test name (e.g. dotnet test --filter DisplayName~allocated) (Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.) This change adds two new .NET packages: XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter. IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory. Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package. There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory. Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged). Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Update Boogie to 2.9.4 (#1531) Co-authored-by: Remy Willems <> * No more `assume 2 < 2;` (#1354) * Add test file * Don't remove Lit brackets when assert/assume By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`. * Refactor Assert helper methods This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway. * Redo changes lost in the merge Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * fix: Document outline for functions and methods without body (#1536) This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature). The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1. Co-authored-by: Remy Willems <rgv.willems@gmail.com> Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com> Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com> Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Rustan Leino <leino@amazon.com>
prvshah51
added a commit
that referenced
this pull request
Nov 17, 2021
* fix: Const initializations problems #1111 (#1509) Fixed #1111 * Only emit captureState when debugging with /mv (#1465) - Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation. - A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify. * Separate document verification from load (#1516) * Extracted the text change migration into a new service * Added cancellation token to the position resolution * Added the possible exceptions to the XML doc. * Extracted the symbol relocation into a dedicated service * Removed the default token argument * Moved document updates to database to make it fully responsible of cancellation * Added integration tests for OnSave/Never verification status messages * Made document opening more self-descriptive * Moved the verification responsibility to the document database * Removed the SerializedCounterExamples from the document constructor * Restructured code * Reduce the TPL stress by mutually exclude verification asynchronously * Moved verification back to the document loader * Fixed doc typos * Now verifying documents on the large stack thread Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Enhance `Import` printer (#1487) This commit optimises `Import M = M` to `Import M`, and `Import M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests for module insertion. Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Counterexamples from Command Line (#1511) * Move position extraction to DafnyModelState * Move DafnyModel parsing to DafnyModel class * Add /extractCounterExample option * Add a lit Test * Update option description * Change source location reporting Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore(version): Bump version for pre-release (#1524) * Bump version for pre-release * Allow PR title to satisfy semantic PRs app * chore: Fix version number in attributes (#1525) * Add document symbols to support outline (#1483) Enable support for document outlines and the breadcrumb navigation at the top of the editor. Co-authored-by: Remy Willems <rgv.willems@gmail.com> * chore: xUnit-based lit test runner (#680) Adds an xUnit-based test runner for all of the lit tests under Test. The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite. Where this alternate runner really shines is in IDEs that support .NET test frameworks: Getting a tree of test results in the UI Being able to re-run/debug individual tests by right-clicking on them Filtering by test name (e.g. dotnet test --filter DisplayName~allocated) (Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.) This change adds two new .NET packages: XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter. IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory. Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package. There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory. Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged). Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Update Boogie to 2.9.4 (#1531) Co-authored-by: Remy Willems <> * No more `assume 2 < 2;` (#1354) * Add test file * Don't remove Lit brackets when assert/assume By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`. * Refactor Assert helper methods This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway. * Redo changes lost in the merge Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * fix: Document outline for functions and methods without body (#1536) This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature). The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1. Co-authored-by: Remy Willems <rgv.willems@gmail.com> Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com> Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com> Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Rustan Leino <leino@amazon.com>
prvshah51
added a commit
to prvshah51/dafny
that referenced
this pull request
May 25, 2022
* fix: Const initializations problems dafny-lang#1111 (dafny-lang#1509) Fixed dafny-lang#1111 * Only emit captureState when debugging with /mv (dafny-lang#1465) ### Changes - Do not emit `assume {:capturestate ...} true` statements unless the `/mv:<file>` option, which is only used for debugging, is passed. These statements contained source locations which prevent proof isolation. ### Testing - A side effect of the first change is that source locations in error messages may shift, since previously sometimes the location attached to an `assume {:capturestate ...} true` at the end of a block, which would be the location of any `ensures` clauses, was being picked as the return location of the block. I believe the new behavior is better so I've updated the tests, but please verify. * Separate document verification from load (dafny-lang#1516) * Extracted the text change migration into a new service * Added cancellation token to the position resolution * Added the possible exceptions to the XML doc. * Extracted the symbol relocation into a dedicated service * Removed the default token argument * Moved document updates to database to make it fully responsible of cancellation * Added integration tests for OnSave/Never verification status messages * Made document opening more self-descriptive * Moved the verification responsibility to the document database * Removed the SerializedCounterExamples from the document constructor * Restructured code * Reduce the TPL stress by mutually exclude verification asynchronously * Moved verification back to the document loader * Fixed doc typos * Now verifying documents on the large stack thread Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Enhance `Import` printer (dafny-lang#1487) This commit optimises `Import M = M` to `Import M`, and `Import M\`{N}` to `Import M\`N`. It also fixes and adds to the existing tests for module insertion. Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Counterexamples from Command Line (dafny-lang#1511) * Move position extraction to DafnyModelState * Move DafnyModel parsing to DafnyModel class * Add /extractCounterExample option * Add a lit Test * Update option description * Change source location reporting Co-authored-by: Robin Salkeld <salkeldr@amazon.com> * chore(version): Bump version for pre-release (dafny-lang#1524) * Bump version for pre-release * Allow PR title to satisfy semantic PRs app * chore: Fix version number in attributes (dafny-lang#1525) * Add document symbols to support outline (dafny-lang#1483) Enable support for document outlines and the breadcrumb navigation at the top of the editor. Co-authored-by: Remy Willems <rgv.willems@gmail.com> * chore: xUnit-based lit test runner (dafny-lang#680) Adds an xUnit-based test runner for all of the lit tests under Test. The new runner supports executing commands such as %dafny by directly invoking the main entry point of the corresponding C# package (i.e. DafnyDriver), which makes running the debugger against a particular test much more convenient. By default this is disabled and the runner creates a separate dafny process just as lit does, however. This is because the main CLI implementation currently has shared static state, which causes errors when invoking the CLI in the same process on multiple inputs in sequence, much less in parallel. Future changes will address this so that the in-process Main invocation can be used instead, however, which will likely improve performance but more importantly allow us to measure code coverage of the test suite. Where this alternate runner really shines is in IDEs that support .NET test frameworks: Getting a tree of test results in the UI Being able to re-run/debug individual tests by right-clicking on them Filtering by test name (e.g. dotnet test --filter DisplayName~allocated) (Earlier versions of this PR went further and aimed to convert the lit tests to a new format. We may still want to do this in the future, but parsing and understanding the existing test suite is a necessary prerequisite anyway.) This change adds two new .NET packages: XUnitExtensions - Contains a few generic extensions to xUnit to support file-based parameterized tests (a.k.a. Theories), and the alternate Lit test interpreter. IntegrationTests - Contains a single file-based parameterized xUnit test to run all lit tests in the Test directory. Other .NET projects that use lit, such as Boogie, could also leverage this runner by depending on the generic XUnitExtensions package and defining a similar second package. There is one fundamental difference in behavior between the two runners: our current lit configuration uses the immediate directory of each test case as the current directory, whereas .NET test runners always run in the single project output directory (e.g. IntegrationTests/bin/Debug/net5.0). It wouldn't be feasible to change the current directory to match lit's behavior, since multiple parallel tests cannot do this at the same time. Instead, I prepended the %S substitution macro to a handful of command arguments that were relative paths, and otherwise ensured the tests did not depend on the current directory. Because the IntegrationTests package runs all tests out of the output directory rather than the Test directory, its csproj configuration and its dependencies ensure that a few additional files are also copied into that directory, such as z3 and the necessary runtime files. I also applied this technique to the other test projects to avoid the manual step of copying z3 as described in the wiki (and will remove that step once this PR is merged). Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * Update Boogie to 2.9.4 (dafny-lang#1531) Co-authored-by: Remy Willems <> * No more `assume 2 < 2;` (dafny-lang#1354) * Add test file * Don't remove Lit brackets when assert/assume By removing this optimization (?), a condition like `false` is no longer passed to Boogie that way, but instead of `Lit(false)`. * Refactor Assert helper methods This change also removes a redundant `this.assertionCount++;`. This increment is done by the `builder.Add` method anyway. * Redo changes lost in the merge Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Remy Willems <rgv.willems@gmail.com> * fix: Document outline for functions and methods without body (dafny-lang#1536) This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature). The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1. Co-authored-by: Remy Willems <rgv.willems@gmail.com> Co-authored-by: Christoph Amrein <camrein@users.noreply.github.com> Co-authored-by: hirataqdees <syeda.hira.taqdees@gmail.com> Co-authored-by: Hira Syeda <syedahir@amazon.com> Co-authored-by: Aleksandr Fedchin <sasha.fedchin@gmail.com> Co-authored-by: Robin Salkeld <salkeldr@amazon.com> Co-authored-by: Alex Cioc <4691979+acioc@users.noreply.github.com> Co-authored-by: Rustan Leino <leino@amazon.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature).
The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using
tok
andBodyEndTok
. However,BodyEndTok
is set toToken.NoToken
if there is no body, leading to a range ending at line -1.