From 8af257a9a60a5f14d50e65ad33a47a74942960e4 Mon Sep 17 00:00:00 2001 From: SimonGuilloud Date: Fri, 4 Oct 2024 12:27:05 +0200 Subject: [PATCH] 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 | 3 +++ build.sbt | 13 +++++++++---- lisa-examples/src/main/scala/Lattices.scala | 4 ++-- .../main/scala/lisa/automation/Substitution.scala | 2 +- .../lisa/maths/settheory/types/TypeSystem.scala | 8 +++++++- lisa-utils/src/main/scala/lisa/fol/Common.scala | 5 ++--- .../src/main/scala/lisa/utils/parsing/Parser.scala | 1 + .../test/scala/lisa/kernel/SubstitutionTest.scala | 3 +++ 8 files changed, 28 insertions(+), 11 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 3c8fec63a..fdcd76e10 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 faa922e1e..d0acb6d18 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 be45953c8..cbc4c28ed 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 79795e57d..87eab43cd 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 ff939e4dc..e85f6e233 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 3bb976577..ab09773d5 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 73e7af4a1..806caf3da 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 e1ee7a350..b5e59ffc7 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