Enable packaging Dafny as a .NET tool #2051

atomb · 2022-04-22T17:52:04Z

This makes the first steps toward packaging Dafny as a .NET CLI tool.

Mostly fixes #1779, but doesn't yet auto-install Z3. We can do that as part of a later PR.

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

mschlaipfer · 2022-04-22T18:08:34Z

What about the target language runtimes and supporting the /compile:3 argument? How is that different from z3? Is it because the default is not /noVerify so z3 is required whereas the target compilers are optional?

atomb · 2022-04-22T18:23:47Z

What about the target language runtimes and supporting the /compile:3 argument? How is that different from z3? Is it because the default is not /noVerify so z3 is required whereas the target compilers are optional?

That's a good question. I think the idea is that all the target language runtimes would be available through the packaging system for the respective languages (and the C# runtime is prepared to be available through NuGet, so C# compilation and execution should work smoothly).

Alternatively, I expect the source files for the target language runtimes could be included as data files in the Dafny package, and spit out alongside the generated code (as I think would be necessary for C++?). They're at least not platform-dependent, whereas Z3 binaries are.

robin-aws · 2022-04-22T19:28:51Z

Alternatively, I expect the source files for the target language runtimes could be included as data files in the Dafny package, and spit out alongside the generated code (as I think would be necessary for C++?).

This is the approach we should use for now, including the DafnyRuntime.cs file even if/when it's possible to get the DafnyRuntime.dll artifact from nuget. The default behavior is still to prepend that code to the compiler output anyway.

I'm assuming that dotnet tool install --global ... works as well? That's how I'll want to document the common installation process for users, as that will add the dafny CLI to the PATH so you don't need the dotnet tool run ... part.

Commented-out code also exists to upload them, but we need to configure an API key first.

fabiomadge · 2022-06-07T19:57:55Z

.github/workflows/publish-release.yml

+ #- name: Upload package to NuGet
+ # run: dotnet nuget push "Binaries/Dafny*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json


Suggested change

#- name: Upload package to NuGet

# run: dotnet nuget push "Binaries/Dafny*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json

- name: Upload package to NuGet

run: dotnet nuget push "Binaries/Dafny*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json

fabiomadge · 2022-06-07T20:22:23Z

Source/Dafny/DafnyPipeline.csproj

+ <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntime.csproj">
+ <LogicalName>DafnyRuntime.csproj</LogicalName>
+ </EmbeddedResource>


Would this also work if done in DafnyRuntime?

The DafnyPipeline project doesn't depend on the DafnyRuntime project, so I don't think we'd be able to get the files into the executable assembly that way. The DafnyRuntime project is, as I understand it, something that generated C# code can depend on, but not something the compiler includes in its code base at all.

Would adding that dependency be so bad?

It seems like it would be sort of a strange thing to do, to me. The DafnyRuntime project is a C# library intended for use by generated C# code. It doesn't make sense to me for it include, for instance, DafnyRuntime.js as an embedded resource. Said differently, it makes more sense, in my view, for the compiler to bake in the code for the various runtime systems, rather than having the runtime system for one language include the runtime systems for other languages.

And why do you need the csproj file itself inside the DLL? What is reading that exactly?

I think we should either get rid of the csproj entirely, or use it as much as possible.

Another way to look at it: if we embed those files in DafnyRuntime.csproj, then the DafnyRuntime.dll file that users download from NuGet to link with their generated C# code will also include the text of the various other language runtimes. It wouldn't cause problems to do that, but it seems awkward to me.

I think we should have separate projects for each back-end, and each of those should include their own runtime, and then , not DafnyPipeline but DafnyDriver.csproj should reference those. That way, consumers of Dafny as a library will consume DafnyPipeline but not necessarily all the back-ends and runtimes, while Dafny tool consumers do get all the back-ends. One example we have of a Dafny as a library consumer is DafnyLanguageServer. In the proposed setup, you can build DafnyLanguageServer without having Java instead because there's no dependency on DafnyRuntime.csproj.

Keeping DafnyRuntime.csproj as is, the above proposal turns into DafnyDriver.csproj referencing DafnyRuntime.csproj.

Yeah, I like the main proposal you're making, @keyboardDrummer. Each back-end should be a separate project.

Given the current state of the code, though, the reason for embedding those resources in DafnyPipeline for the moment is so that the compilers can get a reference to them through GetExecutingAssembly. I originally put them in DafnyDriver. It would be possible to move them back into DafnyDriver and instead use GetEntryAssembly.

