Dependency and Scala Upgrades (#221)

* More sensible multi line strings, up scalafmt version * Upgrade sbt version * Upgrade sbt plugins * Upgrade Scala version to 3.3.3 * Update library dependencies * Expose library main classes * Remove infinite loop (?) * Uncomment examples, move Goeland examples to separate object * Scala fmt * Comment SimpleTautology
epfl-lara · Jun 18, 2024 · 712da94 · 712da94
1 parent cbec155
commit 712da94
Show file tree

Hide file tree

Showing 7 changed files with 104 additions and 119 deletions.
diff --git a/.scalafmt.conf b/.scalafmt.conf
@@ -1,4 +1,4 @@
-version = 3.4.2
+version = 3.7.13
 
 runner.dialect = scala3
 
@@ -8,4 +8,7 @@ docstrings.style = Asterisk
 docstrings.oneline = unfold
 docstrings.wrap = no
 
-align.preset = none
+# align and indentation settings
+align.preset = none
+assumeStandardLibraryStripMargin = true
+align.stripMargin = true
diff --git a/build.sbt b/build.sbt
@@ -14,19 +14,14 @@ ThisBuild / scalacOptions ++= Seq(
 ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
 ThisBuild / semanticdbEnabled := true
 ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
-ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
-
-
-
 
 val commonSettings = Seq(
-  crossScalaVersions := Seq("3.3.1"),
+  crossScalaVersions := Seq("3.3.3"),
   run / fork := true
 )
 
-
 val scala2 = "2.13.8"
-val scala3 = "3.3.1"
+val scala3 = "3.3.3"
 
 val commonSettings2 = commonSettings ++ Seq(
   scalaVersion := scala2,
@@ -36,15 +31,10 @@ val commonSettings3 = commonSettings ++ Seq(
   scalaVersion := scala3,
   scalacOptions ++= Seq(
     "-language:implicitConversions",
-
-    // "-source:future", re-enable when liancheng/scalafix-organize-imports#221 is fixed
-
   ),
   javaOptions += "-Xmx10G",
-  libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
-  libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.3.0",
-  //libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
-  // libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
+  libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.18" % "test",
+  libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.4.1",
   Test / parallelExecution := false
 )
 
@@ -63,12 +53,14 @@ silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
 
 lazy val root = Project(
     id = "lisa",
-    base = file(".")
+    base = file("."),
   )
   .settings(commonSettings3)
   .dependsOn(kernel, withTests(utils), withTests(sets)) // Everything but `examples`
   .aggregate(utils) // To run tests on all modules
 
+Compile / run := (sets / Compile / run).evaluated
+
 lazy val kernel = Project(
   id = "lisa-kernel",
   base = file("lisa-kernel")

diff --git a/lisa-examples/src/main/scala/ADTExample.scala b/lisa-examples/src/main/scala/ADTExample.scala
@@ -46,12 +46,12 @@ object ADTExample extends lisa.Main {
   show(nil.intro)
   show(cons.intro)
 
-  Lemma(nil(A) :: list(A)){
+  Lemma(nil(A) :: list(A)) {
     have(thesis) by TypeChecker.prove
-  } 
-  Lemma((x :: A, l :: list(A)) |- cons(A) * x * l :: list(A)){
+  }
+  Lemma((x :: A, l :: list(A)) |- cons(A) * x * l :: list(A)) {
     have(thesis) by TypeChecker.prove
-  } 
+  }
 
   // Induction
   show(list.induction)
@@ -69,12 +69,11 @@ object ADTExample extends lisa.Main {
   }
 
   val pred = fun(nat, nat):
-    Case(zero): 
-      zero 
-    Case(succ, n): 
+    Case(zero):
+      zero
+    Case(succ, n):
       n
 
-
   // ************************
   // * 4 : Induction Tactic *
   // ************************
@@ -103,16 +102,16 @@ object ADTExample extends lisa.Main {
     val typeNil = have(nil(A) :: list(A)) by TypeChecker.prove
     val typeCons = have((y :: A, l :: list(A)) |- cons(A) * y * l :: list(A)) by TypeChecker.prove
 
-    have(l :: list(A) |- forall(x, x :: A ==> !(l === cons(A) * x * l))) by Induction(){
+    have(l :: list(A) |- forall(x, x :: A ==> !(l === cons(A) * x * l))) by Induction() {
       Case(nil) subproof {
         have(x :: A ==> !(nil(A) === cons(A) * x * nil(A))) by Tautology.from(list.injectivity(nil, cons) of (y0 := x, y1 := nil(A)), typeNil)
         thenHave(forall(x, x :: A ==> !(nil(A) === cons(A) * x * nil(A)))) by RightForall
       }
       Case(cons, y, l) subproof {
         have((y :: A ==> !(l === cons(A) * y * l), y :: A, l :: list(A)) |- x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l))) by Tautology.from(
-             cons.injectivity of (x0 := y, x1 := l, y0 := x, y1 := cons(A) * y * l),
-             typeCons
-           )
+          cons.injectivity of (x0 := y, x1 := l, y0 := x, y1 := cons(A) * y * l),
+          typeCons
+        )
         thenHave((y :: A ==> !(l === cons(A) * y * l), y :: A, l :: list(A)) |- forall(x, x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l)))) by RightForall
         thenHave((forall(x, x :: A ==> !(l === cons(A) * x * l)), y :: A, l :: list(A)) |- forall(x, x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l)))) by LeftForall
       }
@@ -122,4 +121,4 @@ object ADTExample extends lisa.Main {
     thenHave(thesis) by Tautology
   }
 
-}
+}
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
@@ -1,9 +1,9 @@
+import lisa.automation.Congruence
 import lisa.automation.Substitution.{ApplyRules as Substitute}
 import lisa.automation.Tableau
 import lisa.automation.atp.Goeland
