search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
359 stars 53 forks source link

Make sbt-stainless work without requiring an external solver #179

Open dotta opened 6 years ago

dotta commented 6 years ago

Currently, sbt-stainless expects an external solver to be installed and available in the $PATH. This because I couldn't make scalaz3 work on OSX (see https://github.com/epfl-lara/ScalaZ3/issues/56).

Once the scalaz3 ticket is resolved, we should publish a stainless-scalac-plugin embedding scalaz3 for each supported os and architecture. This way, sbt-stainless will be usable without having to install an external solver.

I've started working on this ticket in this branch: https://github.com/dotta/stainless/tree/wip/include-scalaz3-in-fat-jar

vkuncak commented 5 years ago

@romac is this still an issue?

romac commented 5 years ago

Not in the sense that we support Princess out of the box, and having z3 support just requires installing Z3. But yeah, we do not currently ship NativeZ3 with the compiler plugin, which we perhaps should?