I had previously only seen methods in the Assembly class to load by type, and types in DafnyRuntime aren't available in the compilers, which are currently in DafnyPipeline, unless we make DafnyRuntime a dependency of DafnyPipeline, which is pretty much the opposite of what you're proposing. We could potentially use Load to load DafnyRuntime by name. I prefer something that doesn't require a name as a string, but not strongly.

I see, sorry I didn't see the GetExecutingAssembly call. In that case I think adding DafnyRuntime as a dependency to DafnyPipeline is OK for now.

fabiomadge

How did we deal with z3?

atomb · 2022-06-07T20:38:38Z

How did we deal with z3?

The current plan is to have it be an implicit dependency that must be installed separately for the moment, but perhaps to add functionality to automatically download it at some point in the future.

robin-aws

Today is a great day for Dafny. :)

Mostly just questions, but one other blocker: we need a copy of release-downloads.yml that installs the .NET tool version and runs the same smoke test. I don't see an easy way of triggering that automatically, so we should just make it a manual step of the release process for now.

robin-aws · 2022-06-07T21:02:13Z

RELEASE_NOTES.md

@@ -1,6 +1,7 @@
 # Upcoming

 - feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified.
+- feat: Dafny is now available on NuGet, installable with `dotnet tool install Dafny`.


Suggested change

- feat: Dafny is now available on NuGet, installable with `dotnet tool install Dafny`.

- feat: Dafny is now available on NuGet, installable with `dotnet tool install --global Dafny`.

Debatable perhaps, but it seems like the most common use case by far is putting it on your PATH so you can just run dafny on the command line.

I would also be more specific about the set of packages we're publishing than just "Dafny" :)

robin-aws · 2022-06-07T21:02:47Z

Source/Dafny/Compilers/Compiler-go.cs

- var rt = wr.NewFile("dafny/dafny.go");
- ReadRuntimeSystem("DafnyRuntime.go", rt);


Why did this have to move?

Because it now depends on program which isn't in scope in EmitBuiltinDecls but is in EmitHeader. And changing the parameters of EmitBuiltinDecls would require changes to every compiler. The other compilers read the runtimes in EmitHeader, too, so it's more consistent that way.

You could argue that EmitBuiltinDecls is the right place for them all to emit the runtime system, though.

robin-aws · 2022-06-07T21:06:46Z

RELEASE.md

+ x.y.z.40112). Edit the internal version number in the following
+ places:
+
+ * `Source/version.cs`


I'd add a comment to this file noting that the other two instances have to be kept in sync, just in case.

Good thought.

robin-aws · 2022-06-07T21:17:39Z

Source/Dafny/DafnyPipeline.csproj

+ <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntime.csproj">
+ <LogicalName>DafnyRuntime.csproj</LogicalName>
+ </EmbeddedResource>


And why do you need the csproj file itself inside the DLL? What is reading that exactly?

keyboardDrummer · 2022-06-08T08:50:21Z

Source/DafnyLanguageServer/DafnyLanguageServer.csproj

@@ -8,6 +8,7 @@
 <RootNamespace>Microsoft.Dafny.LanguageServer</RootNamespace>
 <OutputPath>..\..\Binaries\</OutputPath>
 <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
+ <PackageVersion>3.6.0.40511</PackageVersion>


What's the use of publishing this as a package? I think it could be useful as a too, either a separate tool or part of the one dafny tool (preferred), so that the VSCode extension can install it using dotnet install tool dafny

Do you know whether it's possible to set it up so that the language server gets distributed along with the main CLI? And, if so, how to do it? I think that'd be ideal, but wasn't sure if it would be possible, at least without significant refactoring.

I'm sure it possible, and I think we should, but we should spend a little more time discussing whether we want it. For now, maybe just not publish DafnyLanguageServer, unless you see a reason why it would be useful to consume for other .NET projects.

Sounds reasonable.

keyboardDrummer · 2022-06-08T08:50:45Z

Source/Dafny/DafnyPipeline.csproj

@@ -34,4 +34,19 @@
 <ItemGroup>


Shouldn't DafnyPipeline and DafnyRuntime be published as packages for Dafny as a library use-cases?

I think so, but I was thinking that we'd make the modifications you mention here before doing that. If you think the library would be useful as-is then, yeah, let's include it.

I think we should publish them now. Customers can always copy things from DafnyDriver if they're missing something that's only there.

keyboardDrummer · 2022-06-08T15:51:33Z

Source/Dafny/DafnyPipeline.csproj

@@ -34,4 +34,19 @@
 <ItemGroup>
 <Content Include="DafnyPrelude.bpl" CopyToOutputDirectory="PreserveNewest" />
 </ItemGroup>
+
+ <ItemGroup>


For reasons I outlined here, I don't think DafnyPipeline should reference DafnyRuntime in any way. Can we move these references to DafnyDriver?

