Update project to scala version 3.5.1. Rewrite depreciated syntax. (#227

)

* Update project to scala version 3.5.1. Rewrite depreciated syntax.
Hide scallion warning report.

* update changelist

* minonr fix, mark n and u infix in Lattices.scala.

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). 
 

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(

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

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
       }
 

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

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

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)
       },

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