dafny build with extern declarations

[DavePearce]

Dafny version

3.12.0

Code to produce this issue

module Test {
  function {:extern} inc(x:int) : (r:int)

  method aTest() {
    expect inc(1) == 1;
  }
}

Command to run and resulting output

dafny build --function-syntax 4 test.dfy

This resulted in the following:

Dafny program verifier finished with 0 verified, 0 errors
Errors compiling program into test
(5003,37): error CS0117: '__default' does not contain a definition for 'inc'

What happened?

I don't necessarily believe the above was unexpected --- but I am stuck. The question is: how do I compile Dafny containing {:extern} functions to Java?

Instead of using dafny build I logically tried dafny translate next. Unfortunately, this does not generate the DafnyRuntime.jar even with --include-runtime provided (perhaps that is the real bug here). This means I cannot build just from the Dafny source, but would have to check the runtime jar into my repository.

My requirements for building the project are:

1. Dafny source files in one directory (e.g. src/dafny)
2. My Java source files in another directory (e.g. src/java) which provides implementation for {:extern} functions.
3. Generated Java files from Dafny placed into a build directory (e.g. bin/java).
4. At which point, I should be able to compile everything in src/java and bin/java together.

I should also note that dafny test has similar problems to dafny build. However, I cannot control how dafny test is trying to build my project. It does not even support the --output option from dafny build.

Anyway, any thoughts on this would be appreciated.

What type of operating system are you experiencing the problem on?

Linux

[DavePearce]

An additional note:

1. I thought copying my Java file containing the native implementations of my {:extern} functions into the bin/java build directory would be one option for it to work.
2. This seemed like it would work as the module containing these functions has no other code, hence Dafny does not generate a file for it at all.
3. However, Dafny appears to delete the file I copied over (and does not replace it with anything).

If this approach was permitted, then it would offer me a solution. I could copy the native Java code into position beforehand.

[keyboardDrummer]

I think you have to pass the .java file that implements your {:extern} as an additional input file on the command line, when invoking dafny build, like dafny build --target:java program.dfy externs.java

Instead of using dafny build I logically tried dafny translate next. Unfortunately, this does not generate the DafnyRuntime.jar even with --include-runtime provided (perhaps that is the real bug here)

That's indeed a bug. It should generate it when --include-runtime is provided.

[davidcok]

David - you should be able to just have the .java file on the command-line.
Try this:

A.java:
package p;

public class A {
public static void mjava() {
System.out.println("Hi from Java");
}
}

test.dfy:
method Main() {
print "Hi from Dafny\n";
mm();
}

method {:extern "p.A","mjava"} mm()

And then, with those two files in your current directory:
dafny build -t:java test.dfy A.java
java -jar test.jar

The test.jar that is created (by build) is an executable jar. It includes compiled .class files for any .java files that are on the commandline.

[DavePearce]

Hey David & Remy,

Great --- thanks, I will try that out. It wasn't obvious to me that was how you're supposed to do it.

[DavePearce]

One issue I have encountered straightaway:

• My default implementation depends on external dependencies provide from Maven central! Specifically, a jar file.

The problem we have here is that Dafny is trying to replace the build system, but not providing all the functionality of a build system. Anyways, there is one possible solution here:

• I write some dummy files matching the functions used in the external dependency. I ask Dafny to compile against them. Then I delete them, and use the jar file instead. Potentially, an interface with a default static implementation that can be overriden elsewhere.

Personally, I think a better approach would be to allow all commands which generate code to have an option like --source-only which stops them from trying to actually compile the code. Thus, dafny build --source-only replaces dafny translate and we have dafny test --source-only to generate the test harness. That way, I can use my build system to manage the actual building process, rather than working around dafny. Anyway, that's just a thought and appreciate its probably not on your priority list!

[davidcok]

aside from not providing the DafnyRuntime.jar, does dafny translate do what you want dafny build-source-only to do?
(I realize there is not a source option for dafny test)

[DavePearce]

Hey David,

Yes, I think so. I just suggested --source-only to make it consistent between build and test.

[DavePearce]

I think there is another option for me actually. That is to avoid {:extern} altogether! I think I can do this using lambda's on the Dafny side. Then on the Java side when I create my Dafny object I fill out the lambda's with what I actually need.

[keyboardDrummer]

The {:test} attribute has not fully matured at the moment, but dafny translate could, without extra arguments, also generate the test harnass for methods annotated with {:test}. It already generates some XUnit testing harnass when C# is the target.

[keyboardDrummer]

I think there is another option for me actually. That is to avoid {:extern} altogether! I think I can do this using lambda's on the Dafny side. Then on the Java side when I create my Dafny object I fill out the lambda's with what I actually need.

That works for sure :-) I think externs are only needed when there is functionality that you want to be available statically, without requiring closures or traits to be passed around.