Yeah, I think that's where they belong (and where I originally put them). Now that I understand how to make that work, I'm going to do it.

I changed my mind on this yet again. The issue I came across is that the DafnyPipeline project, which we're making available as a library, includes the compilers. If you invoke those compilers and their assembly (or, as an option, possibly some other one that's available at runtime) doesn't contain the runtime files, they'll crash. So the runtime files can't reasonably go in DafnyDriver. They ultimately should go in language-specific compiler packages, as I think we all agree. But I still feel like it'd be messy to put them in the DafnyRuntime assembly (even though the source code is in that package). So that leaves DafnyPipeline, for now, until we split off the individual compilers.

atomb · 2022-06-09T16:15:51Z

This is currently failing due to a failed LSP test, EnsuresPriorityWorksEvenIfRemovingMethodsWhileTypo. We'll need to fix that separately before merging.

robin-aws · 2022-06-10T18:35:27Z

.github/workflows/release-downloads-nuget.yml

+ z3 -version
+ dafny -version
+ - name: Check
+ run: dafny/dafny /compileVerbose:0 /compile:0 a.dfy


You'l have to replace dafny/dafny with dafny everywhere, since dotnet tool install --global will put it directly on the PATH.

robin-aws · 2022-06-10T19:37:00Z

RELEASE.md

+ `RELEASE_NOTES.md`, and add a new "Upcoming" header above it.
+
+ Push and cut a PR, get it approved, and squash and merge those
+ changes to the `master` branch.



You need a step after #7 to manually trigger the new release-downloads-nuget.yml workflow too.

robin-aws · 2022-06-10T19:37:44Z

Scripts/package.py

- lastdot = lines[2].rindex('.',qstart)
- v1 = lines[2][qstart+1:lastdot]
- v2 = lines[2][lastdot+1:qend]
+ verline = lines[5]


Yuck - there has to be a better way of tracking the version number in the future :P

Yeah, I agree. :)

robin-aws · 2022-06-10T19:39:04Z

Source/Dafny/Compilers/Compiler-java.cs

@@ -16,6 +16,7 @@
 using System.Diagnostics;
 using System.Text.RegularExpressions;
 using System.Reflection;
+using Microsoft.Win32.SafeHandles;


Is this used somehow? Hopefully not?

Ah, IDEs! I was exploring various APIs to use to emit DafnyRuntime.jar, and my IDE must have inserted that while I had something temporary in place that I removed as soon as I read the docstring. :)

robin-aws · 2022-06-10T19:40:29Z

Source/Dafny/Compilers/Compiler-java.cs

@@ -2195,6 +2196,19 @@ private class GenericArrayElementLvalue : ILvalue {
 }
 }

+ private void EmitRuntimeJar(string targetDirectory) {


This is definitely "weird", but not a lot weirder than the old way. :)

It's at least more consistent with the behavior of the other languages.

robin-aws · 2022-06-10T19:47:30Z

Source/Dafny/Compilers/Compiler-java.cs

@@ -2207,8 +2221,12 @@ private class GenericArrayElementLvalue : ILvalue {
 return false;
 }
 }
+
+ var targetDirectory = Path.GetDirectoryName(targetFilename);
+ EmitRuntimeJar(targetDirectory);


Hmm...this should probably only happen if DafnyOptions.O.UseRuntimeLib is false. If it's true, the assumption is that you'll add DafnyRuntime.jar to the classpath yourself when you compile/run later. How hard is it to extract DafnyRuntime.jar from the nuget package after you've installed it?

I don't think this is blocking since existing codebases since we're still publishing the zip files as well, but we should probably make sure we start publishing DafnyRuntime.jar as well before we STOP publishing the zip files.

That's an easy check to add, so I'll do it even if it's not immediately critical.

Oh, and in response to your question, I don't know of any way to extract the embedded files from an assembly other than through the .NET API, but there probably is one.

Enable packaging Dafny as a .NET tool

a852483

atomb self-assigned this May 24, 2022

atomb added 7 commits June 1, 2022 14:36

Merge remote-tracking branch 'upstream/master' into dotnet-tool

ac6fd5e

Embed runtime files in the Dafny assembly

9777107

Have compilers use embedded runtime files

0cc5b32

Remove obsolete TODO

20d028f

Fix versions for NuGet packages

dc3240b

Build NuGet packages in CI

09e10a6

Commented-out code also exists to upload them, but we need to configure an API key first.

Merge remote-tracking branch 'upstream/master' into dotnet-tool

c56e4a3

atomb marked this pull request as ready for review June 7, 2022 17:52

atomb added 2 commits June 7, 2022 10:57

Update list of version locations for releases

