Ignore tests that fail because of missing MATLAB/MATLink

LS-Lab · Aug 12, 2024 · fe0c116 · fe0c116
1 parent de10211
commit fe0c116
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 22 deletions.
diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/btactics/ContinuousInvariantTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/btactics/ContinuousInvariantTests.scala
@@ -11,7 +11,7 @@ import org.keymaerax.btactics.TactixLibrary._
 import org.keymaerax.core._
 import org.keymaerax.parser.StringConverter._
 import org.keymaerax.parser.{ArchiveParser, Declaration}
-import org.keymaerax.tagobjects.{ExtremeTest, SlowTest}
+import org.keymaerax.tagobjects.{ExtremeTest, IgnoreInBuildTest, SlowTest}
 import org.keymaerax.tools.MathematicaComputationTimedOutException
 import org.scalatest.LoneElement._
 import org.scalatest.prop.TableDrivenPropertyChecks.{forEvery, whenever}
@@ -39,22 +39,25 @@ class ContinuousInvariantTests extends TacticTestBase {
         ("x>2".asFormula, Some(AnnotationProofHint(tryHard = true))) :: Nil)
   }
 
-  "Continuous invariant generation" should "generate a simple invariant" in withMathematicaMatlab { _ =>
-    val problem = "x>-1 & -2*x > 1 & -2*y > 1 & y>=-1 ==> [{x'=y,y'=x^5 - x*y}] x+y<=1".asSequent
-    proveBy(problem, ODE(1)) shouldBe Symbol("proved")
-
-    val (simpleInvariants, pegasusInvariants) =
-      TactixLibrary.differentialInvGenerator.generate(problem, SuccPos(0), Declaration(Map.empty)).splitAt(4)
-    simpleInvariants should contain theSameElementsAs
-      (("x>-1".asFormula, None) :: ("-2*x>1".asFormula, None) :: ("-2*y>1".asFormula, None) ::
-        ("y>=-1".asFormula, None) :: Nil)
-    // pegasus result may vary depending on its internal configuration - check only basic properties
-    // (last element is a candidate composed of all other candidates)
-    pegasusInvariants should have size 3
-    val invariants = pegasusInvariants.take(pegasusInvariants.size - 1)
-    val candidate = pegasusInvariants.last
-    candidate shouldBe invariants.map(_._1).reduce(And) -> Some(PegasusProofHint(isInvariant = true, None))
-  }
+  "Continuous invariant generation" should "generate a simple invariant" taggedAs IgnoreInBuildTest in
+    withMathematicaMatlab { _ =>
+      val problem = "x>-1 & -2*x > 1 & -2*y > 1 & y>=-1 ==> [{x'=y,y'=x^5 - x*y}] x+y<=1".asSequent
+      proveBy(problem, ODE(1)) shouldBe Symbol("proved")
+
+      val (simpleInvariants, pegasusInvariants) = TactixLibrary
+        .differentialInvGenerator
+        .generate(problem, SuccPos(0), Declaration(Map.empty))
+        .splitAt(4)
+      simpleInvariants should contain theSameElementsAs
+        (("x>-1".asFormula, None) :: ("-2*x>1".asFormula, None) :: ("-2*y>1".asFormula, None) ::
+          ("y>=-1".asFormula, None) :: Nil)
+      // pegasus result may vary depending on its internal configuration - check only basic properties
+      // (last element is a candidate composed of all other candidates)
+      pegasusInvariants should have size 3
+      val invariants = pegasusInvariants.take(pegasusInvariants.size - 1)
+      val candidate = pegasusInvariants.last
+      candidate shouldBe invariants.map(_._1).reduce(And) -> Some(PegasusProofHint(isInvariant = true, None))
+    }
 
   it should "generate invariants for nonlinear benchmarks with Pegasus" taggedAs ExtremeTest in withMathematica {
     tool =>

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/btactics/InvariantGeneratorTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/btactics/InvariantGeneratorTests.scala
@@ -15,7 +15,7 @@ import org.keymaerax.hydra.DatabasePopulator
 import org.keymaerax.infrastruct.{FormulaTools, SuccPosition}
 import org.keymaerax.parser.StringConverter._
 import org.keymaerax.parser.{ArchiveParser, Declaration, Parser}
-import org.keymaerax.tagobjects.TodoTest
+import org.keymaerax.tagobjects.{IgnoreInBuildTest, TodoTest}
 import org.keymaerax.tags.{ExtremeTest, UsualTest}
 import org.keymaerax.tools.ext.{MathematicaInvGenTool, PlotConverter}
 import org.keymaerax.tools.install.ToolConfiguration
@@ -211,7 +211,7 @@ class InvariantGeneratorTests extends TacticTestBase with PrivateMethodTester {
       )
   }
 
-  it should "generate Darboux polynomials" in withMathematicaMatlab { _ =>
+  it should "generate Darboux polynomials" taggedAs IgnoreInBuildTest in withMathematicaMatlab { _ =>
     val s = """x > -1, x < -3/4, y <= 3/2 & y >= 1
               |==>
               |[

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/btactics/SwitchedSystemsTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/btactics/SwitchedSystemsTests.scala
@@ -9,7 +9,7 @@ import org.keymaerax.btactics.SwitchedSystems._
 import org.keymaerax.btactics.TactixLibrary._
 import org.keymaerax.core._
 import org.keymaerax.parser.StringConverter._
-import org.keymaerax.tagobjects.TodoTest
+import org.keymaerax.tagobjects.{IgnoreInBuildTest, TodoTest}
 
 class SwitchedSystemsTests extends TacticTestBase {
 
@@ -224,7 +224,7 @@ class SwitchedSystemsTests extends TacticTestBase {
     pr2 shouldBe Symbol("proved")
   }
 
-  it should "prove system stable automatically" in withMathematicaMatlab { _ =>
+  it should "prove system stable automatically" taggedAs IgnoreInBuildTest in withMathematicaMatlab { _ =>
     val ode1 = ODESystem("x1'=-2*x1-x2-x3, x2'=-x2, x3'=-x1-x2-2*x3".asDifferentialProgram, True)
     val ode2 = ODESystem("x1'=2*x2, x2'=-2*x1-x2, x3'=x1-2*x2-x3".asDifferentialProgram, True)
 
@@ -497,7 +497,7 @@ class SwitchedSystemsTests extends TacticTestBase {
     pr2 shouldBe Symbol("proved")
   }
 
-  it should "prove guarded system stable automatically" in withMathematica { _ =>
+  it should "prove guarded system stable automatically" taggedAs IgnoreInBuildTest in withMathematica { _ =>
     // Johansson and Rantzer motivating example
     val ode1 = ODESystem("x1' = -5*x1-4*x2, x2' =   -x1-2*x2".asDifferentialProgram, "x1<=0".asFormula)
     val ode2 = ODESystem("x1' = -2*x1-4*x2, x2' = 20*x1-2*x2".asDifferentialProgram, "x1>=0".asFormula)