-
Notifications
You must be signed in to change notification settings - Fork 39
/
build.sbt
189 lines (158 loc) · 8.22 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
import java.io.{FileInputStream, InputStreamReader}
import java.nio.charset.StandardCharsets
import java.nio.file.{Files, Paths}
import java.util.Properties
ThisBuild / scalaVersion := "2.13.13"
ThisBuild / version := "5.1.1"
ThisBuild / scalacOptions ++= Seq(
// Always show all non-suppressed warnings. See `scalac -Wconf:help` for more info.
// https://www.scala-lang.org/2021/01/12/configuring-and-suppressing-warnings.html
"-Wconf:any:w",
"-Ymacro-annotations",
)
ThisBuild / assemblyMergeStrategy := {
// Multiple dependency jars have a module-info.class file in the same location.
// Without custom rules, they cause merge conflicts with sbt-assembly.
// Since we're building an uberjar, it should be safe to discard them (according to stackoverflow).
// https://stackoverflow.com/a/55557287
case PathList(elements @ _*) if elements.last == "module-info.class" => MergeStrategy.discard
// https://github.com/sbt/sbt-assembly#merge-strategy
case path =>
val oldStrategy = (ThisBuild / assemblyMergeStrategy).value
oldStrategy(path)
}
// Never execute tests in parallel across all sub-projects
Global / concurrentRestrictions += Tags.limit(Tags.Test, 1)
lazy val macros = project
.in(file("keymaerax-macros"))
.disablePlugins(AssemblyPlugin)
.settings(
name := "KeYmaeraX Macros",
libraryDependencies += "org.scala-lang" % "scala-reflect" % scalaVersion.value,
)
lazy val core = project
.in(file("keymaerax-core"))
.enablePlugins(BuildInfoPlugin)
.dependsOn(macros)
.settings(
name := "KeYmaeraX Core",
mainClass := Some("org.keymaerax.cli.KeymaeraxCore"),
libraryDependencies += "org.scala-lang" % "scala-compiler" % scalaVersion.value,
libraryDependencies += "cc.redberry" %% "rings.scaladsl" % "2.5.8",
libraryDependencies += "com.github.scopt" %% "scopt" % "4.1.0",
libraryDependencies += "com.lihaoyi" %% "fastparse" % "3.1.0",
libraryDependencies += "io.github.classgraph" % "classgraph" % "4.8.174",
libraryDependencies += "io.spray" %% "spray-json" % "1.3.6",
libraryDependencies += "org.apache.commons" % "commons-configuration2" % "2.10.1",
libraryDependencies += "org.apache.commons" % "commons-lang3" % "3.14.0",
libraryDependencies += "org.reflections" % "reflections" % "0.10.2",
libraryDependencies += "org.typelevel" %% "paiges-core" % "0.4.3",
libraryDependencies += "org.typelevel" %% "spire" % "0.18.0",
// Logging
//
// KeYmaera X and some of its dependencies use slf4j for logging.
// Slf4j is a facade for various logging frameworks called "providers".
// Forcing slf4j 2 usually works fine for dependencies that create logs,
// but forcing an slf4j 1 provider to use slf4j 2 will break things.
// Since some dependencies updated to slf4j 2 already, we have to use an slf4j 2 provider
// and force all other dependencies to use slf4j 2 as well via sbt's default version conflict resolution.
//
// https://github.com/jokade/slogging?tab=readme-ov-file#getting-started
// https://www.baeldung.com/slf4j-with-log4j2-logback#Log4j2
libraryDependencies += "biz.enef" %% "slogging-slf4j" % "0.6.2",
libraryDependencies += "org.apache.logging.log4j" % "log4j-api" % "2.23.1",
libraryDependencies += "org.apache.logging.log4j" % "log4j-core" % "2.23.1",
libraryDependencies += "org.apache.logging.log4j" % "log4j-slf4j2-impl" % "2.23.1",
// A published version of scala-smtlib that works with Scala 2.13
// https://github.com/regb/scala-smtlib/issues/46#issuecomment-955691728
// https://mvnrepository.com/artifact/com.regblanc/scala-smtlib_2.13/0.2.1-42-gc68dbaa
libraryDependencies += "com.regblanc" %% "scala-smtlib" % "0.2.1-42-gc68dbaa",
Compile / run / mainClass := mainClass.value,
assembly / mainClass := mainClass.value,
assembly / assemblyJarName := s"${normalizedName.value}-${version.value}.jar",
// Include version number as constant in source code
buildInfoKeys := Seq[BuildInfoKey](
version,
"copyright" -> Files.readString(Paths.get("COPYRIGHT.txt")),
"license" -> Files.readString(Paths.get("LICENSE.txt")),
"licensesThirdParty" -> Files.readString(Paths.get("LICENSES_THIRD_PARTY.txt")),
),
buildInfoPackage := "org.keymaerax.info",
buildInfoOptions += BuildInfoOption.PackagePrivate,
// Use Mathematica's JLink.jar as unmanaged dependency
// The path is read from the property mathematica.jlink.path in the file local.properties
Compile / unmanagedJars += {
val properties = new Properties()
try {
val stream = new FileInputStream("local.properties")
val reader = new InputStreamReader(stream, StandardCharsets.UTF_8)
properties.load(reader)
} catch {
case e: Throwable => throw new Exception("Failed to load file local.properties", e)
}
val jlinkPath: String = properties.getProperty("mathematica.jlink.path")
if (jlinkPath == null) {
throw new Exception("Property mathematica.jlink.path not found in file local.properties")
}
file(jlinkPath)
},
)
lazy val webui = project
.in(file("keymaerax-webui"))
.dependsOn(macros, core)
.settings(
name := "KeYmaeraX WebUI",
mainClass := Some("org.keymaerax.cli.KeymaeraxWebui"),
/// sqlite driver
libraryDependencies += "com.typesafe.slick" %% "slick" % "3.5.1",
libraryDependencies += "com.typesafe.slick" %% "slick-codegen" % "3.5.1",
libraryDependencies += "org.xerial" % "sqlite-jdbc" % "3.45.3.0",
// Akka
libraryDependencies += "com.typesafe.akka" %% "akka-http" % "10.5.3",
libraryDependencies += "com.typesafe.akka" %% "akka-http-spray-json" % "10.5.3",
libraryDependencies += "com.typesafe.akka" %% "akka-http-xml" % "10.5.3",
libraryDependencies += "com.typesafe.akka" %% "akka-slf4j" % "2.8.5",
libraryDependencies += "com.typesafe.akka" %% "akka-stream" % "2.8.5",
libraryDependencies += "io.spray" %% "spray-json" % "1.3.6",
Compile / run / mainClass := mainClass.value,
assembly / mainClass := mainClass.value,
assembly / assemblyJarName := s"${normalizedName.value}-${version.value}.jar",
// Include some resources as triggers for triggered execution (~)
watchTriggers += baseDirectory.value.toGlob / "src" / "main" / "resources" / "partials" / "*.html",
watchTriggers += baseDirectory.value.toGlob / "src" / "main" / "resources" / "js" / "*.{js,map}",
watchTriggers += baseDirectory.value.toGlob / "src" / "main" / "resources" / "*.html",
/////////////
// Testing //
/////////////
libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % Test,
libraryDependencies += "org.scalamock" %% "scalamock" % "5.2.0" % Test,
// For generating HTML scalatest reports using the `-h <directory>` flag
// See "Using Reporters" in https://www.scalatest.org/user_guide/using_scalatest_with_sbt
// https://stackoverflow.com/a/59059383
// https://github.com/scalatest/scalatest/issues/1736
libraryDependencies += "com.vladsch.flexmark" % "flexmark-all" % "0.64.8" % Test,
Test / parallelExecution := false,
// set fork to true in order to run tests in their own Java process.
// not forking avoids broken pipe exceptions in test reporter, but forking might become necessary in certain
// multithreaded setups (see ScalaTest documentation)
Test / fork := false,
// record and report test durations
Test / testOptions += Tests.Argument(TestFrameworks.ScalaTest, "-oD"),
// report long-running tests (report every hour for tests that run longer than 1hr)
Test / testOptions += Tests.Argument(TestFrameworks.ScalaTest, "-W", "3600", "3600"),
resolvers ++= Resolver.sonatypeOssRepos("snapshots"), // ScalaMeter
testFrameworks += new TestFramework("org.scalameter.ScalaMeterFramework"),
logBuffered := false,
)
// build KeYmaera X full jar with sbt clean assembly
lazy val root = project
.in(file("."))
.aggregate(macros, core, webui)
.enablePlugins(ScalaUnidocPlugin)
.disablePlugins(AssemblyPlugin)
.settings(
name := "KeYmaeraX",
Compile / doc / scalacOptions ++= Seq("-doc-root-content", "rootdoc.txt"),
ScalaUnidoc / unidoc / scalacOptions += "-Ymacro-expand:none",
ScalaUnidoc / unidoc / unidocProjectFilter := inAnyProject -- inProjects(macros),
)