chore: Factor out projects without runtimes #2568

robin-aws · 2022-08-09T18:31:50Z

Factors out two new projects that don't depend on the DafnyRuntime project or DafnyRuntime.* runtime artifacts, and removes the DLL-level dependencies on DafnyRuntime.dll. It also has the happy side-effect of making directory, csproj, and assembly names consistent.

The four main changes are:

Rename Dafny folder/DafnyPipeline project to DafnyCore, remove reference to DafnyRuntime and DafnyRuntime.* embedded resources
Create new DafnyPipeline folder/project, referencing DafnyCore and adding DafnyRuntime.* embedded resources
- Note DafnyPipeline.dll does NOT depend on DafnyRuntime.dll, however! It has a project-level dependency to ensure DafnyRuntime is built first, but only embeds the runtime artifacts.
Relabel DafnyDriver as DafnyDriver.dll instead of Dafny.dll, remove reference to DafnyRuntime
- I'll be able to use this entry point to build Dafny source code into the runtimes when implementing Implement lazy sequence concatenation in remaining backends #2390
Create new Dafny folder/project, referencing DafnyDriver and DafnyPipeline (and hence pulling in embedded runtimes)

Note that we are still only publishing Dafny.dll and DafnyPipeline.dll as Nuget packages, and they still transitively contain the same content. We could publish DafnyDriver and/or DafnyCore in the future as well.

Removing DafnyRuntime as a DLL dependency from all of these projects initially caused the Test/dafny0/DafnyLibClient.dfy test to break. This is because the driver was attempting to Assembly.Load each DLL passed to it, in order to read any DafnySourceAttribute value out of it if present. This has never been a good idea, since an arbitrary DLL will have dependencies not satisfied by the invoking context, and not finding DafnyRuntime.dll was just one potential error this could cause. I had previously used Cecil to read DLL files without loading them, but this was lost when we moved to .NET Core v2 since that library was not supported. This time I've used the built-in System.Reflection.Metadata.MetadataReader and related types to decode enough of the DLL to read this attribute.

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

* Rename Dafny folder/DafnyPipeline project to DafnyCore, remove reference to DafnyRuntime and DafnyRuntime.* embedded resources * Create new DafnyPipeline folder/project, referencing DafnyCore and adding DafnyRuntime.* embedded resources * Relabel DafnyDriver as DafnyDriver.dll instead of Dafny.dll, remove reference to DafnyRuntime * Create new Dafny folder/project, referencing DafnyDriver and DafnyPipeline (and hence pulling in embedded runtimes)

…projects-without-runtimes

atomb

This is a very nice improvement. :) I noticed a few tiny things that could be fixed (which should fix at least one of the test failures) but it otherwise seems great.

atomb · 2022-08-09T19:57:44Z

Makefile

@@ -29,12 +29,12 @@ z3-ubuntu:
 mv z3-4.8.5-x64-ubuntu-16.04 ${DIR}/Binaries/z3

 format:
- dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude Dafny/Scanner.cs --exclude Dafny/Parser.cs
+ dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs

 clean:
 (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin )


This line should perhaps be updated to include DafnyCore, too?

atomb · 2022-08-09T19:58:10Z

Makefile


 clean:
 (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin )
 (cd ${DIR} ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
- make -C ${DIR}/Source/Dafny -f Makefile clean
+ make -C ${DIR}/Source/DafnyCore -f Makefile clean
 (cd ${DIR}/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
 make -C ${DIR}/docs/DafnyRef clean
 (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin )


Same as for the previous rm line.

atomb · 2022-08-09T20:04:32Z

Source/DafnyCore/Compilers/Compiler-java.cs

- }
+ var fullJarName = $"{targetDirectory}/{jarName}";
+ FileStream outStream = new FileStream(fullJarName, FileMode.Create, FileAccess.Write);
+ stream!.CopyTo(outStream);


This change has the side effect of creating an empty JavaRuntime.jar if it's not found in the assembly, as opposed to doing nothing, which is perhaps better behavior? It might be even nicer to emit an error message in that case, but I didn't do that in the original code, either. :)

Ah my intention was just to cleanly make this an exception rather than a silent failure, but I can throw right away without that messy side effect.

Note that I'm going to make it an exception rather than an error message as SinglePassCompiler.ReadRuntimeSystem does (and I intend to make that throw as well in the next PR). At least right now, the publicly released tools should always have the runtimes attached, so I'd rather crash loudly if we've made a publishing mistake.

In fact I'm touching SinglePassCompiler.ReadRuntimeSystem already anyway, I'm going to make it throw in this PR after all - no time like the present!

atomb · 2022-08-09T20:06:27Z

Source/DafnyDriver/DafnyDriver.csproj

@@ -1,18 +1,14 @@
 <Project Sdk="Microsoft.NET.Sdk">

 <PropertyGroup>
