Merge pull request #128 from jad-hamza/allow-insecure

Allow Insecure Protocol to prevent warnings during build and upgrade to Scala 2.12.13 / sbt 1.3.0

.gitignore

@@ -59,3 +59,10 @@ out-classes
 
 # VS Code
 .vscode
+
+# metals and bloop
+.bloop/
+.bsp/
+project/.bloop/
+project/metals.sbt
+project/project/

.larabot.conf

@@ -1,7 +1,7 @@
 commands = [
+    "sbt -batch ++2.12.13 test"
+    "sbt -batch ++2.12.13 it:test"
     "sbt -batch ++2.11.8 test"
-    "sbt -batch ++2.11.8 it:test"
-    "sbt -batch ++2.12.1 test"
 ]
 
 trusted = [

build.sbt

@@ -1,14 +1,14 @@
 name := "inox"
 
-enablePlugins(GitVersioning, TutPlugin)
+enablePlugins(GitVersioning, MdocPlugin)
 
 git.useGitDescribe := true
 
 organization := "ch.epfl.lara"
 
-scalaVersion := "2.12.8"
+scalaVersion := "2.12.13"
 
-crossScalaVersions := Seq("2.11.8", "2.12.8")
+crossScalaVersions := Seq("2.11.8", "2.12.13")
 
 scalacOptions ++= Seq(
   "-deprecation",
@@ -33,7 +33,7 @@ unmanagedJars in Compile += {
 resolvers ++= Seq(
   "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots",
   "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases",
-  "uuverifiers" at "http://logicrunch.research.it.uu.se/maven"
+  ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven").withAllowInsecureProtocol(true)
 )
 
 libraryDependencies ++= Seq(
@@ -103,10 +103,11 @@ sourceGenerators in Compile += Def.task {
 
 lazy val genDoc = taskKey[Unit]("Typecheck and interpret the documentation")
 
-tutSourceDirectory := sourceDirectory.value / "main" / "doc"
-tutTargetDirectory := baseDirectory.value / "doc"
+mdocIn  := sourceDirectory.value / "main" / "doc"
+mdocOut := baseDirectory.value / "doc"
+mdocExtraArguments := Seq("--no-link-hygiene")
 
-genDoc := { tutQuick.value; () }
+genDoc := { () }
 genDoc := (genDoc dependsOn (compile in Compile)).value
 
 Keys.fork in run := true

doc/API.md

@@ -1,7 +1,7 @@
 Inox API
 ========
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Trees
 -----

doc/interpolations.md

@@ -1,7 +1,7 @@
 Inox String Interpolation
 =========================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 # Table of Content
 
@@ -44,26 +44,24 @@ import inox._
 import inox.trees._
 import inox.trees.interpolator._
 
-implicit val symbols: trees.Symbols = trees.NoSymbols
+implicit val symbols: inox.trees.Symbols = inox.trees.NoSymbols
 ```
 
 Once imported, it is possible to build Inox types and expressions using a friendlier syntax:
 
 ```scala
-scala> val tpe = t"Boolean"
-tpe: inox.trees.interpolator.trees.Type = Boolean
-
-scala> val expr = e"1 + 1 == 2"
-expr: inox.trees.interpolator.trees.Expr = 1 + 1 == 2
+val tpe = t"Boolean"
+// tpe: Type = Boolean
+val expr = e"1 + 1 == 2"
+// expr: Expr = 1 + 1 == 2
 ```
 
 It is also possible to embed types and expressions:
 
 ```scala
-scala> e"let x: $tpe = $expr in !x"
-res0: inox.trees.interpolator.trees.Expr =
-val x: Boolean = 1 + 1 == 2
-¬x
+e"let x: $tpe = $expr in !x"
+// res0: Expr = val x: Boolean = 1 + 1 == 2
+// ¬x
 ```
 
 <a name="syntax"></a>
@@ -76,62 +74,61 @@ val x: Boolean = 1 + 1 == 2
 ### Boolean literals
 
 ```scala
-scala> e"true"
-res1: inox.trees.interpolator.trees.Expr = true
-
-scala> e"false"
-res2: inox.trees.interpolator.trees.Expr = false
+e"true"
+// res1: Expr = true
+e"false"
+// res2: Expr = false
 ```
 
 <a name="numeric-literals"></a>
 ### Numeric literal
 
 ```scala
-scala> e"1"
-res3: inox.trees.interpolator.trees.Expr = 1
+e"1"
+// res3: Expr = 1
 ```
 
 Note that the type of numeric expressions is inferred. In case of ambiguity, `BigInt` is chosen by default.
 
 ```scala
-scala> e"1".getType
-res4: inox.trees.interpolator.trees.Type = BigInt
+e"1".getType
+// res4: Type = BigInt
 ```
 
 It is however possible to annotate the desired type.
 
 ```scala
-scala> e"1 : Int".getType
-res5: inox.trees.interpolator.trees.Type = Int
+e"1 : Int".getType
+// res5: Type = Int
 ```
 
 ```scala
-scala> e"1 : Real".getType
-res6: inox.trees.interpolator.trees.Type = Real
+e"1 : Real".getType
+// res6: Type = Real
 ```
 
 <a name="real-literals"></a>
 #### Real literals
 
 ```scala
-scala> e"3.75"
-res7: inox.trees.interpolator.trees.Expr = 15/4
+e"3.75"
+// res7: Expr = 15/4
 ```
 
 <a name="string-literals"></a>
 ### String literals
 
 ```scala
-scala> e"'Hello world!'"
-res8: inox.trees.interpolator.trees.Expr = "Hello world!"
+e"'Hello world!'"
+// res8: Expr = "Hello world!"
 ```
 
 <a name="character-literals"></a>
 ### Character literals
 
 ```scala
-scala> e"`a`"
-res9: inox.trees.interpolator.trees.Expr = 'a'
+e"`a`"
+// res9: Expr = 'a'
 ```
 
 <a name="arithmetic"></a>
@@ -140,53 +137,51 @@ res9: inox.trees.interpolator.trees.Expr = 'a'
 Arithmetic operators are infix and have there usual associativity and priority.
 
 ```scala
-scala> e"1 + 2 * 5 + 6 - 7 / 17"
-res10: inox.trees.interpolator.trees.Expr = ((1 + 2 * 5) + 6) - 7 / 17
+e"1 + 2 * 5 + 6 - 7 / 17"
+// res10: Expr = ((1 + 2 * 5) + 6) - 7 / 17
 ```
 
 <a name="conditionals"></a>
 ## Conditionals
 
 ```scala
-scala> e"if (1 == 2) 'foo' else 'bar'"
-res11: inox.trees.interpolator.trees.Expr =
-if (1 == 2) {
-  "foo"
-} else {
-  "bar"
-}
+e"if (1 == 2) 'foo' else 'bar'"
+// res11: Expr = if (1 == 2) {
+//   "foo"
+// } else {
+//   "bar"
+// }
 ```
 
 <a name="let-bindings"></a>
 ## Let bindings
 
 ```scala
-scala> e"let word: String = 'World!' in concatenate('Hello ', word)"
-res12: inox.trees.interpolator.trees.Expr =
-val word: String = "World!"
-"Hello " + word
+e"let word: String = 'World!' in concatenate('Hello ', word)"
+// res12: Expr = val word: String = "World!"
+// "Hello " + word
 ```
 
 <a name="lambda-expressions"></a>
 ## Lambda expressions
 
 ```scala
-scala> e"lambda x: BigInt, y: BigInt. x + y"
-res13: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y
+e"lambda x: BigInt, y: BigInt. x + y"
+// res13: Expr = (x: BigInt, y: BigInt) => x + y
 ```
 
 It is also possible to use the Unicode `λ` symbol.
 
 ```scala
-scala> e"λx: BigInt, y: BigInt. x + y"
-res14: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y
+e"λx: BigInt, y: BigInt. x + y"
+// res14: Expr = (x: BigInt, y: BigInt) => x + y
 ```
 
 Type annotations can be omitted for any of the parameters if their type can be inferred.
 
 ```scala
-scala> e"lambda x. x * 0.5"
-res15: inox.trees.interpolator.trees.Expr = (x: Real) => x * 1/2
+e"lambda x. x * 0.5"
+// res15: Expr = (x: Real) => x * 1/2
 ```
 
 <a name="quantifiers"></a>
@@ -196,33 +191,30 @@ res15: inox.trees.interpolator.trees.Expr = (x: Real) => x * 1/2
 ### Universal Quantifier
 
 ```scala
-scala> e"forall x: Int. x > 0"
-res16: inox.trees.interpolator.trees.Expr = ∀x: Int. (x > 0)
-
-scala> e"∀x. x || true"
-res17: inox.trees.interpolator.trees.Expr = ∀x: Boolean. (x || true)
+e"forall x: Int. x > 0"
+// res16: Expr = ∀x: Int. (x > 0)
+e"∀x. x || true"
+// res17: Expr = ∀x: Boolean. (x || true)
 ```
 
 <a name="existential-quantifiers"></a>
 ### Existential Quantifier
 
 ```scala
-scala> e"exists x: BigInt. x < 0"
-res18: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt. ¬(x < 0)
-
-scala> e"∃x, y. x + y == 0"
-res19: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt, y: BigInt. (x + y ≠ 0)
+e"exists x: BigInt. x < 0"
+// res18: Expr = ¬∀x: BigInt. ¬(x < 0)
+e"∃x, y. x + y == 0"
+// res19: Expr = ¬∀x: BigInt, y: BigInt. (x + y ≠ 0)
 ```
 
 <a name="choose"></a>
 ## Choose
 
 ```scala
-scala> e"choose x. x * 3 < 17"
-res20: inox.trees.interpolator.trees.Expr = choose((x: BigInt) => x * 3 < 17)
-
-scala> e"choose x: String. true"
-res21: inox.trees.interpolator.trees.Expr = choose((x: String) => true)
+e"choose x. x * 3 < 17"
+// res20: Expr = choose((x: BigInt) => x * 3 < 17)
+e"choose x: String. true"
+// res21: Expr = choose((x: String) => true)
 ```
 
 <a name="primitives"></a>

doc/trees.md

@@ -1,7 +1,7 @@
 Extending the Trees
 ===================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Inox trees are designed to be extensible with minimal pain and maximal gain.
 By extending the [```Trees```](/src/main/scala/inox/ast/Trees.scala) trait,
@@ -158,7 +158,7 @@ interfaces for such cases:
 It is sometimes useful to have a bidirectional translation between two sorts of trees.
 Inox provides a mechanism to maintain an encoder/decoder pair alongside a pair of
 source and target programs through an instance of
-[ProgramTransformer](/src/main/scala/inox/ast/ProgramEncoder.scala).
+[ProgramTransformer](/src/main/scala/inox/transformers/ProgramTransformer.scala).
 
 ## Providing new semantics
 

doc/tutorial.md

@@ -1,7 +1,7 @@
 Tutorial
 ========
 
-[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Let us consider the problem of checking whether the following size function on a list is always greater or equal to 0.
 ```scala
@@ -25,8 +25,8 @@ import inox.solvers._
 
 The explanation is the following:
 - `inox._` imports [`InoxProgram` and many others](/src/main/scala/inox/package.scala#L19)
-- `inox.trees._` imports the content of the default implementation [`trees`](/src/main/scala/inox/package.scala#L58) extending [`Trees`](/src/main/scala/inox/ast/Trees.scala#L10).
-- `inox.trees.dsl._` imports the [domain-specific-language helpers](/src/main/scala/inox/ast/DSL.scala#L20) to create [`trees`](/src/main/scala/inox/package.scala#L58) expressions.
+- `inox.trees._` imports the content of the default implementation [`trees`](/src/main/scala/inox/package.scala#L53) extending [`Trees`](/src/main/scala/inox/ast/Trees.scala#L10).
+- `inox.trees.dsl._` imports the [domain-specific-language helpers](/src/main/scala/inox/ast/DSL.scala#L20) to create [`trees`](/src/main/scala/inox/package.scala#L53) expressions.
 - `inox.solvers._` imports the [solvers](/src/main/scala/inox/solvers/package.scala#L8).
 
 ## Creating the Symbol Table
@@ -157,7 +157,7 @@ val sizeFunction = mkFunDef(size)("A") { case Seq(tp) => (
 
 A symbol table in Inox is an instance of `Symbols`. The easiest way to construct one is to use
 ```scala
-implicit val symbols: trees.Symbols = {
+implicit val symbols: inox.trees.Symbols = {
   NoSymbols
     .withFunctions(Seq(sizeFunction))
     .withSorts(Seq(listSort))

project/build.properties

@@ -1 +1 @@
-sbt.version=1.2.8
+sbt.version=1.3.0

project/plugins.sbt

@@ -1,5 +1,5 @@
 
-addSbtPlugin("org.tpolecat" % "tut-plugin" % "0.6.11")
+addSbtPlugin("org.scalameta" % "sbt-mdoc" % "2.2.18")
 
 addSbtPlugin("com.typesafe.sbt" % "sbt-git" % "1.0.0")
 

src/main/doc/API.md

@@ -1,7 +1,7 @@
 Inox API
 ========
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Trees
 -----