From 32d5be76baaddb6047e64b8bb98a41ca61489ca1 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Wed, 6 Dec 2023 16:36:27 +0100
Subject: [PATCH] Upgrade to Scala 3.3.1 (#197)
* Upgrade to 3.3.1 disabling pattern matching checks
* Fixes for build
* scalafix
* Fix reference to kernel formula
* File changes
---
CHANGES.md | 6 +++++
build.sbt | 12 +++++++--
.../scala/lisa/automation/CommonTactics.scala | 25 ++++++++++---------
.../maths/settheory/orderings/Induction.scala | 2 +-
.../maths/settheory/orderings/Recursion.scala | 2 +-
.../maths/settheory/orderings/Segments.scala | 2 +-
.../scala/lisa/prooflib/WithTheorems.scala | 15 ++++++-----
7 files changed, 41 insertions(+), 23 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index 64137c56..b054dda8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,11 @@
# Change List
+## 2023-12-06
+Upgrade to Scala 3.3.1
+
+- the `Proof` class has been temporarily unsealed, till [lampepfl/dotty#19031](https://github.com/lampepfl/dotty/issues/19031) / [epfl-lara/lisa#190](https://github.com/epfl-lara/lisa/issues/190) is fixed
+- minor fixes to address compilation errors, mostly involving explicitly specifying types or implicits in some places.
+
## 2023-12-02
Creation of the present Change Liste, going back to October 2023
diff --git a/build.sbt b/build.sbt
index 23635146..8178b559 100644
--- a/build.sbt
+++ b/build.sbt
@@ -26,7 +26,7 @@ val commonSettings = Seq(
val scala2 = "2.13.8"
-val scala3 = "3.2.2"
+val scala3 = "3.3.1"
val commonSettings2 = commonSettings ++ Seq(
scalaVersion := scala2,
@@ -94,7 +94,15 @@ lazy val utils = Project(
.dependsOn(scallion % "compile->compile")
.settings(libraryDependencies += "io.github.leoprover" % "scala-tptp-parser_2.13" % "1.4")
-
+ThisBuild / assemblyMergeStrategy := {
+ case PathList("module-info.class") => MergeStrategy.discard
+ case x if x.endsWith("/module-info.class") => MergeStrategy.discard
+ case x if x.endsWith(".class") => MergeStrategy.first
+ case x if x.endsWith(".tasty") => MergeStrategy.first
+ case x =>
+ val oldStrategy = (ThisBuild / assemblyMergeStrategy).value
+ oldStrategy(x)
+}
lazy val examples = Project(
diff --git a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
index 6de053d7..3ecd56b4 100644
--- a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
@@ -143,18 +143,19 @@ object CommonTactics {
case Some(value: lib.FunctionDefinition[?]) => value
case _ => return proof.InvalidProofTactic("Could not get definition of function.")
}
- val method = expr.f.substituteUnsafe(expr.vars.zip(xs).toMap) match {
- case F.AppliedConnector(
- F.And,
- Seq(
- F.AppliedConnector(F.Implies, Seq(a, _)),
- F.AppliedConnector(F.Implies, Seq(b, _))
- )
- ) if F.isSame(F.Neg(a), b) =>
- conditional
-
- case _ => unconditional
- }
+ val method: (F.ConstantFunctionLabel[?], proof.Fact) => Seq[F.Term] => F.Sequent => proof.ProofTacticJudgement =
+ expr.f.substituteUnsafe(expr.vars.zip(xs).toMap) match {
+ case F.AppliedConnector(
+ F.And,
+ Seq(
+ F.AppliedConnector(F.Implies, Seq(a, _)),
+ F.AppliedConnector(F.Implies, Seq(b, _))
+ )
+ ) if F.isSame(F.Neg(a), b) =>
+ conditional(using lib, proof)
+
+ case _ => unconditional(using lib, proof)
+ }
method(f, uniqueness)(xs)(bot)
}
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Induction.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Induction.scala
index e57c0683..b43484c7 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Induction.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Induction.scala
@@ -4,7 +4,7 @@ import lisa.automation.settheory.SetTheoryTactics.*
import lisa.maths.Quantifiers.*
import lisa.maths.settheory.SetTheory.*
import lisa.maths.settheory.orderings.InclusionOrders.*
-import lisa.maths.settheory.orderings.Ordinals.*
+import Ordinals.*
import lisa.maths.settheory.orderings.PartialOrders.*
import lisa.maths.settheory.orderings.Segments.*
import lisa.maths.settheory.orderings.WellOrders.*
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
index 6182209b..60af52ff 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
@@ -5,7 +5,7 @@ import lisa.maths.Quantifiers.*
import lisa.maths.settheory.SetTheory.*
import lisa.maths.settheory.orderings.InclusionOrders.*
import lisa.maths.settheory.orderings.Induction.*
-import lisa.maths.settheory.orderings.Ordinals.*
+import Ordinals.*
import lisa.maths.settheory.orderings.PartialOrders.*
import lisa.maths.settheory.orderings.Segments.*
import lisa.maths.settheory.orderings.WellOrders.*
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Segments.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Segments.scala
index 0ecd5aae..877ad459 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Segments.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Segments.scala
@@ -4,7 +4,7 @@ import lisa.automation.settheory.SetTheoryTactics.*
import lisa.maths.Quantifiers.*
import lisa.maths.settheory.SetTheory.*
import lisa.maths.settheory.orderings.InclusionOrders.*
-import lisa.maths.settheory.orderings.Ordinals.*
+import Ordinals.*
import lisa.maths.settheory.orderings.PartialOrders.*
import lisa.maths.settheory.orderings.WellOrders.*
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index 24614ca3..46a510d4 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -25,7 +25,10 @@ trait WithTheorems {
*
* @param assump list of starting assumptions, usually propagated from outer proofs.
*/
- sealed abstract class Proof(assump: List[F.Formula]) {
+ // TODO: reseal this class
+ // see https://github.com/lampepfl/dotty/issues/19031
+ // and https://github.com/epfl-lara/lisa/issues/190
+ abstract class Proof(assump: List[F.Formula]) {
val possibleGoal: Option[F.Sequent]
type SelfType = this.type
type OutsideFact >: JUSTIFICATION
@@ -259,11 +262,11 @@ trait WithTheorems {
*/
def asOutsideFact(j: JUSTIFICATION): OutsideFact
- @nowarn("msg=.*It would fail on pattern case: _: InnerProof.*")
- def depth: Int = this match {
- case p: Proof#InnerProof => 1 + p.parent.depth
- case _: BaseProof => 0
- }
+ def depth: Int =
+ (this: @unchecked) match {
+ case p: Proof#InnerProof => 1 + p.parent.depth
+ case _: BaseProof => 0
+ }
/**
* Create a subproof inside the current proof. The subproof will have the same assumptions as the current proof.
--
GitLab