- <OutputType>Exe</OutputType>
- <AssemblyName>Dafny</AssemblyName>
+ <OutputType>Library</OutputType>


One nice impact of this is that a client can now get all of Dafny as a library (though only conveniently if we publish this library to NuGet).

Yes, and I think I'm going to have to define an additional "DafnyWithoutRuntimes" Exe project that depends on this in order to run Dafny on my DafnyRuntime.dfy code in the next PR. My intent remains to keep this and that project internal-only for now though.

atomb · 2022-08-09T20:15:41Z

Source/IntegrationTests/IntegrationTests.csproj

@@ -21,8 +21,7 @@
 </ItemGroup>

 <ItemGroup>
- <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" />
- <ProjectReference Include="..\DafnyRuntime\DafnyRuntime.csproj" />


Based on the test output, it seems that this project still depends dynamically on DafnyRuntime.

Specific tests are depending on linking to DafnyRuntime.dll, yup. Unfortunately one of them reveals that DafnyMain calls Assembly.LoadFile on any dll file passed to the CLI, in order to read the contents of any DafnySourceAttribute: https://github.com/dafny-lang/dafny/blob/master/Source/Dafny/DafnyMain.cs#L67. This will fail if its dependencies are not available (DafnyRuntime.dll or any other dependency!).

I originally fixed this by loading the assembly reflectively using Cecil, but unfortunately we lost that when switching to .NET Core: https://github.com/dafny-lang/dafny/pull/794/files#diff-0ba2e4842e187b0efcf6a6b5fd6fca73b546ece27e54074265eab734f826240dL45-R47. Even better, there's an Assembly.ReflectionOnlyLoad method, but it turns out it always did a regular load instead, and now always throws an exception instead (which is definitely better, but still feels like a bait-and-switch :P )

Eventually figured out the supported replacement for Assembly.ReflectionOnlyLoad - see updated PR description and release note.

…projects-without-runtimes

MikaelMayer · 2022-08-10T19:17:48Z

Source/DafnyCore/DafnyCore.csproj

@@ -30,36 +29,8 @@
 <PackageReference Include="Boogie.ExecutionEngine" Version="2.15.7" />
 </ItemGroup>

- <ItemGroup>
- <ProjectReference Include="..\DafnyRuntime\DafnyRuntime.csproj" />


I'm fine removing the reference to the DafnyRuntime, however, in one of my PRs, I am making use of the DafnyRuntime.cs which should then become a dependency of DafnyCore in your setting. Can we just add an external dependency to this file so that it's included at compile time?
That was we don't need a dependency of all the possible runtimes as you suggest but I have still it working for us.

Your PR will actually work just fine after this change. Since you're not passing /useRuntimeLib when compiling your Dafny code through dafny.msbuild, the compiled output will have the embedded DafnyRuntime.cs file prepended, and you won't need to depend on DafnyRuntime.dll.

That means that the version of the runtime you build your part of DafnyCore with doesn't affect the version that a dafny end user will end up depending on in their compiled code. It's admittedly a little weird and confusing to have the C# runtime code embedded like that though. :)

Oh I see, it's in the generated code. That's fine I think ^^

keyboardDrummer · 2022-08-11T11:34:48Z

Source/DafnyDriver/DafnyDriver.csproj

@@ -1,18 +1,14 @@
 <Project Sdk="Microsoft.NET.Sdk">


From the PR description:

Relabel DafnyDriver as DafnyDriver.dll instead of Dafny.dll, remove reference to DafnyRuntime
I'll be able to use this entry point to build Dafny source code into the runtimes when implementing #2390

Why do you need this project? Can't you use DafnyCore instead? Are you planning on setting the output type here to Exe again so you can run it?

I'm planning on adding an empty Exe project that references DafnyDriver, something like DafnyWithoutRuntimes, so I can easily invoke the Dafny compiler from something like a Makefile. I don't know of any way to invoke logic in DafnyCore directly, but I'd be happier if there was!

…projects-without-runtimes # Conflicts: # RELEASE_NOTES.md # Source/DafnyCore/DafnyCore.csproj # Source/DafnyDriver/DafnyDriver.csproj # Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs # Source/version.cs

…projects-without-runtimes

atomb

This looks good! I had a couple of questions that could lead to changes, but I'm approving it to avoid delay in the (likely) case where they don't require any.

atomb · 2022-09-09T00:25:21Z

Source/Dafny/Dafny.csproj

+
+ <ItemGroup>
+ <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" />
+ <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />


Does this need DafnyPipeline?

Absolutely, since that's how the runtime files are included. I understand why you ask, because the minimal contents of Dafny should just be DafnyDriver + runtimes, but DafnyPipeline is exactly the assembly that embeds the runtimes. Most importantly the compilers load them from the DafnyPipeline.dll assembly explicitly rather than whatever the currently executing assembly is.

