feat: import Unicode libraries #4780
Conversation
| @@ -10,6 +10,10 @@ DOO_FILE_ARITHMETIC_TARGET=binaries/DafnyStandardLibraries-arithmetic.doo | |||
|
|
|||
| all: check-binary test check-format check-examples | |||
|
|
|||
| verify: | |||
There was a problem hiding this comment.
Nice improvements! I had some of these as part of the FileIO import too, especially since the build will change per language too. I did find a slightly cleaner approach but I can apply that in my PR instead of insisting on it here.
|
|
||
| module Helpers { | ||
| import opened DafnyStdLibs.Wrappers | ||
| // TODO: consider tweaking /testContracts to support this use case better. |
There was a problem hiding this comment.
+1, and would prefer an issue to a TODO, but don't want to block on it
There was a problem hiding this comment.
I just copied this comment over from where Helpers was originally defined, but here's a new issue for it: #4786
| // This top-level module contains no definitions. | ||
| // It exists to enable import between child modules, | ||
| // and so that its doc comment appears in generated documentation. |
There was a problem hiding this comment.
This is a good point and too bad we can't do the same for the top level DafnyStdLibs module since it has to appear in multiple doo files. But could hopefully address that somehow in the future.
This PR imports the Unicode libraries from
dafny-lang/libraries.Notes:
dfyconfig.toml, as not all of the many false-positives can be resolved by rewriting existing proofs (as far as I can tell). We'll want to re-enable them in the future, for example if/when finer-grained control of such warnings is possible.DafnyStdLibsonly supports a single set of verification options right now, and we are proceeding with--unicode-char:true, theUnicodeStringsWithoutUnicodeCharmodule is not included in this PR.TODO:
Description
How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.