The classpath is often too long for development builds on windows

JLedelay commented 1 year ago

On the dev branch since PR #735, I'm encountering some issues with verification of Java files:

It seems the first file in the argument list now needs to contain a main method
The order of input files now matters for the output
Errors and verification result are no longer printed, or verification is no longer run?

Each of these have an example below. I've combined them into one issue because I'm assuming they are strongly related.

The following input:
```
public class C {
}
```
yields the following output: error: can't find main(String[]) method in class: C

The following input:
```
// C.java: 
public class C {
D d;
}
```

// D.java: 
public class D {
}

with the following input: vercors\bin\vct C.java D.java yields the following output:

C.java:3: error: cannot find symbol
        D d;
        ^
  symbol:   class D
  location: class C
1 error
error: compilation failed

Changing the order to vercors\bin\vct D.java C.java yields error: can't find main(String[]) method in class: D.

Adding a main class to D.java as such:
```
// D.java
public class D {
public static void main(String[] args) {
    //@ assert false;
}
}
```
and running vercors\bin\vct D.java C.java yields no output (also no [INFO] Starting verification), and terminates in ~0.6 seconds.

In comparison, running the same command with an older version of vercors (hash 4f3663596290352668f94c5d91998a33505cf2f3, just prior to the merger of PR #735 in 9e9305fa2e4d633534294567ad7e8526e1f0cf02) takes 18 seconds and gives the following output:

======================================
 At D.java:3:7:
--------------------------------------
    1  public class D {
    2   public static void main(String[] args) {
                   [-------------
    3           //@ assert false;
                    -------------]
    4   }
    5  }
--------------------------------------
[1/2] Assertion may not hold, since ...
--------------------------------------
[At generated constant `false`]
--------------------------------------
[2/2] ... this expression may be false (https://utwente.nl/vercors#assertFailed:false)
======================================

pieter-bos commented 1 year ago

I suspect that:

you are running vercors via the bin/vct script (this is fine, but unfortunately occasionally brittle);
the file bin/.classpath exists, but is empty or only contains whitespace.

VerCors is invoked from this script like:

java %MORE_JAVA_OPTS% -Xss128M -cp "%CLASSPATH%" %*

This ends up being:

java -Xss128M -cp vct.main.Main C.java

Sure enough:

$ java -Xss128M -cp vct.main.Main examples/private/joel15.java
error: can't find main(String[]) method in class: C

Deleting the bin/.classpath file should regenerate the classpath, resolving the problem - let me know.

Edit: to be clear: this invokes the java compiler - not vercors. We are using the nonsense classpath "vct.main.Main". Apparently you can pass a source file directly to java to run it.

JLedelay commented 1 year ago

I indeed run vercors via the bin/vct script. The file bin/.classpath is not empty. I renamed bin/.classpath to bin/.classpath_temp. Running bin/vct C.java again, the classpath is extracted from sbt. The contents of the newly generated bin/.classpath are identical to bin/.classpath_temp, and I get the same error as before.

The contents of bin/.classpath

`C:\Universiteit\Master\Afstuderen\vercors-dblock\target\scala-2.13\classes;C:\Universiteit\Master\Afstuderen\vercors-dblock\hre\target\scala-2.13\classes;C:\Universiteit\Master\Afstuderen\vercors-dblock\col\target\scala-2.13\classes;C:\Universiteit\Master\Afstuderen\vercors-dblock\rewrite\target\scala-2.13\classes;C:\Universiteit\Master\Afstuderen\vercors-dblock\viper\target\scala-2.13\classes;C:\Universiteit\Master\Afstuderen\vercors-dblock\parsers\target\scala-2.13\classes;C:\Users\joell\.sbt\1.0\staging\b306aa57c2c5f83a9da9\silver\target\scala-2.13\classes;C:\Users\joell\.sbt\1.0\staging\3f8dde1bc2ca9c35301e\carbon\target\scala-2.13\classes;C:\Users\joell\.sbt\1.0\staging\ae2eeccd5c701dd530b0\silicon\target\scala-2.13\classes;C:\Users\joell\.sbt\1.0\staging\ae2eeccd5c701dd530b0\silicon\common\target\scala-2.13\classes;C:\Universiteit\Master\Afstuderen\vercors-dblock\parsers\lib\SysCIR.jar;C:\Universiteit\Master\Afstuderen\vercors-dblock\src\main\universal\res;C:\Universiteit\Master\Afstuderen\vercors-dblock\src\main\universal\deps;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\scala-library\2.13.5\scala-library-2.13.5.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\code\gson\gson\2.8.0\gson-2.8.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scalactic\scalactic_2.13\3.2.7\scalactic_2.13-3.2.7.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-xml_2.13\1.2.0\scala-xml_2.13-1.2.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-parallel-collections_2.13\1.0.4\scala-parallel-collections_2.13-1.0.4.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\github\scopt\scopt_2.13\4.0.1\scopt_2.13-4.0.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\typesafe\scala-logging\scala-logging_2.13\3.9.4\scala-logging_2.13-3.9.4.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\ch\qos\logback\logback-classic\1.2.3\logback-classic-1.2.3.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upickle_2.13\2.0.0\upickle_2.13-2.0.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.cli\0.8.7\org.jacoco.cli-0.8.7-nodeps.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.agent\0.8.7\org.jacoco.agent-0.8.7-runtime.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\fusesource\jansi\jansi\2.4.0\jansi-2.4.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\harawata\appdirs\1.2.1\appdirs-1.2.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\thesamet\scalapb\scalapb-runtime_2.13\0.11.11\scalapb-runtime_2.13-0.11.11.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\apache\commons\commons-lang3\3.1\commons-lang3-3.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\sosy-lab\java-smt\3.14.3\java-smt-3.14.3.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\github.com\niomaster\antlr4\releases\download\4.8-extractors-2\antlr4.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\scala-reflect\2.13.5\scala-reflect-2.13.5.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\slf4j\slf4j-api\1.7.30\slf4j-api-1.7.30.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\ch\qos\logback\logback-core\1.2.3\logback-core-1.2.3.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\ujson_2.13\2.0.0\ujson_2.13-2.0.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upack_2.13\2.0.0\upack_2.13-2.0.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upickle-implicits_2.13\2.0.0\upickle-implicits_2.13-2.0.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.core\0.8.7\org.jacoco.core-0.8.7.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.report\0.8.7\org.jacoco.report-0.8.7.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\args4j\args4j\2.0.28\args4j-2.0.28.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\java\dev\jna\jna-platform\5.6.0\jna-platform-5.6.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\thesamet\scalapb\lenses_2.13\0.11.11\lenses_2.13-0.11.11.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\protobuf\protobuf-java\3.19.2\protobuf-java-3.19.2.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-collection-compat_2.13\2.7.0\scala-collection-compat_2.13-2.7.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\sosy-lab\common\0.3000-529-g6152d88\common-0.3000-529-g6152d88.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\guava\guava\31.1-jre\guava-31.1-jre.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\checkerframework\checker-qual\3.22.0\checker-qual-3.22.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\github\spotbugs\spotbugs-annotations\4.7.0\spotbugs-annotations-4.7.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\code\findbugs\jsr305\3.0.2\jsr305-3.0.2.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\de\uni-freiburg\informatik\ultimate\smtinterpol\2.5-1242-g5c50fb6d\smtinterpol-2.5-1242-g5c50fb6d.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\github\uuverifiers\princess_2.13\2022-07-01\princess_2.13-2022-07-01.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\codehaus\mojo\animal-sniffer-annotations\1.18\animal-sniffer-annotations-1.18.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scalatest\scalatest_2.13\3.1.2\scalatest_2.13-3.1.2.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-parser-combinators_2.13\1.1.2\scala-parser-combinators_2.13-1.1.2.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\fastparse_2.13\2.2.2\fastparse_2.13-2.2.2.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\rogach\scallop_2.13\4.0.4\scallop_2.13-4.0.4.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\commons-io\commons-io\2.8.0\commons-io-2.8.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jgrapht\jgrapht-core\1.5.0\jgrapht-core-1.5.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\apache\commons\commons-pool2\2.9.0\commons-pool2-2.9.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\spray\spray-json_2.13\1.3.6\spray-json_2.13-1.3.6.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\www.sosy-lab.org\ivy\org.sosy_lab\javasmt-solver-z3\com.microsoft.z3-4.8.7.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upickle-core_2.13\2.0.0\upickle-core_2.13-2.0.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm\9.1\asm-9.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm-commons\9.1\asm-commons-9.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm-tree\9.1\asm-tree-9.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\java\dev\jna\jna\5.6.0\jna-5.6.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\guava\failureaccess\1.0.1\failureaccess-1.0.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\guava\listenablefuture\9999.0-empty-to-avoid-conflict-with-guava\listenablefuture-9999.0-empty-to-avoid-conflict-with-guava.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\errorprone\error_prone_annotations\2.11.0\error_prone_annotations-2.11.0.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\j2objc\j2objc-annotations\1.3\j2objc-annotations-1.3.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\github\uuverifiers\princess-parser_2.13\2022-07-01\princess-parser_2.13-2022-07-01.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\github\uuverifiers\princess-smt-parser_2.13\2022-07-01\princess-smt-parser_2.13-2022-07-01.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\sf\squirrel-sql\thirdparty-non-maven\java-cup\0.11a\java-cup-0.11a.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\sourcecode_2.13\0.1.7\sourcecode_2.13-0.1.7.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\geny_2.13\0.7.1\geny_2.13-0.7.1.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jheaps\jheaps\0.13\jheaps-0.13.jar;C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm-analysis\9.1\asm-analysis-9.1.jar `

bin/.classpath, but then split lines at `;` for readability

``` C:\Universiteit\Master\Afstuderen\vercors-dblock\target\scala-2.13\classes; C:\Universiteit\Master\Afstuderen\vercors-dblock\hre\target\scala-2.13\classes; C:\Universiteit\Master\Afstuderen\vercors-dblock\col\target\scala-2.13\classes; C:\Universiteit\Master\Afstuderen\vercors-dblock\rewrite\target\scala-2.13\classes; C:\Universiteit\Master\Afstuderen\vercors-dblock\viper\target\scala-2.13\classes; C:\Universiteit\Master\Afstuderen\vercors-dblock\parsers\target\scala-2.13\classes; C:\Users\joell\.sbt\1.0\staging\b306aa57c2c5f83a9da9\silver\target\scala-2.13\classes; C:\Users\joell\.sbt\1.0\staging\3f8dde1bc2ca9c35301e\carbon\target\scala-2.13\classes; C:\Users\joell\.sbt\1.0\staging\ae2eeccd5c701dd530b0\silicon\target\scala-2.13\classes; C:\Users\joell\.sbt\1.0\staging\ae2eeccd5c701dd530b0\silicon\common\target\scala-2.13\classes; C:\Universiteit\Master\Afstuderen\vercors-dblock\parsers\lib\SysCIR.jar; C:\Universiteit\Master\Afstuderen\vercors-dblock\src\main\universal\res; C:\Universiteit\Master\Afstuderen\vercors-dblock\src\main\universal\deps; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\scala-library\2.13.5\scala-library-2.13.5.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\code\gson\gson\2.8.0\gson-2.8.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scalactic\scalactic_2.13\3.2.7\scalactic_2.13-3.2.7.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-xml_2.13\1.2.0\scala-xml_2.13-1.2.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-parallel-collections_2.13\1.0.4\scala-parallel-collections_2.13-1.0.4.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\github\scopt\scopt_2.13\4.0.1\scopt_2.13-4.0.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\typesafe\scala-logging\scala-logging_2.13\3.9.4\scala-logging_2.13-3.9.4.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\ch\qos\logback\logback-classic\1.2.3\logback-classic-1.2.3.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upickle_2.13\2.0.0\upickle_2.13-2.0.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.cli\0.8.7\org.jacoco.cli-0.8.7-nodeps.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.agent\0.8.7\org.jacoco.agent-0.8.7-runtime.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\fusesource\jansi\jansi\2.4.0\jansi-2.4.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\harawata\appdirs\1.2.1\appdirs-1.2.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\thesamet\scalapb\scalapb-runtime_2.13\0.11.11\scalapb-runtime_2.13-0.11.11.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\apache\commons\commons-lang3\3.1\commons-lang3-3.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\sosy-lab\java-smt\3.14.3\java-smt-3.14.3.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\github.com\niomaster\antlr4\releases\download\4.8-extractors-2\antlr4.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\scala-reflect\2.13.5\scala-reflect-2.13.5.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\slf4j\slf4j-api\1.7.30\slf4j-api-1.7.30.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\ch\qos\logback\logback-core\1.2.3\logback-core-1.2.3.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\ujson_2.13\2.0.0\ujson_2.13-2.0.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upack_2.13\2.0.0\upack_2.13-2.0.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upickle-implicits_2.13\2.0.0\upickle-implicits_2.13-2.0.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.core\0.8.7\org.jacoco.core-0.8.7.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jacoco\org.jacoco.report\0.8.7\org.jacoco.report-0.8.7.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\args4j\args4j\2.0.28\args4j-2.0.28.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\java\dev\jna\jna-platform\5.6.0\jna-platform-5.6.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\thesamet\scalapb\lenses_2.13\0.11.11\lenses_2.13-0.11.11.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\protobuf\protobuf-java\3.19.2\protobuf-java-3.19.2.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-collection-compat_2.13\2.7.0\scala-collection-compat_2.13-2.7.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\sosy-lab\common\0.3000-529-g6152d88\common-0.3000-529-g6152d88.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\guava\guava\31.1-jre\guava-31.1-jre.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\checkerframework\checker-qual\3.22.0\checker-qual-3.22.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\github\spotbugs\spotbugs-annotations\4.7.0\spotbugs-annotations-4.7.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\code\findbugs\jsr305\3.0.2\jsr305-3.0.2.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\de\uni-freiburg\informatik\ultimate\smtinterpol\2.5-1242-g5c50fb6d\smtinterpol-2.5-1242-g5c50fb6d.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\github\uuverifiers\princess_2.13\2022-07-01\princess_2.13-2022-07-01.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\codehaus\mojo\animal-sniffer-annotations\1.18\animal-sniffer-annotations-1.18.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scalatest\scalatest_2.13\3.1.2\scalatest_2.13-3.1.2.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\modules\scala-parser-combinators_2.13\1.1.2\scala-parser-combinators_2.13-1.1.2.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\fastparse_2.13\2.2.2\fastparse_2.13-2.2.2.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\rogach\scallop_2.13\4.0.4\scallop_2.13-4.0.4.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\commons-io\commons-io\2.8.0\commons-io-2.8.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jgrapht\jgrapht-core\1.5.0\jgrapht-core-1.5.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\apache\commons\commons-pool2\2.9.0\commons-pool2-2.9.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\spray\spray-json_2.13\1.3.6\spray-json_2.13-1.3.6.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\www.sosy-lab.org\ivy\org.sosy_lab\javasmt-solver-z3\com.microsoft.z3-4.8.7.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\upickle-core_2.13\2.0.0\upickle-core_2.13-2.0.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm\9.1\asm-9.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm-commons\9.1\asm-commons-9.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm-tree\9.1\asm-tree-9.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\java\dev\jna\jna\5.6.0\jna-5.6.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\guava\failureaccess\1.0.1\failureaccess-1.0.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\guava\listenablefuture\9999.0-empty-to-avoid-conflict-with-guava\listenablefuture-9999.0-empty-to-avoid-conflict-with-guava.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\errorprone\error_prone_annotations\2.11.0\error_prone_annotations-2.11.0.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\google\j2objc\j2objc-annotations\1.3\j2objc-annotations-1.3.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\github\uuverifiers\princess-parser_2.13\2022-07-01\princess-parser_2.13-2022-07-01.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\io\github\uuverifiers\princess-smt-parser_2.13\2022-07-01\princess-smt-parser_2.13-2022-07-01.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\net\sf\squirrel-sql\thirdparty-non-maven\java-cup\0.11a\java-cup-0.11a.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\sourcecode_2.13\0.1.7\sourcecode_2.13-0.1.7.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\com\lihaoyi\geny_2.13\0.7.1\geny_2.13-0.7.1.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\jheaps\jheaps\0.13\jheaps-0.13.jar; C:\Users\joell\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\ow2\asm\asm-analysis\9.1\asm-analysis-9.1.jar ```

Edit: I do indeed get the same result when running with an empty bin/.classpath file. I'm wondering if there's something obviously missing in mine?

pieter-bos commented 1 year ago

Ah okay, next guess: you have the correct classpath, but it's too long: I believe 8192 characters is some type of limit on windows. I would not expect it to entirely drop an argument that is too long, but I don't know how else to explain it...

At least a workaround for now: compile vercors with sbt stage instead (or just type stage in the sbt shell in IntelliJ). This generates the files for the release, without actually bundling them in a deb or zip etc. You should find a working run script in target/universal/stage/bin. The reason this works is because in the release all our jars are in one directory, so we can directly pass lib/* to java (this does not expand to all the files in the shell script, it remains the literal string *, apparently supported by java)

bobismijnnaam commented 1 year ago

I vaguely remember there being a character limit on (environment?) variables on windows... This might impact the run script?

Also: putting the root of your project in C:\ might help

Edit: as for cause analysis: I added some dependencies in that PR; that might've pushed the classpath length over the limit.

JLedelay commented 1 year ago

It indeed seemed like the classpath (or the complete command including the classpath) was indeed too long.

I did a few things to work around this issue:

I used sbt stage as Pieter recommended. I did have some trouble getting the script to work, and it seemed that the classpath still wasn't being loaded properly. Because of this, I moved on to some suggestions that Bob mentioned.
I set the environment variable COURSIER_CACHE to C:\COURSIER_CACHE. This replaced the default value C:\Users\joell\AppData\Local\Coursier\v1\ with C:\COURSIER_CACHE. Instructions can be found here. This path occurred more than 50 times in bin/.classpath, so this shortened it considerably to around 8100 characters (under the 8192 character limit, but not by a lot). This allowed me to run VerCors, but when the command became too long, I got an error "error: The syntax of this command is incorrect" in cmd (and powershell), which indicated to me that the classpath needed to be shortened further.
I moved my project to C:\vercors-dblock. Since the previous path C:\Universiteit\Master\Afstuderen\vercors-dblock\ occurred 9 times in the bin/.classpath file, this shortened it by a further ~300 characters. This didn't seem to change anything in the number of files I could provide as arguments and seemed like a brittle solution anyway, so I moved on to the final suggestion from Bob, which was to run VerCors from IntelliJ.
I tried running VerCors from IntellliJ. After some fiddling with settings (setting the java version for sbt to jdk17), this worked, and I can provide all necessary java files. While this works, I'm now missing the script I wrote which measures execution time and notifies me through sound when verification is finished. I fixed this last point by adding an IntelliJ Marketplace plugin which plays a sound when a run is finished.
Plugin link and disclaimer

The plugin can be found here. No guarantees are given on the quality of the plugin. As the reviews state, the default sounds are not ideal. I replaced the sounds with the default Windows notification sound.

In conclusion: Running VerCors from the IntelliJ environment (as described on the wiki) is the workaround I'm using. This solves the problem, at least for now. VerCors is also usable from the command line, if the COURSIER_CACHE environment variable is set to a short path and not too many files are provided as arguments.

Thanks for the help!

bobismijnnaam commented 1 year ago

Joel's problems look consistent with the classpath being too long for the windows command line to handle, and with the symptoms described in the question of this stack overflow post: https://stackoverflow.com/a/54270831/2078414 Maybe we can consider the file-argument (where the java command expands the contents of a file to arguments) approach. I think you can combine this approach with regular arguments, e.g. java @classPathArgs vct.main.Main MyInputFile.java, so there's a good chance we can make it work.

bobismijnnaam commented 1 year ago

@JLedelay For now you can use the following workaround:

Run an sbt server in the vercors project folder by executing sbt there and leaving it open
Instead of using the bin script, use sbt --client run ...your args.... I think for this to work you need to be in the vercors project directory, though, so you might need to change your arguments a bit.

The --client flag causes sbt to look for an sbt server that's running on the current project. On my laptop this takes a second or so, but since your verification time is (sadly :( ) often > 30s, that might be acceptable for now

The only downside is that flags like --help don't work properly anymore. But you were just passing files to vercors, right? So that shouldn't be a problem. This way you can probably also integrate it with the original script you had.

@niomaster I remember you suggesting this method a year ago or so. Maybe we should move to this method officially? The bin script has been annoying since... Forever. We can replace the bin scripts to just use "sbt run", and people who want a faster script can then use the server mode of sbt somehow, maybe?

EDIT: We do need to do something about that --help problem, though. That's annoying.

pieter-bos commented 1 year ago

No, sbt run fiddles with e.g. the logging configuration, so I prefer not to recommend that method in general.

The classpath file does seems promising, though.

pieter-bos commented 1 year ago

As of switching to mill we use a classpath argument file. Additionally, the classpath is always updated before running VerCors (with mill this is very efficient)

utwente-fmt / vercors

The classpath is often too long for development builds on windows #986