Right, of course!

atomb · 2022-09-09T00:34:58Z

Source/DafnyCore/DafnyMain.cs

+ }
+
+ private static string GetDafnySourceAttributeText(string dllPath) {
+ using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite);


Does this result in a reasonable error if dllPath is a non-existent file? Or does the earlier code in DafnyFile ensure that it exists?

Good callout! It's no worse than the old version that tried to Assembly.LoadFile it: you still get a System.IO.FileNotFoundException, just with a slightly different stack trace.

It's worth making that cleaner since it's a user error that shouldn't lead to a crash, but it may be non-trivial to fix. Throwing IllegalDafnyFile will probably lead to a different less helpful error so it may need some refactoring. I cut #2719 as a follow up.

robin-aws added 15 commits August 5, 2022 10:22

Updating several paths referring to DafnyDriver or DafnyPipeline

83244db

Fix customBoogie.patch

21ad5c0

Missed a reference

bd4504c

Fix more project references

7e72c50

Add reference to runtime project (sigh)

95906d4

fix Makefile

49790ad

Fix package.py

b33ae97

Fix EmitRuntimeJar too

e361483

More project reference fixes

0a001b2

Whitespace (and fix paths in workflow to check it)

9ab70d8

Fixing plugin tests

3b5f007

A few more unit test fixes

581f719

Break DLL dependency on DafnyRuntime, fix TestDafny

bbdc8c3

Merge branch 'master' of github.com:dafny-lang/dafny into factor-out-…

0872013

…projects-without-runtimes

robin-aws requested review from atomb and MikaelMayer August 9, 2022 19:53

atomb requested changes Aug 9, 2022

View reviewed changes

robin-aws added 7 commits August 10, 2022 07:16

Don’t Assembly.Load to get DafnySourceAttribute contents

e614f50

Throw exception cleanly if runtime resource files are missing

37cc1b0

Update Makefile

981ff3f

Fixing test broken by not depending on DafnyRuntime.dll

45a32b0

Add DafnyRuntime.dll to IntegrationTests

59051c0

Added release note about not loading DLLs

d3d645c

Merge branch 'master' of github.com:dafny-lang/dafny into factor-out-…

1ad39ae

…projects-without-runtimes

MikaelMayer reviewed Aug 10, 2022

View reviewed changes

Whitespace

76cb8a5

keyboardDrummer reviewed Aug 11, 2022

View reviewed changes

robin-aws added 2 commits September 7, 2022 16:05

Delete Dafny-generated files that snuck in from a different branch

c5ab527

robin-aws added 9 commits September 7, 2022 16:15

And these too

0c25cce

Moving new files since merge over

b2636d9

Fix bad merge

d7c85bd

Merge branch 'master' of github.com:dafny-lang/dafny into factor-out-…

8d6aab6

…projects-without-runtimes

Need to explicitly include DafnyRuntime.dll in release package

cfb268c

Poke CI

fcaa3a7

Don’t publish DafnyCore and DafnyDriver to Nuget (yet)

1e697f3

Merge branch 'master' of github.com:dafny-lang/dafny into factor-out-…

e17d7d5

…projects-without-runtimes

Move new files to DafnyCore

27ca0bb

robin-aws marked this pull request as ready for review September 8, 2022 19:37

atomb approved these changes Sep 9, 2022

View reviewed changes

robin-aws merged commit 7fc07d3 into dafny-lang:master Sep 9, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: Factor out projects without runtimes #2568

chore: Factor out projects without runtimes #2568

robin-aws commented Aug 9, 2022 •

edited

Loading

atomb left a comment

atomb Aug 9, 2022

atomb Aug 9, 2022

atomb Aug 9, 2022

robin-aws Aug 9, 2022

robin-aws Aug 9, 2022

atomb Aug 9, 2022

robin-aws Aug 9, 2022

atomb Aug 9, 2022

robin-aws Aug 9, 2022

robin-aws Aug 10, 2022

MikaelMayer Aug 10, 2022

robin-aws Aug 10, 2022

MikaelMayer Aug 10, 2022

keyboardDrummer Aug 11, 2022

robin-aws Sep 7, 2022

atomb left a comment

atomb Sep 9, 2022

robin-aws Sep 9, 2022

atomb Sep 9, 2022

atomb Sep 9, 2022

robin-aws Sep 9, 2022 •

edited

Loading

chore: Factor out projects without runtimes #2568

chore: Factor out projects without runtimes #2568

Conversation

robin-aws commented Aug 9, 2022 • edited Loading

atomb 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

atomb 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 Sep 9, 2022 • edited Loading

Choose a reason for hiding this comment

robin-aws commented Aug 9, 2022 •

edited

Loading

robin-aws Sep 9, 2022 •

edited

Loading