Pre-test of Dafny 4 #3466

davidcok · 2023-02-06T17:59:33Z

Changed the defaults for
--function-syntax to 4
--quantifier-syntax to 4
--unicode-char to true

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

robin-aws

Just got through Source for now, will tackle the rest separately.

Note that there will be other options changing defaults for 4.0, but those can be made after we fork the 4.x branch (which is where this PR will need to land once it's ready).

Source/DafnyCore/AST/Function.cs

robin-aws · 2023-02-22T18:19:45Z

Source/IntegrationTests/LitTests.cs

@@ -151,6 +151,7 @@ public class LitTests {
 [FileTheory]
 [FileData(Includes = new[] { "**/*.dfy", "**/*.transcript" },
 Excludes = new[] { "**/Inputs/**/*", "**/Output/**/*",
+ "**/libraries/**",


This shouldn't be necessary now that dafny-lang/libraries#97 is merged if we update the submodule pointer, right?

Well, it seemed odd that the CI tests should run lit on the library when there is a library nightly that runs anyway. So it seems they ought to be excluded here.

The original intention of adding the submodule was to ensure Dafny changes didn't break that code, so it's not the same as relying on that code testing itself as it evolves. I'm not 100% sure that makes sense and we could consider dropping it (i.e. we're moving towards testing against nightly Dafny releases to catch such breakages instead), but not as part of the scope of this PR.

OK - I'll push a commit that omits that exclusion.

Co-authored-by: Robin Salkeld <[email protected]>

See dafny-lang#3595

…cok-3459-dafny4test

robin-aws

Did at least a good spot check of all the test files and with the fixes I pushed to master already, they LGTM. Several nits but I think this is basically ready to merge with main-4.x once I create that.

Are there no other pieces of documentation that need to change for 4.0 as well, or were those already merged to master? We may need to relocate some so that we can still release 3.Last at the same time as 4.0.

robin-aws · 2023-02-22T23:31:40Z

docs/DafnyRef/Types.md

+A _Named Type_ is used to specify a user-defined type by a (possibly module- or class-qualified) name.
+Named types are introduced by


This isn't a Dafny 4.0 difference is it?

No - just a clarification.

Source/DafnyCore/AST/Function.cs

robin-aws · 2023-02-22T23:38:03Z

Test/DafnyTests/RunAllTestsOption.dfy

-// RUN: ! %baredafny test %args --no-verify --target:go "%s" >> "%t"
-// RUN: ! %baredafny test %args --no-verify --target:js "%s" >> "%t"
-// RUN: ! %baredafny test %args --no-verify --target:py "%s" >> "%t"
+// RUN: ! %baredafny test %args --unicode-char:false --no-verify --target:cs "%s" >> "%t"


Good change since #3608 adds a copy of this test that uses --unicode-char.

robin-aws · 2023-02-22T23:50:52Z

Test/DafnyTests/TestAttribute.dfy.README

+This test is failing at the moment.
+- It works locally
+- It fails in CI
+- I suspect it has something to do with dotnet test


Shoot, I should have deleted this file in my PR, will address separately

I'll take it out in these changes.

Feel free, but it should be taken out in 3.X anyway

robin-aws · 2023-02-22T23:51:46Z

Source/DafnyCore/DafnyOptions.cs

- public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version3;
- public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version3;
+ public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version4;
+ public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version4;


The new CLI option documentation still says "[default: Version3]" for me for some reason.

I'll investigate

When I compile in this branch I get [default: 4]. But found some places in help text to change -- pushed those commits also.

robin-aws · 2023-02-22T23:54:03Z

Test/git-issues/model

@@ -0,0 +1,859 @@
+*** MODEL


Accidental checkin?

I don't where this keeps coming from. I'll commit the removal.

robin-aws · 2023-02-22T23:54:47Z

Test/lit.site.cfg

+ # Unlimited errors (instead of just 5)
+ #'errorLimit:0',
+


Suggested change

# Unlimited errors (instead of just 5)

#'errorLimit:0',

# Unlimited errors (instead of just 5)

#'errorLimit:0',

Github won't take this suggestion. I'll add the newline manually. Actually there already is a blank line after.

Suggested change

# Unlimited errors (instead of just 5)

#'errorLimit:0',

Oops, I was actually trying to suggest removing commented out configuration. Or do you think it's helpful to leave this here for debugging?

OK. I removed it. It was not there before.

robin-aws · 2023-02-22T23:56:11Z

Test/lit.site.cfg

@@ -153,7 +156,7 @@ def buildCmd(args):

 dafny = addParams(buildCmd(dafnyArgs))

-standardArguments = addParams(' '.join(newDafnyArgs))
+standardArguments = addParams(' '.join([]))


Should these edits be in master as well?

I'll investigate (for a different PR)

robin-aws · 2023-02-22T23:58:21Z

docs/DafnyRef/Options.txt

@@ -103,8 +103,8 @@ Usage: dafny [ option ... ] [ filename ... ]
 ---- Language feature selection --------------------------------------------


We should end up with two other corresponding changes somehow too. We might want to more explicitly document what the default is for /functionSyntax and /quantifierSyntax in the legacy hooks.

OK. Options.txt is a generated file (that is then committed) -- only used in generating the pdf of the RefMan.

Yup I know, I was pointing out the fact that CI should have forced us to update it with changes for the other two options, which suggests that we didn't in fact update the /help output for them yet.

And when I did I had a failure for not having updated the documentation sources...

Co-authored-by: Robin Salkeld <[email protected]>

… into cok-3459-dafny4test

robin-aws

LGTM! Thanks so much for slogging through this. I pointed out a couple of things to clean up before merging but the actual content is good to go.

Only requesting changes because this needs to target the main-4.x branch you're cutting instead, ping me once that's changed and I'll actually approve.

robin-aws · 2023-02-23T17:33:24Z

.github/workflows/deep-tests.yml

+ push:
+ branches:
+ [ cok-3459-dafny4test ]


Suggested change

push:

branches:

[ cok-3459-dafny4test ]

.github/workflows/msbuild.yml

robin-aws · 2023-02-23T17:54:32Z

Source/DafnyCore/DafnyOptions.cs

 `predicate method`. Ghost functions are written `function` and
 `predicate`.
- 4 - Compiled functions are written `function` and `predicate`. Ghost
+ 4 (default) - Compiled functions are written `function` and `predicate`. Ghost


FYI I pushed a commit that does the same for /quantifierSyntax below as well

robin-aws · 2023-02-23T17:58:25Z

docs/DafnyRef/GrammarDetails.md

@@ -186,19 +186,26 @@ To aid in explaining the grammar we have added some additional productions
 that are not present in the original grammar. We name these with a trailing
 underscore. Inlining these where they are referenced will reconstruct the original grammar.

-### 17.2.1. Programs ([discussion](#sec-program)) {#g-program}
+<!-- A note on formatting the sections below: LaTex renders the 'discussion' link in line with the heading for level-4 and higher headings.


Just flagging all these edits as relevant for master as well, but I can live with them only in main-4.x if too much of a pain to separate out.

I'll port them over to master separately

robin-aws · 2023-02-23T18:16:28Z

One other thing, we need to update the various pull_request triggers in the GitHub Actions workflows to also trigger on main-* branches. It's probably simplest to do that here, and we might even back-port that change to master to further minimize differences.

Co-authored-by: Robin Salkeld <[email protected]>

… into cok-3459-dafny4test

davidcok added 30 commits August 23, 2022 20:57

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

d78800a

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

dc2f742

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

8b4e194

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

c292bae

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

50702f8

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

c49f8a3

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

9c68747

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

aee08f5

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

6bba113

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

032e12a

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

e11fd63

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

24921df

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

2e3a81f

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

91e05eb

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

ba9f954

Checking included files

47815c1

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

956e476

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

5aa1aa9

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

834cee3

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

f6b3d49

Merge branch 'cok-quicktest' of https://github.com/davidcok/dafny

977b36a

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

043986b

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

710f269

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

ea10461

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

09591e8

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

408f44e

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

02ffee4

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

c99fbe9

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

f4d4a02

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

448cb44

Merge conflicts

5c617ad

robin-aws reviewed Feb 22, 2023

View reviewed changes

davidcok and others added 4 commits February 22, 2023 13:34

More merge conflicts

62d093e

Update Source/DafnyCore/AST/Function.cs

8047d5d

Co-authored-by: Robin Salkeld <[email protected]>

Redirect stderr of dotnet test instead of stdout

6fd4587

See dafny-lang#3595

Merge branch 'cok-3459-dafny4test' of github.com:davidcok/dafny into …

1ff157b

…cok-3459-dafny4test

robin-aws mentioned this pull request Feb 22, 2023

Change default values of CLI options for Dafny 4.0 #2548

Closed

restoring the checking of libraries

4a24c94

robin-aws reviewed Feb 23, 2023

View reviewed changes

davidcok and others added 10 commits February 22, 2023 19:11

Update Source/DafnyCore/AST/Function.cs

dd1f1bf

Co-authored-by: Robin Salkeld <[email protected]>

Review comments

762cd1d

Merge branch 'cok-3459-dafny4test' of https://github.com/davidcok/dafny…

633fba7

… into cok-3459-dafny4test

Merge branch 'master' into cok-3459-dafny4test

4154190

Review changes

9d0de26

Fixing some rendering problems

9f19eb5

Removing commented out errorLimit

19d8a1b

Updating Options.txt

abf92f0

Adapting back to old library

ff44dba

Updating default marker for quantifierSyntax in /help

7d5ca09

robin-aws requested changes Feb 23, 2023

View reviewed changes

davidcok and others added 7 commits February 23, 2023 13:48

Update .github/workflows/msbuild.yml

ce35ed9

Co-authored-by: Robin Salkeld <[email protected]>

Edits in prep for main-4

02424d3

Merge branch 'cok-3459-dafny4test' of https://github.com/davidcok/dafny…

57ea87e

… into cok-3459-dafny4test

Updating Options.txt for changes in defaults

06268fe

Updating Options.txt for changes in defaults

a78ba11

Merge conflicts

81cb497

Merge branch 'master' into cok-3459-dafny4test

762cf11

davidcok closed this Mar 8, 2023

davidcok deleted the cok-3459-dafny4test branch March 8, 2023 21:32

		A _Named Type_ is used to specify a user-defined type by a (possibly module- or class-qualified) name.
		Named types are introduced by

		@@ -103,8 +103,8 @@ Usage: dafny [ option ... ] [ filename ... ]
		---- Language feature selection --------------------------------------------

Pre-test of Dafny 4 #3466

Pre-test of Dafny 4 #3466

Conversation

davidcok commented Feb 6, 2023

robin-aws left a 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

robin-aws left a 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

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

Choose a reason for hiding this comment

robin-aws left a 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

robin-aws commented Feb 23, 2023