feat: Standard library support + DafnyStdLibs.Wrappers #4678

robin-aws · 2023-10-18T03:54:50Z

Description

This change adds support for "standard libraries" that are packaged together with the Dafny distribution, at least for now. They are automatically available for import with the option --standard-libraries, which will likely become true by default in Dafny 5. To avoid Dafny's footprint from getting larger and larger over time, some portion of them may be moved into separately distributed packages at a later date. They will remain optional and the Dafny language itself should not depend on them.

A later change will likely add pre-translated source to the runtimes as well, and a translation option such as --include-standard-libraries similar to --include-runtime to rely on this copy of them instead of translating them into every component.

Implementation notes:

The primary implementation approach, which is mostly not user-visible, is to pre-build one or more .doo files and embed them in DafnyPipeline.dll, just as we already do with the various runtime files such as DafnyRuntime.dll. They are added as input DafnyFiles, using URIs of the form dllresource://DafnyPipeline/<name>.doo, so they are not re-verified but are in scope for compilation.
I've fixed/improved a few things around .doo files, such as loosening the library checks for some options, and no longer checking options that only affect compilation (it may make sense to leverage these files for compilation compatibility checking in the future but that's not currently in scope).
The current limitations of the standard library support are documented in Source/DafnyStandardLibraries/CONTRIBUTING.md, and should make it clear which pending libraries are still partially blocked.

How has this been tested?

The general standard library support is tested with the integration tests under stdlibs and metatests/StdLibsOffByDefaultInTests.dfy
The Wrappers library is tested via WrappersExamples.dfy

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

Source/DafnyCore/AST/Grammar/ProgramParser.cs

Source/DafnyStandardLibraries/scripts/check-examples

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.dfy

Source/DafnyStandardLibraries/src/dfyconfig.toml

Test/metatests/StdLibsOffByDefaultInTests.dfy

Fixes #446 ### Description Do not let documentSymbol API return a faulty line when parsing a symbol name has an error ### How has this been tested? - Added language server test 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).

### Description Attempt at making `QuickEditsInLargeFile` pass more reliably on OSX ### How has this been tested? It's a change intended to affect the existing test `QuickEditsInLargeFile` 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).

Move Littish tests from `Test` to `Source/IntegrationTests/Test`. This way there's no symlink needed which causes Rider to behave annoyingly 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).

keyboardDrummer · 2023-10-20T12:01:42Z

Source/DafnyCore/DooFile.cs

@@ -212,6 +221,30 @@ public class ManifestData {
    return false;
  }

+  // Checks that the library option ==> the local option.


I think it's better to use /// comments. IDE will then also move the comments if you move the definition.

keyboardDrummer · 2023-10-20T12:16:34Z

Source/DafnyStandardLibraries/CONTRIBUTING.md

+but we should be very resistant to raising the limit in the checked in copy.
+
+**Brittleness of code using the standard libraries**: This one is tougher.
+There is tension between two different use cases:


Should imports have the ability to customize opaqueness ? @MikaelMayer

Have chatted with @jtristan about this a bit too. Cut #4697 to follow up with ideas.

We can deal with this at the library side by refining modules and expose more or less data, and also define careful export sets.
That way, customizing opaqueness is done at the import level.

I also wish users should also be able to refine a library module while exposing everything, and then in their refining module they could hide everything they don't want.

keyboardDrummer · 2023-10-20T12:23:28Z

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.md

+be applied. When a FC-value is returned by a method there is no place to call such a conversion function: the return value of the method must be captured by either `:=` or `:-`.
+So some new syntax will be needed --- what this will be is under design and discussion.
+
+The workaround, however, is straitforward: just capture the results using `:=` and make the conversion directly. Here the is example above restated using a method.


give it to me STRAIT

keyboardDrummer · 2023-10-20T12:39:40Z

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.md

+
+The Wrappers module holds some
+simple datatypes to support common patterns, such as optional values or the result of operations that can fail.
+These are additionally useful with Dafny's abrupt-termination-on-failure `:-` operator.


I'm not a native English speaker but: additionally -> particularly?

keyboardDrummer · 2023-10-20T12:41:08Z

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.md

+- `Outcome<E>` - which is either `Pass` with no informatino or `Fail` with an error value of type `E` (often a `string`) 
+- `Result<R,E>` - which is either `Success` with a value of type `R` or `Failure` with error value of type `E`
+
+These are common programming idioms. The main complication comes when they are mixed in the same program.


Consider leaving out line 16. Line 5 already says these datatypes help with common patterns, and the second sentence on line 16 does not constructive to me.

keyboardDrummer · 2023-10-20T12:43:19Z

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.md

