chore: xUnit-based lit test runner #680
There are no files selected for viewing
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
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -30,6 +30,7 @@ Package/ | |
|
|
||
| Source/*/bin/ | ||
| Source/*/obj/ | ||
| Source/*/bin_core/ | ||
| Source/*/obj_core/ | ||
| Source/packages | ||
|
|
||
|
|
||
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
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
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
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
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
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
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
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
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
File renamed without changes.
File renamed without changes.
File renamed without changes.
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,43 @@ | ||
| <Project Sdk="Microsoft.NET.Sdk"> | ||
|
|
||
| <PropertyGroup> | ||
| <TargetFramework>net5.0</TargetFramework> | ||
| <GenerateEmbeddedFilesManifest>true</GenerateEmbeddedFilesManifest> | ||
| <IsPackable>false</IsPackable> | ||
| </PropertyGroup> | ||
|
|
||
| <ItemGroup> | ||
| <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.9.4" /> | ||
| <PackageReference Include="xunit" Version="2.4.1" /> | ||
| <PackageReference Include="xunit.runner.visualstudio" Version="2.4.3"> | ||
| <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets> | ||
| <PrivateAssets>all</PrivateAssets> | ||
| </PackageReference> | ||
| <PackageReference Include="coverlet.collector" Version="3.0.2"> | ||
| <IncludeAssets>runtime; build; native; contentfiles; analyzers; buildtransitive</IncludeAssets> | ||
| <PrivateAssets>all</PrivateAssets> | ||
| </PackageReference> | ||
| </ItemGroup> | ||
|
|
||
| <ItemGroup> | ||
| <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" /> | ||
| <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" /> | ||
| <ProjectReference Include="..\XUnitExtensions\XUnitExtensions.csproj" /> | ||
| </ItemGroup> | ||
|
|
||
| <ItemGroup> | ||
| <Content Include="..\..\Binaries\z3\**\*.*" LinkBase="z3"> | ||
| <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory> | ||
| </Content> | ||
| <Content Include="..\..\Test\**\*.*" LinkBase="TestFiles\LitTests\LitTest"> | ||
| <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory> | ||
| </Content> | ||
| <Content Include="..\..\docs\DafnyRef\examples\**\*.*" LinkBase="TestFiles\LitTests\LitTest\refman\examples"> | ||
| <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory> | ||
| </Content> | ||
| <Content Include="..\..\node_modules\**\*.*" LinkBase="TestFiles\LitTests\LitTest\node_modules"> | ||
| <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory> | ||
| </Content> | ||
| </ItemGroup> | ||
|
|
||
| </Project> |
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,98 @@ | ||
| using System; | ||
| using System.Collections.Generic; | ||
| using System.IO; | ||
| using System.Linq; | ||
| using System.Reflection; | ||
| using System.Runtime.InteropServices; | ||
| using Microsoft.Dafny; | ||
| using Xunit; | ||
| using Xunit.Abstractions; | ||
| using XUnitExtensions; | ||
| using XUnitExtensions.Lit; | ||
|
|
||
| [assembly: TestCollectionOrderer("XUnitExtensions.TestCollectionShardFilter", "XUnitExtensions")] | ||
|
|
||
| namespace IntegrationTests { | ||
| public class LitTests { | ||
|
|
||
| private static readonly Assembly dafnyDriverAssembly = typeof(DafnyDriver).Assembly; | ||
| private static readonly Assembly dafnyServerAssembly = typeof(Server).Assembly; | ||
|
|
||
| private static readonly string[] defaultDafnyArguments = new[] { | ||
| "/countVerificationErrors:0", | ||
|
|
||
| // We do not want absolute or relative paths in error messages, just the basename of the file | ||
| "/useBaseNameForFileName", | ||
|
|
||
| // We do not want output such as "Compiled program written to Foo.cs" | ||
| // from the compilers, since that changes with the target language | ||
| "/compileVerbose:0", | ||
|
|
||
| // Hide Boogie execution traces since they are meaningless for Dafny programs | ||
| "/errorTrace:0", | ||
|
|
||
| // Set a default time limit, to catch cases where verification time runs off the rails | ||
| "/timeLimit:300" | ||
| }; | ||
|
|
||
| private static ILitCommand MainWithArguments(Assembly assembly, IEnumerable<string> arguments, LitTestConfiguration config, bool invokeDirectly) { | ||
| return MainMethodLitCommand.Parse(assembly, arguments, config, invokeDirectly); | ||
| } | ||
|
|
||
| private static readonly LitTestConfiguration CONFIG = new() { | ||
| Commands = new Dictionary<string, Func<IEnumerable<string>, LitTestConfiguration, ILitCommand>> { | ||
| { "%baredafny", (args, config) => | ||
| MainWithArguments(dafnyDriverAssembly, args, config, false) }, | ||
| { "%dafny", (args, config) => | ||
| MainWithArguments(dafnyDriverAssembly, defaultDafnyArguments.Concat(args), config, false) }, | ||
| { "%server", (args, config) => | ||
| MainWithArguments(dafnyServerAssembly, args, config, false) }, | ||
| }, | ||
|
|
||
| Substitions = new Dictionary<string, string> { | ||
| { "%diff", "diff" }, | ||
| { "%binaryDir", "." }, | ||
| { "%z3", Path.Join("z3", "bin", "z3") }, | ||
| { "%refmanexamples", Path.Join("TestFiles", "LitTests", "LitTest", "refman", "examples") } | ||
| }, | ||
|
|
||
| PassthroughEnvironmentVariables = new[] { "PATH", "HOME" }, | ||
| }; | ||
|
|
||
| static LitTests() { | ||
| var dafnyReleaseDir = Environment.GetEnvironmentVariable("DAFNY_RELEASE"); | ||
| if (dafnyReleaseDir != null) { | ||
| CONFIG.Commands["%baredafny"] = (args, config) => | ||
| new ShellLitCommand(config, Path.Join(dafnyReleaseDir, "dafny"), args, config.PassthroughEnvironmentVariables); | ||
| CONFIG.Commands["%dafny"] = (args, config) => | ||
| new ShellLitCommand(config, Path.Join(dafnyReleaseDir, "dafny"), defaultDafnyArguments.Concat(args), config.PassthroughEnvironmentVariables); | ||
| CONFIG.Commands["%server"] = (args, config) => | ||
| new ShellLitCommand(config, Path.Join(dafnyReleaseDir, "DafnyServer"), args, config.PassthroughEnvironmentVariables); | ||
| CONFIG.Substitions["%z3"] = Path.Join(dafnyReleaseDir, "z3", "bin", "z3"); | ||
| } | ||
|
|
||
| if (RuntimeInformation.IsOSPlatform(OSPlatform.Linux)) { | ||
| CONFIG.Features = new[] { "ubuntu", "posix" }; | ||
| } else if (RuntimeInformation.IsOSPlatform(OSPlatform.Windows)) { | ||
| CONFIG.Features = new[] { "windows" }; | ||
| } else if (RuntimeInformation.IsOSPlatform(OSPlatform.OSX)) { | ||
| CONFIG.Features = new[] { "macosx", "posix" }; | ||
| } else { | ||
| throw new Exception($"Unsupported OS: {RuntimeInformation.OSDescription}"); | ||
| } | ||
| } | ||
|
|
||
| private readonly ITestOutputHelper output; | ||
|
|
||
| public LitTests(ITestOutputHelper output) { | ||
| this.output = output; | ||
| } | ||
|
|
||
| [FileTheory] | ||
| [FileData(Includes = new[] { "**/*.dfy", "**/*.transcript" }, | ||
| Excludes = new[] { "**/Inputs/**/*", "refman/examples/**/*" })] | ||
|
There was a problem hiding this comment. I had a few output files from a previous run that were accidentally picked up as Lit tests, for example this one:
There was a problem hiding this comment. Right, lit automatically filters out Output files internally. I've addressed this by adding another Ideally it would be automatic, but another improvement I want to make after this PR is to run each test in a fresh temporary directory instead of a fixed and shared |
||
| public void LitTest(string path) { | ||
| LitTestCase.Run(path, CONFIG, output); | ||
| } | ||
| } | ||
| } | ||
Oops, something went wrong.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If this is not working, try
Expand-Archive -LiteralPath z3.zip -DestinationPath Binaries/z3
https://docs.microsoft.com/en-us/powershell/module/microsoft.powershell.archive/expand-archive?view=powershell-7.1
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the suggestion @MikaelMayer! I did eventually get it working in the later commits, but there's probably still a better approach so let me know if I can improve it.