Skip to content

Commit

Permalink
Revert "Unset interpreter in TempDBTools as well"
Browse files Browse the repository at this point in the history
This reverts commit 8b5446f.

Some ToolTacticsTests stopped working due to the original commit, as
discovered by Enguerrand. From what I can tell, the reason is the
following:

When the BelleInterpreter is unset (and thereby killed) after
interpreting is over, the registered TraceRecordingListener edits the
database at TraceRecordingListener.scala line 171.

This then results in the db.extractTactic call to fail to reconstruct
the tactic, and thus the test fails, e.g. at ToolTacticsTests.scala line
272.

I have no idea why db.extractTactic returns "Mathematica <function1>"
and similar instead of failing in a more obvious way.
  • Loading branch information
Joscha Mennicken authored and EnguerrandPrebet committed May 24, 2024
1 parent c22b837 commit de83286
Showing 1 changed file with 5 additions and 13 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -129,19 +129,11 @@ class TempDBTools(additionalListeners: Seq[IOListener]) {
constructGlobalProvable = false,
)
val listeners = listener :: Nil ++ additionalListeners

val result =
try {
BelleInterpreter.setInterpreter(interpreter(listeners))
BelleInterpreter(t, BelleProvable.plain(ProvableSig.startProof(entry.model.asInstanceOf[Formula], entry.defs)))
} finally {
// The TraceRecordingListener has a reference to the db. When the interpreter is killed (e.g. by another call to
// BelleInterpreter.setInterpreter later), this can cause errors if the db has been closed in the meantime.
// Because of this, we unset (and thereby kill) the interpreter here while the db is still valid.
BelleInterpreter.unsetInterpreter()
}

result match {
BelleInterpreter.setInterpreter(interpreter(listeners))
BelleInterpreter(
t,
BelleProvable.plain(ProvableSig.startProof(entry.model.asInstanceOf[Formula], entry.defs)),
) match {
case BelleProvable(provable, _) =>
assert(
entry.defs.exhaustiveSubst(provable.conclusion) == expectedSubstConclusion,
Expand Down

0 comments on commit de83286

Please sign in to comment.