Unintuitive overloading of the term "compile" in CLI flags

[robin-aws]

This is something that's always irked me about the dafny CLI, but that I've just gotten used to. I assert that it's a common sharp edge for new Dafny users and worth fixing.

The current /compile flag has the following meaning (copied from /help output):

/compile:<n>  0 - do not compile Dafny program
    1 (default) - upon successful verification of the Dafny
        program, compile it to the designated target language
        (/noVerify automatically counts as failed verification)
    2 - always attempt to compile Dafny program to the target
        language, regardless of verification outcome
    3 - if there is a Main method and there are no verification
        errors and /noVerify is not used, compiles program in
        memory (i.e., does not write an output file) and runs it
    4 - like (3), but attempts to compile and run regardless of
        verification outcome

There are several problems with this:

1. The idea of "I'm going to compile SO HARD that I actually execute the program too" is not exactly intuitive. :)
2. /compile:1 or /compile:2 currently not only compiles the Dafny source to whatever the /compileTarget is, but also applies the target language compiler (for C# and Java), or at least runs the output through a target language tool (e.g. node) without executing any Main method, presumably to ensure the program is valid. This is quite subtle and surprising if the Dafny compiler doesn't actually produce a valid target language program. If you actually want to run JUST the Dafny compiler the correct set of flags is /compile:0 /spillTargetCode:... instead, which feels even weirder!
3. I generally dislike the style of numeric flags where different numbers have very different semantic meanings, and this is just one of the most egregious examples.

No alternative proposal just yet, and no plans to immediately fix this, just needed to get it written down after my latest adventure with this. :)

[keyboardDrummer]

if the Dafny compiler doesn't actually produce a valid target language program

Shouldn't a valid Dafny program always produce a valid target language program? Extern annotations currently prevent this right? I think we can change how extern is compiled to prevent them from creating invalid target language programs.

If you actually want to run JUST the Dafny compiler the correct set of flags is /compile:0 /spillTargetCode:... instead, which feels even weirder!

Why would you want to do that?

The idea of "I'm going to compile SO HARD that I actually execute the program too" is not exactly intuitive. :)

Made me giggle 😄 I'd prefer separate top-level commands for building and running, similar to dotnet build and dotnet run.

[parno]

Why would you want to do that?

We do that in all of our non-trivial projects. We often want to merge (in a non-trivial way) the Dafny portion of the project with code written in the native language. We also want control over the flags passed to the native compiler. It actually seems strange to me that Dafny wants to try to compile code all the way to an executable for us. There are already tools that will do that, given appropriate input, and having Dafny take over that job seems like it mostly works for small examples.

[keyboardDrummer]

We also want control over the flags passed to the native compiler.

Interesting. Can you give examples?

We often want to merge (in a non-trivial way) the Dafny portion of the project with code written in the native language.

Is that to implement the {:extern} definitions, or also for other things? Can you show an example?

It actually seems strange to me that Dafny wants to try to compile code all the way to an executable for us. There are already tools that will do that, given appropriate input, and having Dafny take over that job seems like it mostly works for small examples.

I think there is value in returning already built target-language artefacts instead of target-language source, because building from source is not a trivial problem. Suppose I have a Dafny project A that depends on another Dafny project B and uses Dafny version 3.2, and I want to integrate project A with a .NET project.

One option is that Dafny spits out:

DafnyA.dll
DafnyB.dll
DafnyRuntime_3.2.dll

I can depend on these binaries in my .NET project and I'll be done. For performance reasons, if code changes, Dafny will rebuild as little as possible. If something changes in the source of project A, only DafnyA.dll needs to be rebuilt. Changes in the source of B may cause DafnyA.dll and DafnyB.dll to be rebuilt. DafnyRuntime_3.2.dll never needs to be rebuilt.

A second option is that Dafny spits out a list of *.cs source files and assuming I want the same build performance as above, I have to:

• Create three .csproj files
• Configure each project to build the right source
• Configure project A to depend on B and the Runtime
• Configure project B to depend on the Runtime

The second option seems like extra work to me.

Alternatively, we could let Dafny emit both the source files and the build configuration, .csproj files in this case. In that case Dafny does most of the work for me, I just need to figure out which version of the C# compiler to use. However, I still wonder what the benefit is. To me, emitting artefacts that are as compiled as possible means that Dafny asks less from the programmer.

[robin-aws]

