Skip to content

Commit

Permalink
Move Inox as a submodule instead of an http dependency (#1520)
Browse files Browse the repository at this point in the history
* make inox submodule tracking main branch

* fix deprecated syntax in StainlessPlugin.scala

* wrong return type for def globalSettings in StainlessPlugin.scala

* add note about submodules in the readme
  • Loading branch information
samuelchassot authored May 14, 2024
1 parent 924f987 commit d0b07bb
Show file tree
Hide file tree
Showing 5 changed files with 24 additions and 13 deletions.
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

0 comments on commit d0b07bb

Please sign in to comment.