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.

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

Move Inox as a submodule instead of an http dependency #1520

Merged
merged 8 commits into from
May 14, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
[submodule "inox"]
path = inox
url = https://github.com/epfl-lara/inox.git
branch = main
5 changes: 5 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions inox
Submodule inox added at 9fdb4d
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -26,17 +28,17 @@ 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.
* Using a configurations enables to fetch dependencies via `update` (see the `fetchJars` method).
*/
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")
)

/**
Expand All @@ -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,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
}
Expand Down