Shouldn't a valid Dafny program always produce a valid target language program? Extern annotations currently prevent this right? I think we can change how extern is compiled to prevent them form creating invalid target language programs.

Agreed, I only mention this because it's how I realized how much compiling was happening - I was trying to work around #1317 (again related to externs). I definitely agree I'd be very happy to come up with a FFI that made it always possible to compile the Dafny code by itself.

I'm torn about the larger question of whether Dafny should take responsibility for producing fully compiled/packaged artifacts in target languages. I agree it can be more convenient for some users, but it's also adopting a lot of complexity to the dafny CLI, and may scale badly as more languages are supported.

[keyboardDrummer]

I'm torn about the larger question of whether Dafny should take responsibility for producing fully compiled/packaged artifacts in target languages. I agree it can be more convenient for some users, but it's also adopting a lot of complexity to the dafny CLI, and may scale badly as more languages are supported.

I think Dafny emitting source for some particular language, but not knowing how to build it, isn't an option since then we can't test whether the emitted code is correct. Given that, I don't think including the full build in the CLI by default is increasing complexity, but I agree that it is a lot.

[robin-aws]

That is a good point - it's certainly already true that we at least have to be able to compile and run a Main method, or else we have no hope of testing a backend in the Dafny test suite.

And the build output may need to declare target language dependencies based on the Dafny source in some cases. E.g. only some Dafny codebases will use unbounded int values, and it would be a lot better to only require libraries like biginteger.js when needed.

[jonhnet]

I think there are two separate issues at play here.

The first is, should Dafny be able to step back and be a component of a bigger build system in complex projects? /compile:0 /spillTargetCode accomplishes that, even if the arguments aren't beautiful.

The second is, should Dafny run all the back-end tools all the way to an executable? When it had a single C# backend, that felt pretty natural, just like I can invoke the assembler and linker by invoking gcc; they're abstracted away into the C interface. With a half-dozen backends, this feels a lot less natural: what an "executable" means for each backend is different, and many of the new backends have been introduced precisely to fit Dafny code into bigger systems. I'm with Bryan that one-step-to-executable is really only relevant for small programs, just as real systems very quickly outgrow "gcc foo.c into a.out".

A proposed convergence:

• There should be a flag that means "verify and then emit target X", analogous to the "-c" flag used to partially build C programs.
• That should be a single flag, not /compile:0 /spillTargetCode /backend=something. Say /emitTarget={C++,JS,...}
• Not all backends should be required to pass beyond the emit-code phase. In little-program mode, you can call Dafny, get a "Verified" result, and run the C# binary all in one step. If you want C++, you're going to have to get into the linking business anyway, so passing /emitTarget is both the only way to select a power user backend like C++, and also means there's no surprise that the C++ backend doesn't invoke gcc; that joy is left for the developer and her makefile.

[parno]

We also want control over the flags passed to the native compiler.
Interesting. Can you give examples?

We might want to compile the C with debug symbols while we debug the system as a whole and then turn on maximum optimization for the release build. We might want to add/remove the frame pointer. We sometimes want to pass special defines (e.g., _LIBCPP_HAS_NO_THREADS) for additional performance optimization when we know the rest of the code is single-threaded. There are other examples in one of our recent makefiles

Dafny can't possibly have Dafny-level flags to toggle all of these, so to go through Dafny, Dafny would need to at the very least allow the user to pass all of these arguments through to the compiler backends (sort of the way it does with Boogie options). Relatedly, if the rest of the project is using clang, but Dafny invokes g++ that can be awkward as well, even though in a perfect world they would play nicely together.

I think Dafny emitting source for some particular language, but not knowing how to build it, isn't an option since then we can't test whether the emitted code is correct.

My vote would be to encode that knowledge into a Makefile (or something similar) that the CI can use, rather than hardcoding it into the Dafny binary.

Is that to implement the {:extern} definitions, or also for other things? Can you show an example?

In terms of fitting within a larger project, yes, I lot of challenges have been around being able to export/import the right definitions (in the Makefile above, you can see there are various hoops to connect up to code that implements some of the extern definitions, as well as to add things like benchmarking on the outside). Some of the more complex ones were projects where we needed to be able to both consume .h files from another project but also produce .h files they could consume, e.g., in our verified QUIC we were trying to interoperate with cryptographic code verified with F* that itself produced a bunch of automatically generated C code.

For performance reasons, if code changes, Dafny will rebuild as little as possible.

