epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

`repr` fails on a `null` match on encountering a wrong theorem #157

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

With some recent changes in how theorems are displayed (#155), it seems displaying errors was broken

  val myCorrectTheorem = Theorem(P(x) |- P(y)) {
    have(thesis) by Restate
  }

Raises a null match exception:

[info] running (fork) lisa.mathematics.FirstOrderLogic 
[error] Exception in thread "main" java.lang.ExceptionInInitializerError
[error]         at lisa.mathematics.FirstOrderLogic.main(FirstOrderLogic.scala)
[error] Caused by: scala.MatchError: null
[error]         at lisa.utils.KernelHelpers$.repr(KernelHelpers.scala:446)
[error]         at lisa.prooflib.TheoriesHelpers$.repr(TheoriesHelpers.scala:22)
[error]         at lisa.prooflib.Library.repr(Library.scala:25)
[error]         at lisa.prooflib.WithTheorems$THM.repr(WithTheorems.scala:297)
[error]         at lisa.prooflib.ProofTacticLib$UnapplicableProofTactic.showError(ProofTacticLib.scala:53)
[error]         at lisa.prooflib.OutputManager.lisaThrow(OutputManager.scala:22)
[error]         at lisa.prooflib.WithTheorems$THM.show(WithTheorems.scala:306)
[error]         at lisa.prooflib.WithTheorems$THM.<init>(WithTheorems.scala:294)
[error]         at lisa.prooflib.ProofsHelpers$$anon$1.<init>(ProofsHelpers.scala:180)
[error]         at lisa.prooflib.ProofsHelpers.apply(ProofsHelpers.scala:180)
[error]         at lisa.prooflib.ProofsHelpers.apply$(ProofsHelpers.scala:17)
[error]         at lisa.prooflib.Library.apply(Library.scala:17)
[error]         at lisa.Main.apply(Main.scala:9)
[error]         at lisa.Main.apply$(Main.scala:8)
[error]         at lisa.mathematics.FirstOrderLogic$.apply(FirstOrderLogic.scala:10)
[error]         at lisa.mathematics.FirstOrderLogic$.<clinit>(FirstOrderLogic.scala:330)
[error]         ... 1 more
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1

I'm not entirely sure as to what produces this null value after a short look.