From 177d8efa8c9d9259d9baf0872a74927f4bb2f5a3 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 7 May 2024 12:48:20 +0200 Subject: [PATCH 1/7] add inox as a submodule --- .gitmodules | 3 +++ build.sbt | 3 +-- inox | 1 + 3 files changed, 5 insertions(+), 2 deletions(-) create mode 100644 .gitmodules create mode 160000 inox diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 000000000..107c71097 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "inox"] + path = inox + url = https://github.com/epfl-lara/inox.git diff --git a/build.sbt b/build.sbt index a96b43eb0..0a73a243c 100644 --- a/build.sbt +++ b/build.sbt @@ -277,8 +277,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 000000000..9fdb4d494 --- /dev/null +++ b/inox @@ -0,0 +1 @@ +Subproject commit 9fdb4d494133595fd832584e8aaa64b3f027fbab From 7f34caaeeac902a9f452cd619307943c05dff311 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 7 May 2024 13:06:22 +0200 Subject: [PATCH 2/7] fix deprecated syntax in StainlessPlugin.scala --- .../lara/sbt/stainless/StainlessPlugin.scala | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) 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 7ed8d3bf6..bd5c0fc73 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[? >: (State => State) & Seq[MavenRepository] <: State & Int => java.io.Serializable]] = 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) } From afac66a7c17efe6c07ddd847596b2752c3c0af44 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 7 May 2024 13:10:05 +0200 Subject: [PATCH 3/7] wrong return type for def globalSettings in StainlessPlugin.scala --- .../main/scala/ch/epfl/lara/sbt/stainless/StainlessPlugin.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 bd5c0fc73..2711c4591 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 @@ -36,7 +36,7 @@ object StainlessPlugin extends sbt.AutoPlugin { */ private val StainlessLibSources = config("stainless-lib").hide - override def globalSettings: Seq[Def.Setting[? >: (State => State) & Seq[MavenRepository] <: State & Int => java.io.Serializable]] = Seq( + override def globalSettings: Seq[Def.Setting[?]] = Seq( onLoad := onLoad.value andThen checkProjectsScalaVersion, stainlessExtraResolvers ++= Resolver.sonatypeOssRepos("snapshots") ) From 894f6e176e803fba55dc1165e20c7221eb49241f Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 7 May 2024 13:26:00 +0200 Subject: [PATCH 4/7] empty --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 65cfb2532..772b8472f 100644 --- a/README.md +++ b/README.md @@ -140,3 +140,4 @@ on program transformations and soundness of both contract and termination checki [nightly-larabot-ref]: http://laraquad4.epfl.ch:9000/epfl-lara/stainless/builds [release-img]: https://img.shields.io/github/release-pre/epfl-lara/stainless.svg [tag-date-img]: https://img.shields.io/github/release-date-pre/epfl-lara/stainless.svg?style=popout + From 70292d0d35193bb97c33ae6ebc2e2112f09a4277 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 7 May 2024 13:40:52 +0200 Subject: [PATCH 5/7] make inox submodule tracking main branch --- .gitmodules | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitmodules b/.gitmodules index 107c71097..7e902b8c9 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,4 @@ [submodule "inox"] path = inox url = https://github.com/epfl-lara/inox.git + branch = main From 0f756b9172676bfde6e8a182c5af85a2ec5b9362 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 7 May 2024 13:46:40 +0200 Subject: [PATCH 6/7] empty --- README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/README.md b/README.md index 772b8472f..65cfb2532 100644 --- a/README.md +++ b/README.md @@ -140,4 +140,3 @@ on program transformations and soundness of both contract and termination checki [nightly-larabot-ref]: http://laraquad4.epfl.ch:9000/epfl-lara/stainless/builds [release-img]: https://img.shields.io/github/release-pre/epfl-lara/stainless.svg [tag-date-img]: https://img.shields.io/github/release-date-pre/epfl-lara/stainless.svg?style=popout - From 003cea7ed17f5517894e1dece9149a447f53ae6a Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Tue, 7 May 2024 14:00:20 +0200 Subject: [PATCH 7/7] add note about submodules in the readme --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index 65cfb2532..597b5b4b0 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. + ## Quick start We test mostly on [Ubuntu](https://ubuntu.com/download); on [Windows](https://www.microsoft.com/eb-gb/software-download/windows10), you can get sufficient text-based Ubuntu environment by installing [Windows Subsystem for Linux](https://learn.microsoft.com/en-us/windows/wsl/install) (e.g. `wsl --install`, then `wsl --install -d ubuntu`). Ensure you have a [Java](https://openjdk.org/projects/jdk/17/) version ready (it can be headless); on Ubuntu `sudo apt install openjdk-17-jdk-headless` suffices.