(a) FWIW, to me, deciding what to rebuild feels like a job for a build system, not a verification tool. (b) Code compilation time is such a small fraction of our development cycle, that I'm not sure it's worth optimizing for inside of Dafny. 99.999% of our time is spent waiting on verification, so saving time on compilation seems marginal.

[keyboardDrummer]

We might want to compile the C with debug symbols while we debug the system as a whole and then turn on maximum optimization for the release build. We might want to add/remove the frame pointer. We sometimes want to pass special defines (e.g., _LIBCPP_HAS_NO_THREADS) for additional performance optimization when we know the rest of the code is single-threaded. There are other examples in one of our recent makefiles

Dafny can't possibly have Dafny-level flags to toggle all of these, so to go through Dafny, Dafny would need to at the very least allow the user to pass all of these arguments through to the compiler backends (sort of the way it does with Boogie options). Relatedly, if the rest of the project is using clang, but Dafny invokes g++ that can be awkward as well, even though in a perfect world they would play nicely together.

Make sense, so Dafny should, without too many flags, produce source output which includes a default method for how to build that source, such as a .csproj file for .NET or a makefile for c++. Optionally, Dafny can run that default build configuration to build an executable, which can be used for testing and simple programs.

My vote would be to encode that knowledge into a Makefile (or something similar) that the CI can use, rather than hardcoding it into the Dafny binary.

Sounds good.

(a) FWIW, to me, deciding what to rebuild feels like a job for a build system, not a verification tool.

Yes, I think spitting out idiomatic build configuration in the "emit source" mode for Dafny should allow those build tools to manage the caching in that step. For example, suppose you could configure a Dafny project A and B, where A depends on B, and you target .NET, Dafny would emit two .csproj files, where one refers to the other, and dotnet would manage when to rebuild B.dll.

Code compilation time is such a small fraction of our development cycle, that I'm not sure it's worth optimizing for inside of Dafny. 99.999% of our time is spent waiting on verification, so saving time on compilation seems marginal.

Thanks for the callout. Relatedly, I think Dafny should be able to know what parts of a program need to be reverified and which not, when developing and repeatedly running verification.

[keyboardDrummer]

I'm curious how others feel about the following:

Update the Dafny CLI so it can accept as its first argument a "command". Commands correspond to use-cases.

• dafny build, compiles to target language source files. Useful for integrating with a target language application.

  • Similar to the current dafny /compile:0 /spillTargetCode:2 .
  • dafny build /noVerify skips verification and produces target source code, similar to dafny /noVerify /compile:0 /spillTargetCode:3.
  • We'll update Dafny so when it emits source files for a target language, it also emits a minimal build configuration, such as a .csproj or makefile, to help with downstream builds.

• dafny verify, runs verification but does not emit anything. Useful during development.

  • Similar to the current dafny /compile:0.

• dafny run, runs the Dafny program. Useful for standalone Dafny programs and testing dafny.

  • Similar to the current dafny /compile:3.
  • dafny run /noVerify runs the program without verifying it, similar to dafny /noVerify /compile:4

Note that there's no dafny executable command for producing executable files, which would be similar to the current dafny /compile:1. The reason I've left this out is that the output would be badly defined. Given any target language, there will be many ways to go from source code to downstream compilation artefacts. Even for dotnet, which is arguably one of the easier to build targets, there is a default, a "Ready to run" and a "Self-contained" build, which all would be equally valid results of a dafny executable command.

Although dafny run is further downstream than dafny executable, its output is well-defined so that one is fine to have.

[robin-aws]

I'm really liking this. So run would depend on build, which would depend on verify (unless /noVerify was provided).

We wouldn't even be breaking backwards compatibility, since non-flag arguments are currently rejected if they don't have a recognized extension for "other files" for the given compilation target.

We could also provide dafny test! The minimal support for the {:test} attribute I added is a bit clunky so far because that doesn't exist: you can only build Dafny test files into C# code with [Xunit.Fact] attributes, and then run via a separate call to dotnet test. It's also still an open question for me whether Dafny should have a separate testing framework itself: those tend to be implemented in user code based on an API for reflection, which Dafny doesn't have yet. dafny test would be a useful abstraction away from those details.

(Loving this discussion by the way, thanks for all the great feedback everyone! I hadn't intended to open such a can of worms by griping about /compile but I'm really glad I did :)

[keyboardDrummer]

Resolved by #2603