b0920ee

Merge remote-tracking branch 'upstream/master' into dotnet-tool

c9fa4df

atomb requested review from robin-aws, fabiomadge and mschlaipfer June 7, 2022 18:04

Add NuGet package support to release notes

12945cf

atomb changed the title ~~[draft] Enable packaging Dafny as a .NET tool~~ Enable packaging Dafny as a .NET tool Jun 7, 2022

fabiomadge reviewed Jun 7, 2022

View reviewed changes

Uncomment NuGet upload steps

09ca7cd

fabiomadge reviewed Jun 7, 2022

View reviewed changes

fabiomadge previously approved these changes Jun 7, 2022

View reviewed changes

robin-aws requested changes Jun 7, 2022

View reviewed changes

atomb added 4 commits June 7, 2022 14:52

Update release notes to mention all NuGet packages

25f1b4c

Don’t embed runtime files that are never used

98b7eed

Add comment to version.cs about other files to keep in sync

5307661

Merge remote-tracking branch 'upstream/master' into dotnet-tool

382a68e

keyboardDrummer reviewed Jun 8, 2022

View reviewed changes

atomb added 7 commits June 8, 2022 09:19

Move embedded files to DafnyDriver

7a25a3e

Don’t package DafnyLanguageServer for now

83db18f

Don’t package DafnyTestGeneration for now

aac8706

Do package DafnyPipeline

5a0b2c9

Update release notes

e04c8cc

Emit C++ header and Java JAR during compilation

fdc3395

Re-add Java tests to NuGet download workflow

06a5274

atomb dismissed fabiomadge’s stale review via 06a5274 June 8, 2022 17:53

atomb added 4 commits June 8, 2022 11:22

Move embedded runtimes back into DafnyPipeline

4fb959a

Fix test output

6294c94

Fix directory calculation for generated JAR file

6f9485f

Add inter-project dependency

a5d0dc2

keyboardDrummer approved these changes Jun 9, 2022

View reviewed changes

Merge branch 'master' into dotnet-tool

1433c5d

keyboardDrummer previously approved these changes Jun 10, 2022

View reviewed changes

Merge branch 'master' into dotnet-tool

a1c97dd

atomb dismissed keyboardDrummer’s stale review via a1c97dd June 10, 2022 19:25

robin-aws requested changes Jun 10, 2022

View reviewed changes

atomb added 4 commits June 10, 2022 13:09

Use dafny/dafny -> dafny for NuGet test

5e58bfd

Add NuGet testing to the release process notes

d89f522

Remove accidental IDE-inserted using clause

cefa240

Only emit JavaRuntime.jar in the absence of /useRuntimeLib

200d002

robin-aws approved these changes Jun 10, 2022

View reviewed changes

atomb merged commit 51b6885 into dafny-lang:master Jun 10, 2022

atomb deleted the dotnet-tool branch June 10, 2022 21:23

cpitclaudel added a commit to dafny-lang/compiler-bootstrap that referenced this pull request Jun 30, 2022

build: Switch to -useRuntimeLib to adjust to dafny-lang/dafny#2051

6c65e10

cpitclaudel added a commit to dafny-lang/compiler-bootstrap that referenced this pull request Jul 12, 2022

build: Switch to -useRuntimeLib to adjust to dafny-lang/dafny#2051

398e629

		#- name: Upload package to NuGet
		# run: dotnet nuget push "Binaries/Dafny*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json

	- feat: Dafny is now available on NuGet, installable with `dotnet tool install Dafny`.
	- feat: Dafny is now available on NuGet, installable with `dotnet tool install --global Dafny`.

		var rt = wr.NewFile("dafny/dafny.go");
		ReadRuntimeSystem("DafnyRuntime.go", rt);

Enable packaging Dafny as a .NET tool #2051

Enable packaging Dafny as a .NET tool #2051

Conversation

atomb commented Apr 22, 2022 • edited Loading

mschlaipfer commented Apr 22, 2022

atomb commented Apr 22, 2022

robin-aws commented Apr 22, 2022

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

keyboardDrummer Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

fabiomadge left a comment

Choose a reason for hiding this comment

atomb commented Jun 7, 2022

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

keyboardDrummer Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Jun 9, 2022

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 commented Apr 22, 2022 •

edited

Loading

keyboardDrummer Jun 8, 2022 •

edited

Loading

keyboardDrummer Jun 8, 2022 •

edited

Loading

keyboardDrummer Jun 8, 2022 •

edited

Loading

keyboardDrummer Jun 8, 2022 •

edited

Loading

keyboardDrummer Jun 8, 2022 •

edited

Loading

keyboardDrummer Jun 8, 2022 •

edited

Loading