diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000000..7e902b8c95 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,4 @@ +[submodule "inox"] + path = inox + url = https://github.com/epfl-lara/inox.git + branch = main diff --git a/README.md b/README.md index e76b73ad3f..995b0eca27 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,11 @@ Hosted at https://github.com/epfl-lara/stainless ; mirrored at https://gitlab.ep Verification framework for a subset of the [Scala](http://scala-lang.org) programming language. See the [tutorial](https://epfl-lara.github.io/asplos2022tutorial/). +Please note that this repository uses `git submodules`, so you need to either: + +- clone it with the `--recursive` option, or +- run `$ git submodule update --init --recursive` after cloning. + Please note that Stainless does not support Scala 2 frontend anymore but only Scala 3.3. The latest release that does support Scala 2.13 frontend is the [v0.9.8.7](https://github.com/epfl-lara/stainless/releases/tag/v0.9.8.7). ## Quick start diff --git a/build.sbt b/build.sbt index 3bdd0e1a18..1a2c2d81c9 100644 --- a/build.sbt +++ b/build.sbt @@ -275,8 +275,7 @@ val scriptSettings: Seq[Setting[_]] = Seq( def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}")) -// lazy val inox = RootProject(file("../inox")) -lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "3b02dcf4308f9e8d74ea82304bd651be8e93517f") +lazy val inox = RootProject(file("./inox")) lazy val cafebabe = ghProject("https://github.com/epfl-lara/cafebabe.git", "616e639b34379e12b8ac202849de3ebbbd0848bc") // Allow integration test to use facilities from regular tests diff --git a/inox b/inox new file mode 160000 index 0000000000..9fdb4d4941 --- /dev/null +++ b/inox @@ -0,0 +1 @@ +Subproject commit 9fdb4d494133595fd832584e8aaa64b3f027fbab diff --git a/sbt-plugin/src/main/scala/ch/epfl/lara/sbt/stainless/StainlessPlugin.scala b/sbt-plugin/src/main/scala/ch/epfl/lara/sbt/stainless/StainlessPlugin.scala index 7ed8d3bf61..2711c45913 100644 --- a/sbt-plugin/src/main/scala/ch/epfl/lara/sbt/stainless/StainlessPlugin.scala +++ b/sbt-plugin/src/main/scala/ch/epfl/lara/sbt/stainless/StainlessPlugin.scala @@ -6,8 +6,10 @@ import java.nio.file.StandardCopyOption import java.util.stream.Collectors import java.util.zip.ZipFile import java.util.zip.ZipEntry -import sbt._ -import sbt.Keys._ +import sbt.{Def, *} +import sbt.Keys.* + +import java.io object StainlessPlugin extends sbt.AutoPlugin { private val IssueTracker = "https://github.com/epfl-lara/stainless/issues" @@ -26,7 +28,7 @@ object StainlessPlugin extends sbt.AutoPlugin { val stainlessExtraResolvers = settingKey[Seq[sbt.librarymanagement.MavenRepository]]("Extra resolvers to pass along to Stainless") } - import autoImport._ + import autoImport.* /** * An (Ivy) configuration allowing us to manage dependencies outside of the project's classpath. @@ -34,9 +36,9 @@ object StainlessPlugin extends sbt.AutoPlugin { */ private val StainlessLibSources = config("stainless-lib").hide - override def globalSettings = Seq( + override def globalSettings: Seq[Def.Setting[?]] = Seq( onLoad := onLoad.value andThen checkProjectsScalaVersion, - stainlessExtraResolvers := Seq(Resolver.sonatypeRepo("releases")) + stainlessExtraResolvers ++= Resolver.sonatypeOssRepos("snapshots") ) /** @@ -59,9 +61,9 @@ object StainlessPlugin extends sbt.AutoPlugin { state } - override lazy val projectSettings: Seq[Def.Setting[_]] = stainlessSettings + override lazy val projectSettings: Seq[Def.Setting[?]] = stainlessSettings - lazy val stainlessSettings: Seq[sbt.Def.Setting[_]] = Seq( + lazy val stainlessSettings: Seq[sbt.Def.Setting[?]] = Seq( stainlessVersion := BuildInfo.stainlessVersion, stainlessEnabled := true, stainlessExtraDeps := Seq.empty, @@ -98,7 +100,7 @@ object StainlessPlugin extends sbt.AutoPlugin { compilerPlugin(pluginRef) +: sourceDeps } - lazy val stainlessConfigSettings: Seq[Def.Setting[_]] = + lazy val stainlessConfigSettings: Seq[Def.Setting[?]] = Seq( managedSources ++= fetchAndUnzipSourceDeps.value, managedSourceDirectories += stainlessSourcesLocation.value @@ -178,11 +180,11 @@ object StainlessPlugin extends sbt.AutoPlugin { var archive: ZipFile = null try { archive = new ZipFile(jar) - import scala.collection.JavaConverters._ + import scala.collection.JavaConverters.* val entries: List[ZipEntry] = archive.stream().collect(Collectors.toList()).asScala.toList entries foreach { entry => - val entryDest = destPath.resolve(entry.getName()) - if (!entry.isDirectory()) { + val entryDest = destPath.resolve(entry.getName) + if (!entry.isDirectory) { Files.createDirectories(entryDest.getParent) Files.copy(archive.getInputStream(entry), entryDest, StandardCopyOption.REPLACE_EXISTING) }