sbt-stainless plugin #176
sbt-stainless plugin #176
Conversation
|
This looks good to me. If think if you rebase and force-push, the CI should hopefully start running on your PRs. I'm not sure I understand about the scalaz3 dependency. Will we have one fat jar per os architecture or is there some way to inject the jar into the classpath later on? And if this is possible, why aren't we doing it for Inox? |
(cherry picked from commit 9ef6e82)
* Created a stainless scalac plugin that can be added to the the compiler pipeline via the compiler option -Xplugin:<path>. * Mind that when using stainless as a compiler plugin no cashing is performed (this because a new compiler Global instance is instantiated every time). This limitation could be fixed by integrating the cache in a custom sbt compiler-bridge - sbt allows to provide your own compiler-bridge via the `scalaCompilerBridgeSource` setting). * The scalac plugin is a "fat" jar because it needs to include all dependencies it needs (e.g., inox and friends). There is in fact no mechanism for including third-party depenencies that are needed by the compiler (i.e., the compiler classpath cannot be easily extended). However, the fact that a "fat" jar is used shouldn't entail any problem because compiler plugins are run in their own classloader, isolated from the compilation classpath. Hence, there is no risk of clushes between the stainless compiler plugin classes included in the "fat" jar and the compilation classpath.
This makes it easier to know the project's current version. Also, the on-development version should either be a SNAPSHOT or generated with the hash appended. Going with the former option because it's a simple change, but you can easily switch to the latter if you'd prefer so.
dotta
force-pushed
the
wip/sbt-plugin
branch
from
5071c7c to
66c7e3c
Compare
Done :)
You are right, we need a stainless-scalac-plugin fat jar per os that includes the z3 dependency. I'll try to work this out now. |
dotta
force-pushed
the
wip/sbt-plugin
branch
from
66c7e3c to
8473d30
Compare
|
@samarion To be able to test that scalaz3 is correctly included in the stainless compiler plugin, I need to be able to run stainless on Mac with it. As this is currently not possible (because of epfl-lara/ScalaZ3#56) I suggest we review and merge the PR as is and we create a ticket for including scalaz3 in the stainles-scalac-plugin fat jar (I've actually pushed a commit with the functionality here dotta@d7748e7, but I can't test it :)). Sounds good? |
| import stainless.lang._ | ||
| import stainless.collection._ | ||
|
|
||
| object ConstructorArgsBoxing1 { |
There was a problem hiding this comment.
You may want to change the successful file here as @dragos robustness PR will break this test case.
You can use frontends/benchmarks/verification/valid/ADTInvariants1.scala instead (for example).
There was a problem hiding this comment.
Oups, I forgot about this comment when hitting approve. Please change this file and then I'll merge.
There was a problem hiding this comment.
Done and force pushed.
* When the `StainlessPlugin` is enabled on a sbt project, it automatically adds the stainless compiler plugin to the compiler. Also, because stainless requires the sources to run the verification, the source directories of the project and the stainless-library-sources.jar are added to the sourcepath. * Because of the above, a `stainless-library` project was created so that the `stainless-library-sources.jar` can be published. * The stainless sbt plugin currently expects that an external solver is installed and available in the $PATH. To remove this limitation a scalaz3 dependency compatible with each supported os/architecture need to be published somewhere. * A scripted test is included to test the sbt-stainless plugin works as expected. * To simplify maintenance the Scala versions that stainless support are passed from the project's build to the sbt-stainless plugin thanks to the sbt-buildinfo plugin. * Currently, the sbt-stainless plugin targets sbt 0.13. However, it should be relatively simple to cross build the plugin against sbt 1 as well. To make this task as simple as possible the version of sbt used by the project was bumped to 0.13.17 (as it contains some important fix for cross building sbt plugins) and the project's build contains a comment hinting at what needs to be done to support sbt 1. * No dotty support.
dotta
force-pushed
the
wip/sbt-plugin
branch
from
8473d30 to
db37108
Compare
Yeah, the sbt-stainless plugin might not yet be bulletproof, but I think it's a good start and it definitely works for the simple case I tested. Let's now have it published so that you/Viktor can test it out. Another aspect we should discuss is if you want the plugin to work with dotty as well (I'm not sure how much work that would be, but hopefully it's not much).
I'm afraid I wouldn't be very productive with this working mode. I think it'd be good to hear from @vkuncak if having scalaz3 working on Mac OS is something he'd want us to do. If so, this can be something we tackle next week. |
This PR adds a sbt-stainless plugin. Please, read the commits message for details.
I expect this PR will fail to execute the scripted test because currently the sbt-stainless plugin requires an external solver to be installed (and I assume that will be missing on the machine running the PR validation). To fix this issue I need a repository to fetch the scalaz3 dependency.