search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

Java 11: compile error from passing a set of map to a function method #1374

Open sorawee opened 3 years ago

sorawee commented 3 years ago 
function method f (x : set<map<int, int>>) : int
{
  1
}

method Main () 
{
  print f({map[1 := 1]});
}

results in:

/Users/sorawee/projects/dsmith/tmp-java/_System/__default.java:15: error: incompatible types: DafnySet<DafnyMap> cannot be converted to DafnySet<? extends DafnyMap<? extends BigInteger,? extends BigInteger>>
    System.out.print(String.valueOf(__default.f(dafny.DafnySet.of(dafny.DafnyMap.fromElements(new dafny.Tuple2(java.math.BigInteger.ONE, java.math.BigInteger.ONE))))));
                                                                 ^

Note that this compiles fine with Java 8.

keyboardDrummer commented 3 years ago

Just curious, what led you to compile this with Java11? Our build uses Java8. Do you think we should support multiple Java versions, or at least the latest one?

sorawee commented 3 years ago

The instruction at https://github.com/dafny-lang/dafny/wiki/INSTALL states:

Install Java (at least Java 8) from https://www.oracle.com/java/technologies/javase-downloads.html or install Amazon Corretto from https://docs.aws.amazon.com/corretto/latest/corretto-11-ug/what-is-corretto-11.html

If Java 11 is not supported, I think the wiki should indicate so.