diff --git a/CHANGES.md b/CHANGES.md
index 64137c56d95804aff50a82477c1c5b99b2e78a43..b054dda822a4658eef9e4db182518cff57837104 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 2363514675c88cbb9850b3f17f952f1e1f47be0b..8178b55994a3812d5655501a33bf6e6d8884a385 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 6de053d76693ba36dbbe031267d3faf66214aab4..3ecd56b43bcc91e6770259727b0374c401212356 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 e57c06834cc5d2d7aab8467e51ff8f13e4f57a87..b43484c7969cfe21c519a45c47b45a5f1cdd82d4 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 6182209bd8378c5dddb3f79c72b4b7d856b96553..60af52ffe3783d2117b63b7fd952a9532695dd35 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 0ecd5aae7f41f37d936900c0e1019ad25991dc71..877ad4593786f811633025be56617b9de299d3bc 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 24614ca346eaae469dfffeba1a11fb1a57d67c31..46a510d48d084fda7d4fd8e4c05823cc90885bbd 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.