dafny-lang / dafny.msbuild Goto Github PK

Since this tool is currently invoking the Dafny CLI rather than depending on it directly as a .NET package, it would be useful to check that the provided Dafny CLI is a compatible version.

This can be either:

1. A release identifier such as "2.3.0.10506", or
2. A git reference ("HEAD", v2.3.0, a commit hash, etc.)

The second option would only be satisfied when running Dafny from a local git repository clone.

This would be helpful for identifying outliers that take a long time to verify, especially when they are approaching the timeout and about to make future changes hit unexpected delays.

Every once in a while a file will fail but with apparently successful output from the Dafny CLI:

938 | Verifying ../src/Util/Sets.dfy failed:
939 | Dafny 2.3.0.10506
940 |  
941 | Dafny program verifier finished with 1 verified, 0 errors

Most of the time, even if you fail to verify a file, you'd like to see the verification results of the rest of the files in scope.

This package is currently published under my own Microsoft Live account:

https://www.nuget.org/packages/dafny.msbuild/

We should create a group for Dafny and transfer ownership.

Not sure if this is possible, but it would be great to hook into a standard build phase instead of a custom task that can only be run from the command line AFAICT.

See https://docs.microsoft.com/en-us/visualstudio/code-quality/code-analysis-for-managed-code-overview?view=vs-2019

Now that we published Dafny as a dotnet tool, it would be good to use it unless an option says otherwise.
That way, we would be able to use it for Dafny development as well without having a circularity problem.

This appears to be a regression or something environment-sensitive, since the task used to default to the number of logical cores.ParallelOptions seems to intentionally default to maximum parallelism according to the source code, so perhaps this changed with a dependency upgrade somehow.

Pure Dafny projects should be able to take advantage of this without assuming the build process uses msbuild/dotnet. The VerifyDafny task should be able to just provide the list of source files to the CLI.

This is an enhancement request to memoize the fact that a file has been verified somehow, so that subsequent executions of the VerifyDafny task don't waste time re-verifying it unless the file is modified.

Doing this correctly will probably require adding a feature to Dafny itself to determine the dependency graph of Dafny files, so that this "cache" can be correctly invalidated.

The build is currently only verifying different use cases pass, but it should also:

• Verify that passing -p:VerifyDafnyJobs=1 results in deterministic, sequential verification
• Verify correct behaviour if at least one file fails to verify
• Verify the /timeLimit parameter is being provided correctly (perhaps by including a file that is very slow to verify)

Perhaps we can use lit to define and compare against the expected dotnet commands' output?

Necessary to support depending on separate Dafny packages.

For reproducible builds, we should allow the configuration of what version of Dafny should be used to build/verify the project.