0.7.1 regression: exception when building projects on windows 10 x64

[mwookawa]

I'm currently using the 0.7.1 stainless jar release resulting from a publishLocal on Windows (have also tried a set of build artifacts built on MacOS). The 'tester' project referenced below was produced via

sbt new epfl-lara/stainless-project.g8

sbt gives me the following new error that was is not present when building with 0.7.0 artifacts.

I've duplicated this on win10 installs with different service packs as well as with jdk 1.8 and jdk 11.

mingk@nomcase MINGW64 ~/tmp/tester $ /c/Users/mingk/Downloads/sbt-1.3.0/sbt/bin/sbt.bat core/run [info] Loading settings for project tester-build from metals.sbt,plugins.sbt ... [info] Loading project definition from C:\Users\mingk\tmp\tester\project [info] Loading settings for project tester from build.sbt ... [info] Set current project to tester (in build file:/C:/Users/mingk/tmp/tester/) [info] Compiling 31 Scala sources to C:\Users\mingk\tmp\tester\verified\target\scala-2.12\classes ... [error] Stainless terminated with an error. [error] Debug output is available in the file stainless-stack-trace.txt, you may report your issue on https://github.com/epfl-lara/stainless/issues [error] You may use --debug=frontend to have the stack trace displayed in the output. 2020-06-23 15:28:12,491 shutdown-hooks-run-all ERROR No Log4j 2 configuration file found. Using default configuration (logging only errors to the console), or user programmatically provided configurations. Set system property 'log4j2.debug' to show Log4j 2 internal initialization logging. See https://logging.apache.org/log4j/2.x/manual/configuration.html for instructions on how to configure Log4j 2

The contents of stainless-stack-trace.txt are below.

java.lang.IllegalArgumentException: Invalid prefix or suffix at java.base/java.nio.file.TempFileHelper.generatePath(TempFileHelper.java:62) at java.base/java.nio.file.TempFileHelper.create(TempFileHelper.java:126) at java.base/java.nio.file.TempFileHelper.createTempFile(TempFileHelper.java:160) at java.base/java.nio.file.Files.createTempFile(Files.java:912) at stainless.frontend.FrontendFactory.$anonfun$libraryFiles$2(FrontendFactory.scala:34) at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238) at scala.collection.immutable.List.foreach(List.scala:392) at scala.collection.TraversableLike.map(TraversableLike.scala:238) at scala.collection.TraversableLike.map$(TraversableLike.scala:231) at scala.collection.immutable.List.map(List.scala:298) at stainless.frontend.FrontendFactory.libraryFiles(FrontendFactory.scala:19) at stainless.frontend.FrontendFactory.libraryFiles$(FrontendFactory.scala:19) at stainless.frontends.scalac.ScalaCompiler$Factory.libraryFiles$lzycompute(ScalaCompiler.scala:135) at stainless.frontends.scalac.ScalaCompiler$Factory.libraryFiles(ScalaCompiler.scala:135) at stainless.MainHelpers.libraryFiles(MainHelpers.scala:103) at stainless.MainHelpers.libraryFiles$(MainHelpers.scala:103) at stainless.Main$.libraryFiles$lzycompute(Main.scala:3) at stainless.Main$.libraryFiles(Main.scala:3) at stainless.frontends.scalac.CodeExtraction.extractUnit(CodeExtraction.scala:66) at stainless.frontends.scalac.CodeExtraction.extractUnit$(CodeExtraction.scala:44) at stainless.frontends.scalac.StainlessPluginComponent.extractUnit(StainlessPlugin.scala:86) at stainless.frontends.scalac.StainlessExtraction$Phase.apply(StainlessExtraction.scala:39) at scala.tools.nsc.Global$GlobalPhase.applyPhase(Global.scala:453) at scala.tools.nsc.Global$GlobalPhase.run(Global.scala:399) at stainless.frontends.scalac.StainlessExtraction$Phase.super$run(StainlessExtraction.scala:45) at stainless.frontends.scalac.StainlessExtraction$Phase.$anonfun$run$1(StainlessExtraction.scala:45) at stainless.frontends.scalac.StainlessPluginComponent.onRun(StainlessPlugin.scala:116) at stainless.frontends.scalac.StainlessExtraction$Phase.run(StainlessExtraction.scala:45) at scala.tools.nsc.Global$Run.compileUnitsInternal(Global.scala:1503) at scala.tools.nsc.Global$Run.compileUnits(Global.scala:1487) at scala.tools.nsc.Global$Run.compileSources(Global.scala:1480) at scala.tools.nsc.Global$Run.compile(Global.scala:1606) at xsbt.CachedCompiler0.run(CompilerInterface.scala:148) at xsbt.CachedCompiler0.run(CompilerInterface.scala:123) at xsbt.CompilerInterface.run(CompilerInterface.scala:35) at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.base/java.lang.reflect.Method.invoke(Method.java:566) at sbt.internal.inc.AnalyzingCompiler.call(AnalyzingCompiler.scala:252) at sbt.internal.inc.AnalyzingCompiler.compile(AnalyzingCompiler.scala:121) at sbt.internal.inc.AnalyzingCompiler.compile(AnalyzingCompiler.scala:94) at sbt.internal.inc.bloop.internal.BloopHighLevelCompiler.compileSources$1(BloopHighLevelCompiler.scala:142) at sbt.internal.inc.bloop.internal.BloopHighLevelCompiler.$anonfun$compile$7(BloopHighLevelCompiler.scala:160) at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23) at sbt.internal.inc.bloop.internal.BloopHighLevelCompiler.$anonfun$compile$1(BloopHighLevelCompiler.scala:72) at bloop.tracing.BraveTracer.traceInternal(BraveTracer.scala:64) at bloop.tracing.BraveTracer.trace(BraveTracer.scala:38) at sbt.internal.inc.bloop.internal.BloopHighLevelCompiler.timed$1(BloopHighLevelCompiler.scala:71) at sbt.internal.inc.bloop.internal.BloopHighLevelCompiler.$anonfun$compile$6(BloopHighLevelCompiler.scala:160) at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23) at monix.eval.internal.TaskRunLoop$.monix$eval$internal$TaskRunLoop$$loop$1(TaskRunLoop.scala:187) at monix.eval.internal.TaskRunLoop$RestartCallback$1.onSuccess(TaskRunLoop.scala:119) at monix.eval.Task$.$anonfun$forkedUnit$2(Task.scala:1463) at java.base/java.util.concurrent.ForkJoinTask$RunnableExecuteAction.exec(ForkJoinTask.java:1426) at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:290) at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1020) at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1656) at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1594) at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:177)

[jad-hamza]

I tried on Windows on PowerShell and got an error as well. I had other issues like colors not being displayed correctly (known issue for PowerShell). For this issue, it looks like the problem comes from a confusion between \ and / for the paths of files. I tried a fix here https://github.com/epfl-lara/stainless/pull/805 but that seems a bit hacky. Could you see if this works for you @mwookawa ? @romac Any thoughts?

[mwookawa]

i added some comments to the diff of #805. The short of it is that it's hacky but it works. maybe something more robust can be found for 0.7.2, but I can make progress again with the current release. thanks!!

[sfiruch]

FYI: We use the Linux JAR, and place the Windows x64 Z3 executable in the same directory. This works fine on Windows when invoking Stainless with -solvers=smt-z3.