Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

sbt integration #155

Closed
vkuncak opened this issue Dec 20, 2017 · 2 comments
Closed

sbt integration #155

vkuncak opened this issue Dec 20, 2017 · 2 comments
Labels
enhancement help wanted

Comments

@vkuncak
Copy link
Collaborator

vkuncak commented Dec 20, 2017 •
edited
Loading

[Iulian and Mirco]

Enable compilation of projects consisting of ordinary .scala files that are compiled as usual, as well as files with .v.scala double extension that are verified with stainless using the included stainless dependencies and then compiled as usual.
@dragos
Copy link
Contributor

dragos commented Dec 20, 2017 •
edited
Loading

We'll try this first instead of the specific source directory (src/stainless/scala -- configuration in Sbt parlance). The advantage of such configurations is that Sbt can handle dependencies independently from other configurations, so we can stuff additional jars without leaking them into "main" sources. However, I agree that .v.stainless is very nice too.

@ceilican ceilican mentioned this issue Jan 4, 2018
Closed
@ghost
Copy link

ghost commented Jan 11, 2018

There is an sbt plugin developed here: https://github.com/NiceKingWei/sbt-stainless ; it adds a task verify which calls on stainless as if one had called it from the command line. Maybe coordinate with @NiceKingWei ?

dotta added a commit to dotta/stainless that referenced this issue Feb 28, 2018
@dotta
Created sbt-stainless plugin. Fix epfl-lara#155
5071c7c 
* 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 added a commit to dotta/stainless that referenced this issue Feb 28, 2018
@dotta
Created sbt-stainless plugin. Fix epfl-lara#155
66c7e3c 
* 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 added a commit to dotta/stainless that referenced this issue Feb 28, 2018
@dotta
Created sbt-stainless plugin. Fix epfl-lara#155
8473d30 
* 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 dotta mentioned this issue Feb 28, 2018
Open
jad-hamza pushed a commit to jad-hamza/stainless that referenced this issue Feb 28, 2018
@dotta @jad-hamza
Created sbt-stainless plugin. Fix epfl-lara#155
ec9c4b6 
* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement help wanted
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@dragos @vkuncak