From 7335d23c178460abe2167a1780834df7c1a12b17 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Fri, 1 Jul 2022 14:00:42 +0200
Subject: [PATCH] In ProofCheckerSuite#checkProof, fail if the proof is not
valid
---
lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
index 6c3d6c4f..4a989fa2 100644
--- a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
+++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
@@ -2,6 +2,8 @@ package lisa.test
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker.*
+import lisa.kernel.proof.SCProofCheckerJudgement
+import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof
import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.proof.SequentCalculus.isSameSequent
import lisa.utils.Helpers.{_, given}
@@ -40,8 +42,7 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
def checkProof(proof: SCProof): Unit = {
val judgement = checkSCProof(proof)
- println(Printer.prettySCProof(judgement))
- println(s"\n(${proof.totalLength} proof steps in total)")
+ assert(judgement.isValid, Printer.prettySCProof(judgement, true))
}
def checkProof(proof: SCProof, expected: Sequent): Unit = {
--
GitLab