forked from epfl-lara/stainless
-
Notifications
You must be signed in to change notification settings - Fork 0
/
build.sbt
304 lines (257 loc) · 11.9 KB
/
build.sbt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
import sbt.ScriptedPlugin
enablePlugins(GitVersioning)
git.baseVersion in ThisBuild := "0.1.0"
git.formattedShaVersion in ThisBuild := git.gitHeadCommit.value map { sha => s"${git.baseVersion.value}-${sha}" }
val osInf = Option(System.getProperty("os.name")).getOrElse("")
val isUnix = osInf.indexOf("nix") >= 0 || osInf.indexOf("nux") >= 0
val isWindows = osInf.indexOf("Win") >= 0
val isMac = osInf.indexOf("Mac") >= 0
val osName = if (isWindows) "win" else if (isMac) "mac" else "unix"
val osArch = System.getProperty("sun.arch.data.model")
val inoxVersion = "1.1.0-114-g364d067"
val dottyVersion = "0.1.1-bin-20170429-10a2ce6-NIGHTLY"
lazy val nParallel = {
val p = System.getProperty("parallel")
if (p ne null) {
try {
p.toInt
} catch {
case nfe: NumberFormatException => 1
}
} else {
1
}
}
val SupportedScalaVersions = Seq("2.11.8")
lazy val frontendClass = settingKey[String]("The name of the compiler wrapper used to extract stainless trees")
// FIXME @nv: dotty compiler needs the scala-library and dotty-library (and maybe some other
// dependencies?) so we set them here through stainless' compile-time dependencies.
lazy val extraClasspath = taskKey[String]("Classpath extensions passed directly to the underlying compiler")
lazy val scriptPath = taskKey[String]("Classpath used in the stainless Bash script")
lazy val baseSettings: Seq[Setting[_]] = Seq(
organization := "ch.epfl.lara",
licenses := Seq("AGPL-V3" -> url("https://www.gnu.org/licenses/agpl-3.0.html"))
)
lazy val artifactSettings: Seq[Setting[_]] = baseSettings ++ Seq(
scalaVersion := crossScalaVersions.value.head,
crossScalaVersions := SupportedScalaVersions
)
lazy val commonSettings: Seq[Setting[_]] = artifactSettings ++ Seq(
scalacOptions ++= Seq(
"-deprecation",
"-unchecked",
"-feature"
),
scalacOptions in (Compile, doc) ++= Seq("-doc-root-content", baseDirectory.value+"/src/main/scala/root-doc.txt"),
unmanagedJars in Runtime += {
root.base / "unmanaged" / s"scalaz3-$osName-$osArch-${scalaBinaryVersion.value}.jar"
},
resolvers ++= Seq(
"Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots",
"Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases",
"uuverifiers" at "http://logicrunch.it.uu.se:4096/~wv/maven",
Resolver.typesafeIvyRepo("releases")
),
libraryDependencies ++= Seq(
"ch.epfl.lara" %% "inox" % inoxVersion,
"ch.epfl.lara" %% "inox" % inoxVersion % "test" classifier "tests",
"ch.epfl.lara" %% "cafebabe" % "1.2",
"org.scalatest" %% "scalatest" % "3.0.1" % "test",
"io.circe" %% "circe-core" % "0.8.0",
"io.circe" %% "circe-generic" % "0.8.0",
"io.circe" %% "circe-parser" % "0.8.0"
),
concurrentRestrictions in Global += Tags.limit(Tags.Test, nParallel),
sourcesInBase in Compile := false,
Keys.fork in run := true,
testOptions in Test := Seq(Tests.Argument("-oDF")),
testOptions in IntegrationTest := Seq(Tests.Argument("-oDF"))
)
lazy val libraryFiles: Seq[(String, File)] = {
val libFiles = ((root.base / "frontends" / "library") ** "*.scala").get
val dropCount = (libFiles.head.getPath indexOfSlice "library") + ("library".size + 1 /* for separator */)
libFiles.map(file => (file.getPath drop dropCount, file)) // Drop the prefix of the path (i.e. everything before "library")
}
lazy val commonFrontendSettings: Seq[Setting[_]] = Defaults.itSettings ++ Seq(
libraryDependencies ++= Seq(
"ch.epfl.lara" %% "inox" % inoxVersion % "it" classifier "tests" classifier "it",
"org.scalatest" %% "scalatest" % "3.0.1" % "it" // FIXME: Does this override `% "test"` from commonSettings above?
),
/**
* NOTE: IntelliJ seems to have trouble including sources located outside the base directory of an
* sbt project. You can temporarily disable the following four lines when importing the project.
*/
unmanagedResourceDirectories in IntegrationTest += (root.base / "frontends" / "benchmarks"),
unmanagedSourceDirectories in Compile += (root.base.getAbsoluteFile / "frontends" / "common" / "src" / "main" / "scala"),
unmanagedSourceDirectories in Test += (root.base.getAbsoluteFile / "frontends" / "common" / "src" / "test" / "scala"),
unmanagedSourceDirectories in IntegrationTest += (root.base.getAbsoluteFile / "frontends" / "common" / "src" / "it" / "scala"),
// We have to use managed resources here to keep sbt's source watcher happy
resourceGenerators in Compile += Def.task {
for ((libPath, libFile) <- libraryFiles) yield {
val resourceFile = (resourceManaged in Compile).value / libPath
println(resourceFile)
IO.write(resourceFile, IO.read(libFile))
resourceFile
}
}.taskValue,
test in assembly := {}, // Skip the test during assembly
sourceGenerators in Compile += Def.task {
val main = (sourceManaged in Compile).value / "stainless" / "Main.scala"
def removeSlashU(in: String): String =
in.replaceAll("\\\\" + "u", "\\\\\"\"\"+\"\"\"u")
.replaceAll("\\\\" + "U", "\\\\\"\"\"+\"\"\"U")
println(libraryFiles)
IO.write(main,
s"""|package stainless
|
|object Main extends MainHelpers {
|
| private val extraCompilerArguments = List("-classpath", "${extraClasspath.value}")
|
| private val libraryPaths = List(
| ${removeSlashU(libraryFiles.map(_._1).mkString("\"\"\"", "\"\"\",\n \"\"\"", "\"\"\""))}
| )
|
| override val factory = new frontends.${frontendClass.value}.Factory(extraCompilerArguments, libraryPaths)
|
|}""".stripMargin)
Seq(main)
}) ++
inConfig(IntegrationTest)(Defaults.testTasks ++ Seq(
logBuffered := (nParallel > 1),
parallelExecution := (nParallel > 1)
))
val scriptSettings: Seq[Setting[_]] = Seq(
extraClasspath := {
((classDirectory in Compile).value.getAbsolutePath +: (dependencyClasspath in Compile).value.map(_.data.absolutePath))
.mkString(System.getProperty("path.separator")).replace("\\", "\\\\")
}
)
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
//lazy val inox = RootProject(file("../inox"))
//lazy val dotty = ghProject("git://github.com/lampepfl/dotty.git", "b3194406d8e1a28690faee12257b53f9dcf49506")
// Allow integration test to use facilities from regular tests
lazy val IntegrationTest = config("it") extend(Test)
lazy val `stainless-core` = (project in file("core"))
.disablePlugins(AssemblyPlugin)
.settings(name := "stainless-core")
.settings(commonSettings, publishMavenSettings)
.settings(site.settings)
.settings(site.sphinxSupport())
//.dependsOn(inox % "compile->compile;test->test")
lazy val `stainless-library` = (project in file("frontends") / "library")
.disablePlugins(AssemblyPlugin)
.settings(
name := "stainless-library",
// don't publish binaries - stainless-library is only consumed as a sources component
publishArtifact in packageBin := false,
crossVersion := CrossVersion.full,
scalaSource in Compile := baseDirectory.value
)
.settings(commonSettings, publishMavenSettings)
lazy val `stainless-scalac` = (project in file("frontends") / "scalac")
.enablePlugins(JavaAppPackaging)
.settings(
name := "stainless-scalac",
frontendClass := "scalac.ScalaCompiler",
extraClasspath := "", // no need for the classpath extension with scalac
libraryDependencies += "org.scala-lang" % "scala-compiler" % scalaVersion.value,
assemblyOption in assembly := (assemblyOption in assembly).value.copy(includeScala = false),
assemblyExcludedJars in assembly := {
val cp = (fullClasspath in assembly).value
// Don't include scalaz3 dependency because it is OS dependent
cp filter {_.data.getName.startsWith("scalaz3")}
},
publish := (),
skip in publish := true // following https://github.com/sbt/sbt-assembly#q-despite-the-concerned-friends-i-still-want-publish-fat-jars-what-advice-do-you-have
)
.dependsOn(`stainless-core`)
//.dependsOn(inox % "test->test;it->test,it")
.configs(IntegrationTest)
.settings(commonSettings, commonFrontendSettings, scriptSettings)
// Following https://github.com/sbt/sbt-assembly#q-despite-the-concerned-friends-i-still-want-publish-fat-jars-what-advice-do-you-have
lazy val `stainless-scalac-plugin` = (project in file("frontends") / "stainless-scalac-plugin")
.settings(
name := "stainless-scalac-plugin",
crossVersion := CrossVersion.full, // because compiler api is not binary compatible
packageBin in Compile := (assembly in (`stainless-scalac`, Compile)).value
)
.settings(artifactSettings, publishMavenSettings)
lazy val `stainless-dotty-frontend` = (project in file("frontends") / "dotty")
.disablePlugins(AssemblyPlugin)
.settings(name := "stainless-dotty-frontend")
.dependsOn(`stainless-core`)
.settings(libraryDependencies += "ch.epfl.lamp" % "dotty_2.11" % dottyVersion % "provided")
.settings(commonSettings, publishMavenSettings)
lazy val `stainless-dotty` = (project in file("frontends") / "stainless-dotty")
.enablePlugins(JavaAppPackaging)
.disablePlugins(AssemblyPlugin)
.settings(
name := "stainless-dotty",
frontendClass := "dotc.DottyCompiler")
.dependsOn(`stainless-dotty-frontend`)
// Should truly depend on dotty, overriding the "provided" modifier above:
.settings(libraryDependencies += "ch.epfl.lamp" % "dotty_2.11" % dottyVersion)
.aggregate(`stainless-dotty-frontend`)
//.dependsOn(inox % "test->test;it->test,it")
.configs(IntegrationTest)
.settings(commonSettings, commonFrontendSettings, artifactSettings, scriptSettings, publishMavenSettings)
lazy val `sbt-stainless` = (project in file("sbt-plugin"))
.enablePlugins(BuildInfoPlugin)
.settings(baseSettings)
.settings(publishSbtSettings)
.settings(
description := "Plugin integrating Stainless in sbt.",
sbtPlugin := true,
// Could also add support for sbt "1.1.0" but a compatibility layer needs to be added to compile against both sbt 0.13 and 1
crossSbtVersions := Vector("0.13.13"),
buildInfoUsePackageAsPath := true,
buildInfoPackage := "ch.epfl.lara.sbt.stainless",
buildInfoKeys := Seq[BuildInfoKey](
BuildInfoKey.map(version) { case (_, v) => "stainlessVersion" -> v },
"supportedScalaVersions" -> SupportedScalaVersions
)
)
.settings(scriptedSettings)
.settings(
scriptedDependencies := {
publishLocal.value
(publishLocal in `stainless-library`).value
(publishLocal in `stainless-scalac-plugin`).value
}
)
def scriptedSettings: Seq[Setting[_]] = ScriptedPlugin.scriptedSettings ++
Seq(
scripted := scripted.tag(Tags.Test).evaluated,
scriptedLaunchOpts ++= Seq(
"-Xmx768m",
"-XX:MaxMetaspaceSize=384m",
"-Dplugin.version=" + version.value,
"-Dscala.version=" + sys.props.get("scripted.scala.version").getOrElse((scalaVersion in `stainless-scalac`).value)
),
scriptedBufferLog := false
)
lazy val root = (project in file("."))
.disablePlugins(AssemblyPlugin)
.settings(artifactSettings)
.settings(
sourcesInBase in Compile := false,
// Don't publish root project
publishArtifact := false,
publish := ()
)
.dependsOn(`stainless-scalac`, `stainless-library`, `stainless-dotty`, `sbt-stainless`)
.aggregate(`stainless-core`, `stainless-library`, `stainless-scalac`, `stainless-dotty`, `sbt-stainless`, `stainless-scalac-plugin`)
def commonPublishSettings = Seq(
bintrayOrganization := Some("epfl-lara")
)
// by default sbt-bintray publishes all sbt plugins in Ivy style
def publishSbtSettings = commonPublishSettings ++ Seq(
bintrayRepository := "sbt-plugins"
)
// by default sbt-bintray publishes all artifacts but sbt plugins in Maven style
def publishMavenSettings = commonPublishSettings ++ Seq(
bintrayRepository := "maven"
)
// FIXME assembly should be disabled at the top level, but isn't
// FIXME assembly is not compatible with dotty -- some conflict with scala versions?