+
+In this library module Dafny defines three such types:
+- `Option<R>` - which is either `Some` with a value of type `T` or a `None` with no information
+- `Outcome<E>` - which is either `Pass` with no informatino or `Fail` with an error value of type `E` (often a `string`) 


informatino

keyboardDrummer · 2023-10-20T12:44:15Z

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.md

+```
+
+You could just capture the result of `Find` using `:=` in a `Option<int>` variable and inspect it. But if the `None` condition is 
+generally a rare error, it is easy to forget to always check that each operation was successful. Instead, the `:-` changes the 


I think I prefer this text not to have line breaks, so the viewer can take care of the appropriate breaking.

Looks like this when I'm reading it

My general preference is loosely adhering to https://sembr.org/ personally. I didn't want to edit this too heavily so we can see a clean diff against the original, though: https://github.com/dafny-lang/libraries/blob/master/src/dafny/Wrappers.md

I don't get it. Why wouldn't you want regular text to look the same when writing as when reading? If we're soft-wrapping it with no explicit line breaks when reading, why not also write it like that?

keyboardDrummer · 2023-10-20T12:45:54Z

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.md

+See the [reference manual](https://dafny.org/latest/DafnyRef/DafnyRef#sec-update-with-failure-statement)
+for more on the similarities and differences with exceptions.
+
+### Outcome


Is this used a lot? C#'s anonymous records Option<(int x, string y)> seem nicer

I actually disagree with the statement that this is the most common use case. It's more important that returning an Outcome instead of a Result means you can say :- CheckSomeThings(x) as opposed to var _ :- CheckSomeThings(x), where in the latter case it's too easy to do var _ := CheckSomeThings(x) which has no effect!

Rewriting.

Ended up just flipping the order of use cases.

keyboardDrummer · 2023-10-20T13:00:00Z

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.md

+
+A `Result` carries both a success value and failure information, with two separate, specifiable types. Its use is then very similar to `Option`.
+
+### Combining different FC-types in expressions


While the acronym FC has been defined before (once, and was not used afterwards), I would not use it in the title here.

Agreed about the titles, although "FC" is used a handful of times in the content.

keyboardDrummer

Amazing! Love it

jtristan · 2023-10-20T15:15:35Z

Source/DafnyStandardLibraries/CONTRIBUTING.md

+enforcing a tight upper-bound on the resources needed to verify each batch of assertions.
+For simplicitly, this project just sets a direct `--resource-limit`,
+rather than relying on the second-pass approach of the `dafny-reportgenerator`.
+I have set this limit aggressively low in the hopes that we can maintain it


I would use a passive voice there.

…ndard-library-support-verification-only

robin-aws added 13 commits October 17, 2023 16:43

First pass at adding build support

07c0eb4

More C# progress, try out Java

a8e2ca0

Leave compilation out of scope for now

4bdaa29

Get basic testing working

aac5c7e

Rename, work around Go bug

6a7d06e

Hook up option

a20ddb6

Off by default in tests

e854330

Add documentation and hook up check-examples

0d4e4c4

Disable by default in general for now

74b4ea0

Tweaks

0af73be

Temporarily checking in stdlib.doo

c47f90f

Better default make target

bd2dae0

Add CI

9fba8ff

robin-aws changed the title ~~feat: Standard library support (verification only), DafnyStdLib.Wrappers~~ feat: Standard library support (verification only), DafnyStdLib.Wrappers (WIP) Oct 18, 2023

robin-aws added 2 commits October 17, 2023 21:01

Working directory for make

3c3ccd1

Whitespace

bcdfe06

keyboardDrummer reviewed Oct 18, 2023

View reviewed changes

Source/DafnyCore/AST/Grammar/ProgramParser.cs Show resolved Hide resolved

keyboardDrummer reviewed Oct 18, 2023

View reviewed changes

Source/DafnyStandardLibraries/scripts/check-examples Show resolved Hide resolved

keyboardDrummer reviewed Oct 18, 2023

View reviewed changes

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.dfy Outdated Show resolved Hide resolved

keyboardDrummer reviewed Oct 18, 2023

View reviewed changes

Source/DafnyStandardLibraries/src/dafnystdlibs/Wrappers.dfy Outdated Show resolved Hide resolved

keyboardDrummer reviewed Oct 18, 2023

View reviewed changes

Source/DafnyStandardLibraries/src/dfyconfig.toml Outdated Show resolved Hide resolved

keyboardDrummer reviewed Oct 18, 2023

View reviewed changes

Test/metatests/StdLibsOffByDefaultInTests.dfy Outdated Show resolved Hide resolved

robin-aws mentioned this pull request Oct 18, 2023

Feature request: automatic testing of documentation examples #4680

Open

robin-aws and others added 7 commits October 18, 2023 08:55

PR feedback

8e128cd

Typo in directory

26b5a62

Add link to check-examples

fdce3d6

Off by default in tests

aa9cc46

Fix bad merge

955e397

keyboardDrummer reviewed Oct 20, 2023

View reviewed changes

keyboardDrummer previously approved these changes Oct 20, 2023

View reviewed changes

jtristan reviewed Oct 20, 2023

View reviewed changes

robin-aws mentioned this pull request Oct 20, 2023

Feature request: allowing consumers to customize opaqueness, intrinsic specifications, etc. #4697

Open

robin-aws added 3 commits October 20, 2023 09:57

Final PR feedback

2b1ee67

src/dafnystdlibs -> src/DafnyStdLibs

3297934

Merge branch 'master' of https://github.com/dafny-lang/dafny into sta…

ad5f6c4

…ndard-library-support-verification-only

robin-aws dismissed keyboardDrummer’s stale review via ad5f6c4 October 20, 2023 17:00

robin-aws changed the title ~~feat: Standard library support (verification only), DafnyStdLib.Wrappers (WIP)~~ feat: Standard library support (verification only), DafnyStdLib.Wrappers Oct 20, 2023

robin-aws changed the title ~~feat: Standard library support (verification only), DafnyStdLib.Wrappers~~ feat: Standard library support (verification only), DafnyStdLibs.Wrappers Oct 20, 2023

robin-aws changed the title ~~feat: Standard library support (verification only), DafnyStdLibs.Wrappers~~ feat: Standard library support (pre-verification only), DafnyStdLibs.Wrappers Oct 20, 2023

robin-aws changed the title ~~feat: Standard library support (pre-verification only), DafnyStdLibs.Wrappers~~ feat: Standard library support + DafnyStdLibs.Wrappers Oct 20, 2023

robin-aws enabled auto-merge (squash) October 20, 2023 17:07

robin-aws disabled auto-merge October 20, 2023 17:07

robin-aws enabled auto-merge (squash) October 20, 2023 17:08

jtristan approved these changes Oct 20, 2023

View reviewed changes

robin-aws added 2 commits October 20, 2023 10:48

Merge branch 'master' into standard-library-support-verification-only

128cea4

Merge branch 'master' into standard-library-support-verification-only

dd69cf8

robin-aws merged commit 38416f8 into master Oct 20, 2023

robin-aws deleted the standard-library-support-verification-only branch October 20, 2023 22:03

robin-aws mentioned this pull request Oct 23, 2023

Add dafny-lang/libraries Wrappers as first "standard library" #4641

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Standard library support + DafnyStdLibs.Wrappers #4678

feat: Standard library support + DafnyStdLibs.Wrappers #4678

robin-aws commented Oct 18, 2023 •

edited

Loading

keyboardDrummer Oct 20, 2023

keyboardDrummer Oct 20, 2023 •

edited

Loading

robin-aws Oct 20, 2023

MikaelMayer Oct 20, 2023

keyboardDrummer Oct 20, 2023

robin-aws Oct 20, 2023

keyboardDrummer Oct 20, 2023

keyboardDrummer Oct 20, 2023 •

edited

Loading

keyboardDrummer Oct 20, 2023

keyboardDrummer Oct 20, 2023

keyboardDrummer Oct 20, 2023

robin-aws Oct 20, 2023 •

edited

Loading

keyboardDrummer Oct 23, 2023

keyboardDrummer Oct 20, 2023 •

edited

Loading

robin-aws Oct 20, 2023

robin-aws Oct 20, 2023

keyboardDrummer Oct 20, 2023

robin-aws Oct 20, 2023

keyboardDrummer left a comment

jtristan Oct 20, 2023


		A `Result` carries both a success value and failure information, with two separate, specifiable types. Its use is then very similar to `Option`.

		### Combining different FC-types in expressions

feat: Standard library support + DafnyStdLibs.Wrappers #4678

feat: Standard library support + DafnyStdLibs.Wrappers #4678

Conversation

robin-aws commented Oct 18, 2023 • edited Loading

Description

How has this been tested?

Choose a reason for hiding this comment

keyboardDrummer Oct 20, 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 20, 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

robin-aws Oct 20, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Oct 20, 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

Choose a reason for hiding this comment

keyboardDrummer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws commented Oct 18, 2023 •

edited

Loading

keyboardDrummer Oct 20, 2023 •

edited

Loading

keyboardDrummer Oct 20, 2023 •

edited

Loading

robin-aws Oct 20, 2023 •

edited

Loading

keyboardDrummer Oct 20, 2023 •

edited

Loading