-import lisa.automation.Congruence
 
-object Example extends lisa.Main {
+object Example extends lisa.Main:
   draft()
 
   val x = variable
@@ -62,91 +62,82 @@ object Example extends lisa.Main {
     have(thesis) by Tableau
   }
 
-  val buveurs2 = Theorem(exists(x, P(x) ==> forall(y, P(y)))) {
-    have(thesis) by Goeland//("goeland/Example.buveurs2_sol")
-  }
-
-
-  val a = variable
-  val one = variable
-  val two = variable
-  val * = SchematicFunctionLabel("*", 2)
-  val << = SchematicFunctionLabel("<<", 2)
-  val / = SchematicFunctionLabel("/", 2)
-  private val star: SchematicFunctionLabel[2] = *
-  private val shift: SchematicFunctionLabel[2] = <<
-  private val divide: SchematicFunctionLabel[2] = /
-
-  while (true) {
-    ()
-  }
-
-  extension (t:Term) {
-    def *(u:Term) = star(t, u)
-    def <<(u:Term) = shift(t, u)
-    def /(u:Term) = divide(t, u)
-  }
-  val congruence = Theorem(((a*two) === (a<<one), a*(two/two) === (a*two)/two, (two/two) === one, (a*one) === a) |- ((a<<one)/two) === a) {
-    have(thesis) by Congruence
-  }
-
-  /*
-
-  import lisa.mathematics.settheory.SetTheory.*
+  // val a = variable
+  // val one = variable
+  // val two = variable
+  // val * = SchematicFunctionLabel("*", 2)
+  // val << = SchematicFunctionLabel("<<", 2)
+  // val / = SchematicFunctionLabel("/", 2)
+  // private val star: SchematicFunctionLabel[2] = *
+  // private val shift: SchematicFunctionLabel[2] = <<
+  // private val divide: SchematicFunctionLabel[2] = /
+
+  // extension (t:Term) {
+  //   def *(u:Term) = star(t, u)
+  //   def <<(u:Term) = shift(t, u)
+  //   def /(u:Term) = divide(t, u)
+  // }
+  // val congruence = Theorem(((a*two) === (a<<one), a*(two/two) === (a*two)/two, (two/two) === one, (a*one) === a) |- ((a<<one)/two) === a) {
+  //   have(thesis) by Congruence
+  // }
 
+  // import lisa.mathematics.settheory.SetTheory.*
 
   // Examples of definitions
-  val succ = DEF(x) --> union(unorderedPair(x, singleton(x)))
-  show
-
-  val inductiveSet = DEF(x) --> in(∅, x) /\ forall(y, in(y, x) ==> in(succ(y), x))
-  show
+  // val succ = DEF(x) --> union(unorderedPair(x, singleton(x)))
+  // show
 
-   */
+  // val inductiveSet = DEF(x) --> in(∅, x) /\ forall(y, in(y, x) ==> in(succ(y), x))
+  // show
 
-
-
-
-
-// Simple tactic definition for LISA DSL
-/*
-import lisa.automation.kernel.OLPropositionalSolver.*
-
-object SimpleTautology extends ProofTactic {
-  def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = {
-    val redF = reducedForm(f)
-    if (redF == ⊤) {
-      Restate(decisionsPos |- f :: decisionsNeg)
-    } else if (redF == ⊥) {
-      proof.InvalidProofTactic("Sequent is not a propositional tautology")
-    } else {
-      val atom = findBestAtom(redF).get
-      def substInRedF(f: Formula) = redF.substituted(atom -> f)
-      TacticSubproof {
-        have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg))
-        val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom)
-        have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg))
-        val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom)
-        have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2)
-        thenHave(decisionsPos |- f :: decisionsNeg) by Restate
-      }
-    }
-  }
+  // Simple tactic definition for LISA DSL
+
+  // object SimpleTautology extends ProofTactic {
+  //   def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = {
+  //     val redF = reducedForm(f)
+  //     if (redF == ⊤) {
+  //       Restate(decisionsPos |- f :: decisionsNeg)
+  //     } else if (redF == ⊥) {
+  //       proof.InvalidProofTactic("Sequent is not a propositional tautology")
+  //     } else {
+  //       val atom = findBestAtom(redF).get
+  //       def substInRedF(f: Formula) = redF.substituted(atom -> f)
+  //       TacticSubproof {
+  //         have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg))
+  //         val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom)
+  //         have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg))
+  //         val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom)
+  //         have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2)
+  //         thenHave(decisionsPos |- f :: decisionsNeg) by Restate
+  //       }
+  //     }
+  //   }
+
+  //   def solveSequent(using proof: library.Proof)(bot: Sequent) =
+  //     TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula
+  //       have(solveFormula(sequentToFormula(bot), Nil, Nil))
+  //       thenHave(bot) by Restate.from
+  //     }
+  // }
 
-  def solveSequent(using proof: library.Proof)(bot: Sequent) =
-    TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula
-      have(solveFormula(sequentToFormula(bot), Nil, Nil))
-      thenHave(bot) by Restate.from
-    }
-}
-*/
-
-  // val a = formulaVariable()
-  // val b = formulaVariable()
-  // val c = formulaVariable()
+  // val a = formulaVariable
+  // val b = formulaVariable
+  // val c = formulaVariable
   // val testTheorem = Lemma((a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))) {
   //   have(thesis) by SimpleTautology.solveSequent
   // }
   // show
 
-}
+/**
+ * Example showing discharge of proofs using the Goeland theorem prover. Will
+ * fail if Goeland is not available on PATH.
+ */
+object GoelandExample extends lisa.Main:
+  val x = variable
+  val y = variable
+  val P = predicate[1]
+  val f = function[1]
+
+  val buveurs2 = Theorem(exists(x, P(x) ==> forall(y, P(y)))) {
+    have(thesis) by Goeland // ("goeland/Example.buveurs2_sol")
+  }
diff --git a/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala b/lisa-utils/src/test/scala/lisa/utils/ParserTest.scala
@@ -268,9 +268,9 @@ class ParserTest extends AnyFunSuite with TestUtils {
       FOLParser.parseFormula("f(x y)")
     } catch {
       case e: UnexpectedInputException => assert(e.getMessage.startsWith("""
-          |f(x y)
-          |    ^
-          |Unexpected input""".stripMargin))
+                                                                           |f(x y)
+                                                                           |    ^
+                                                                           |Unexpected input""".stripMargin))
     }
   }
 
@@ -280,9 +280,9 @@ class ParserTest extends AnyFunSuite with TestUtils {
     } catch {
       case e: UnexpectedInputException =>
         assert(e.getMessage.startsWith("""
-            |x = (a /\ b)
-            |     ^^^^^^
-            |Unexpected input: expected term""".stripMargin))
+                                         |x = (a /\ b)
+                                         |     ^^^^^^
+                                         |Unexpected input: expected term""".stripMargin))
     }
   }
 }
diff --git a/project/build.properties b/project/build.properties
@@ -1,2 +1,2 @@
 
-sbt.version = 1.9.3
+sbt.version = 1.9.9
diff --git a/project/plugins.sbt b/project/plugins.sbt
@@ -1,3 +1,3 @@
-addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.1.0")
-addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.9.34")
-addSbtPlugin("org.scalameta" % "sbt-scalafmt" % "2.4.6")
+addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "2.2.0")
+addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.11.1")
+addSbtPlugin("org.scalameta" % "sbt-scalafmt" % "2.5.2")