Skip to content

Commit

Permalink
Fixing the broken automode (#3533)
Browse files Browse the repository at this point in the history
  • Loading branch information
wadoon authored Dec 16, 2024
2 parents 1b3f51f + db23498 commit c39b255
Showing 1 changed file with 35 additions and 31 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -131,52 +131,56 @@ public void taskFinished(TaskFinishedInfo info) {
super.taskFinished(info);
progressMax = 0; // reset progress bar marker
final Proof proof = info.getProof();
final Object result = info.getResult();
if (proof == null) {
final Object error = info.getResult();
LOGGER.info("Proof loading failed");
if (error instanceof Throwable) {
LOGGER.info("Proof loading failed", (Throwable) error);
if (result instanceof Throwable thrown) {
LOGGER.info("Proof loading failed", thrown);
} else {
LOGGER.info("Proof loading failed");
}
System.exit(1);
}
final int openGoals = proof.openGoals().size();
final Object result2 = info.getResult();
if (info.getSource() instanceof ProverCore || info.getSource() instanceof ProofMacro) {
if (!isAtLeastOneMacroRunning()) {
printResults(openGoals, info, result2);
printResults(openGoals, info, result);
}
} else if (info.getSource() instanceof ProblemLoader) {
LOGGER.debug("{}", result2);
System.exit(-1);
}
if (loadOnly || openGoals == 0) {
LOGGER.info("Number of open goals after loading: {}", openGoals);
System.exit(0);
}
ProblemLoader problemLoader = (ProblemLoader) info.getSource();
if (problemLoader.hasProofScript()) {
try {
ProofScriptEntry script = problemLoader.getProofScript();
if (script != null) {
ProofScriptEngine pse =
new ProofScriptEngine(script.script(), script.location());
this.taskStarted(
new DefaultTaskStartedInfo(TaskKind.Macro, "Script started", 0));
pse.execute(this, proof);
// The start and end messages are fake to persuade the system ...
// All this here should refactored anyway ...
this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof));
if (result != null) {
LOGGER.debug("{}", result);
if (result instanceof Throwable thrown) {
LOGGER.debug("Exception: ", thrown);
}
} catch (Exception e) {
LOGGER.debug("", e);
System.exit(-1);
}
} else if (macroChosen()) {
applyMacro();
} else {
finish(proof);
if (loadOnly || openGoals == 0) {
LOGGER.info("Number of open goals after loading: {}", openGoals);
System.exit(0);
}
ProblemLoader problemLoader = (ProblemLoader) info.getSource();
if (problemLoader.hasProofScript()) {
try {
ProofScriptEntry script = problemLoader.getProofScript();
if (script != null) {
ProofScriptEngine pse =
new ProofScriptEngine(script.script(), script.location());
this.taskStarted(
new DefaultTaskStartedInfo(TaskKind.Macro, "Script started", 0));
pse.execute(this, proof);
// The start and end messages are fake to persuade the system ...
// All this here should refactored anyway ...
this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof));
}
} catch (Exception e) {
LOGGER.debug("", e);
System.exit(-1);
}
} else if (macroChosen()) {
applyMacro();
} else {
finish(proof);
}
}
}

Expand Down

0 comments on commit c39b255

Please sign in to comment.