diff --git a/CHANGES.md b/CHANGES.md
index 3c8fec63a70518c5abad966eb7a2fd8897c5114f..fdcd76e1021249f88b07d07191063a120a767865 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,8 @@
# Change List
+## 2024-10-03
+Update to Scala 3.5.1. Silence warnings from scallion and other erroneous ones.
+
## 2024-07-22
Resealed the `Proof` trait following a fix of the relevant compiler bug [scala/scala3#19031](https://github.com/scala/scala3/issues/19031).
diff --git a/build.sbt b/build.sbt
index faa922e1e7c8215109d83f2c8c64f552f7c769a6..d0acb6d18118742daac42561313c96992e706651 100644
--- a/build.sbt
+++ b/build.sbt
@@ -16,10 +16,10 @@ ThisBuild / semanticdbEnabled := true
ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
val scala2 = "2.13.8"
-val scala3 = "3.4.2"
-
+val scala3 = "3.5.1"
val commonSettings = Seq(
- crossScalaVersions := Seq(scala3, scala2),
+ crossScalaVersions := Seq(scala3),
+
run / fork := true
)
@@ -30,7 +30,10 @@ val commonSettings2 = commonSettings ++ Seq(
val commonSettings3 = commonSettings ++ Seq(
scalaVersion := scala3,
scalacOptions ++= Seq(
- "-language:implicitConversions"
+ "-language:implicitConversions",
+ //"-rewrite", "-source", "3.4-migration",
+ "-Wconf:msg=.*will never be selected.*:silent"
+
),
javaOptions += "-Xmx10G",
libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test",
@@ -49,6 +52,8 @@ lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8
lazy val customTstpParser = githubProject("https://github.com/SimonGuilloud/scala-tptp-parser.git", "eae9c1b7a9546f74779d77ff50fa6e8a1654cfa0")
scallion/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
+scallion/scalacOptions += "-Wconf:any:silent"
+
silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
lazy val root = Project(
diff --git a/lisa-examples/src/main/scala/Lattices.scala b/lisa-examples/src/main/scala/Lattices.scala
index be45953c81ab0854ccd1d19324b68657663230bb..cbc4c28ed0d0a89c21ad4bda6590b08d255ea069 100644
--- a/lisa-examples/src/main/scala/Lattices.scala
+++ b/lisa-examples/src/main/scala/Lattices.scala
@@ -21,8 +21,8 @@ object Lattices extends lisa.Main {
// Enables infix notation
extension (left: Term) {
def <=(right: Term): Formula = Lattices.<=.applyUnsafe(Seq(left, right))
- def u(right: Term): Term = Lattices.u.applyUnsafe(Seq(left, right))
- def n(right: Term): Term = Lattices.n.applyUnsafe(Seq(left, right))
+ infix def u(right: Term): Term = Lattices.u.applyUnsafe(Seq(left, right))
+ infix def n(right: Term): Term = Lattices.n.applyUnsafe(Seq(left, right))
}
// We now states the axioms of lattices
diff --git a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
index 79795e57d8c7cca0827fa68c43420ad17caab6b5..87eab43cd9794766c362b8abca21bff31a3f72ed 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
@@ -42,7 +42,7 @@ object Substitution {
// make sure substitutions are all valid
val violatingSubstitutions = substitutions.collect {
- case f: proof.Fact if !validRule(f) => proof.sequentOfFact(f)
+ case f : proof.Fact @unchecked if !validRule(f) => proof.sequentOfFact(f)
case j: lib.JUSTIFICATION if !validRule(j) => j.statement
}
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
index ff939e4dcc5d458d3e59f5817b00f92d5be389a7..e85f6e233a36930931245b52866978c3c92845eb 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
@@ -13,6 +13,8 @@ import lisa.maths.settheory.SetTheory.functional
import lisa.prooflib.OutputManager
import lisa.maths.settheory.SetTheory.{singleton, app}
+import annotation.nowarn
+
object TypeLib extends lisa.Main {
import TypeSystem.*
@@ -220,7 +222,7 @@ object TypeSystem {
def unapply[N <: Arity](f: Formula): Option[((Term ** N) |-> Term, FunctionalClass)] =
f match
- case ta: FunctionalTypeAssignment[N] => Some((ta.functional, ta.typ))
+ case ta: FunctionalTypeAssignment[N] @unchecked => Some((ta.functional, ta.typ))
case _ => None
}
private class FunctionalTypeAssignmentConstant[N <: Arity](val functional: Term**N |-> Term, val typ: FunctionalClass, formula: ConstantFormula) extends ConstantFormula(formula.id) with FunctionalTypeAssignment[N]
@@ -310,12 +312,16 @@ object TypeSystem {
new TypedSimpleConstantDefinition(fullName, line, file)(expression, out, defThm, typ)
}
}
+
+
extension (d: definitionWithVars[0]) {
+ @nowarn
inline infix def -->[A<:Class](
using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(term:Term, typ: A): TypedConstant[A] =
TypedSimpleConstantDefinition[A](name.value, line.value, file.value)(term, typ).typedLabel
}
+
extension (c: Constant) {
def typedWith[A <: Class](typ:A)(justif: JUSTIFICATION) : TypedConstant[A] =
if justif.statement.right.size != 1 || justif.statement.left.size != 0 || !K.isSame((c `is` typ).asFormula.underlying, justif.statement.right.head.underlying) then
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index 3bb97657726158427a1c37aae79e395f86e5f7d8..ab09773d5caf9a2d49215a97452fe72d074fde88 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -408,10 +408,9 @@ trait Common {
def canEqual(that: Any): Boolean =
that.isInstanceOf[SchematicFunctionLabel[?]]
- // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
override def equals(that: Any): Boolean =
that match {
- case other: SchematicFunctionLabel[N] =>
+ case other: SchematicFunctionLabel[_] =>
((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
|| (other.canEqual(this) // optional only if this class is marked final
&& (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
@@ -457,7 +456,7 @@ trait Common {
// Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
override def equals(that: Any): Boolean =
that match {
- case other: ConstantFunctionLabel[N] =>
+ case other: ConstantFunctionLabel[_] =>
((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
|| (other.canEqual(this) // optional only if this class is marked final
&& (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
diff --git a/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
index 73e7af4a1bd06e15a029637be725943085430c02..806caf3dadd968afa5e08edf13835396dce8d4d0 100644
--- a/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala
@@ -640,6 +640,7 @@ class Parser(
val (id, r) = t match {
case ConstantToken(id, r) => (id, r)
case SchematicToken(id, r) => (id, r)
+ case _ => throw UnreachableException
}
RangedLabel(VariableFormulaLabel(id), r)
},
diff --git a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
index e1ee7a350a13e1acf264bee1c6fdcdb85c561c59..b5e59ffc71bf14891d8339cff8d5b567ace66d70 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/SubstitutionTest.scala
@@ -144,18 +144,21 @@ class SubstitutionTest extends AnyFunSuite {
case class $(f: Formula, m: ((SchematicConnectorLabel, LambdaFormulaFormula) | (SchematicAtomicLabel, LambdaTermFormula) | (SchematicTermLabel, LambdaTermTerm))*)
extension (c: $) {
inline infix def _VS_(t2: Formula): Assertion = {
+ @annotation.nowarn
val mCon: Map[SchematicConnectorLabel, LambdaFormulaFormula] = c.m
.collect({
case e if e._1.isInstanceOf[SchematicConnectorLabel] => e
})
.toMap
.asInstanceOf
+ @annotation.nowarn
val mPred: Map[SchematicAtomicLabel, LambdaTermFormula] = c.m
.collect({
case e if e._1.isInstanceOf[SchematicAtomicLabel] => e
})
.toMap
.asInstanceOf
+ @annotation.nowarn
val mTerm: Map[SchematicTermLabel, LambdaTermTerm] = c.m
.collect({
case e if e._1.isInstanceOf[SchematicTermLabel] => e