1

I'm trying to compile a simple max example (permalink) to java:

$ Scripts/dafny /compileTarget:java /compile:3 max.dfy

Dafny program verifier finished with 3 verified, 0 errors
Wrote textual form of target program to max-java/max.java
Additional target code written to max-java/_System/nat.java
Additional target code written to max-java/_System/__default.java
Additional target code written to max-java/dafny/Tuple0.java
Running...

max element of [7, 4, 2, 9, 6, 3] is 9

So I can compile+run it as a whole, but can't do so independently:

$ Scripts/dafny /compileTarget:java /compile:1 /spillTargetCode:1 /out:main.java max.dfy
$ javac -cp Binaries/DafnyRuntime.jar main-java/main.java
main-java/main.java:3: error: package _System does not exist
import _System.*;
^
main-java/main.java:18: error: package _System does not exist
    dafny.Helpers.withHaltHandling(_System.__default::__Main);
                                          ^
2 errors

Another try:

$ javac -cp Binaries/DafnyRuntime.jar -cp main-java/ main-java/main.java
main-java/main.java:18: error: cannot find symbol
    dafny.Helpers.withHaltHandling(_System.__default::__Main);
         ^
  symbol:   class Helpers
  location: package dafny
1 error

I guess I must be missing something.

OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87

1 Answers1

0

You need to add to the compilation the "additional target code" files which were created by the dafny compiler. You can do it with something like this:

$ javac -cp Binaries/DafnyRuntime.jar main-java/main.java main-java/*/*.java

Then, you can run with something like

$ cd main-java
$ java -cp ../Binaries/DafnyRuntime.jar:. Main

Found this by looking for examples of usage of javac in the test files of the Dafny source - but even there it was failing, and the -cp switch you used was the missing piece.

hmijail
  • 1,069
  • 9
  • 17