diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 1b632e5531c..3daf0e7f065 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -107,6 +107,7 @@ jobs: with: name: test-results-${{ matrix.test }} path: | + key.core/proofs/** **/build/test-results/*/*.xml key.core/build/reports/runallproofs/* **/build/reports/ diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java index 7ccecc800fb..8c9c8ed5ee6 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java @@ -5,14 +5,18 @@ import java.io.File; import java.io.IOException; +import java.io.PrintWriter; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; import java.util.List; +import java.util.zip.GZIPOutputStream; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.nparser.KeyAst; +import de.uka.ilkd.key.pp.LogicPrinter; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.AbstractProblemLoader; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -138,6 +142,11 @@ private void runKey(String file, TestProperty testProperty) throws Exception { LOGGER.info("({}) Finished proof: {}", caseId, (closed ? "closed." : "open goal(s)")); appendStatistics(loadedProof, keyFile.toFile()); + + var path = Paths.get("proofs", + loadedProof.getProofFile().getFileName() + ".proof.xml"); + saveProofXml(loadedProof, path); + if (success) { reload(proofFile, loadedProof); } @@ -162,6 +171,27 @@ private void runKey(String file, TestProperty testProperty) throws Exception { } } + public static void saveProofXml(Proof loadedProof, Path path) throws IOException { + Files.createDirectories(path.getParent()); + try (var out = new PrintWriter(new GZIPOutputStream(Files.newOutputStream(path)))) { + toXml(out, loadedProof.root()); + } + } + + private static void toXml(PrintWriter out, Node node) { + out.format("\n", node.getNodeInfo().getBranchLabel(), + node.getAppliedRuleApp().rule().name()); + out.format("\n\n", node.sequent()); + out.format("\n\n", + LogicPrinter.quickPrintSequent(node.sequent(), node.proof().getServices())); + out.format("\n\n"); + for (Node child : node.children()) { + toXml(out, child); + } + out.format("\n"); + out.format("\n"); + } + /** * Override this method in order to change reload behaviour. */ diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java index 79df3f4b495..db19af07741 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.proof.io.ProofSaver; +import de.uka.ilkd.key.proof.runallproofs.ProveTest; import de.uka.ilkd.key.proof.runallproofs.RunAllProofsTest; import de.uka.ilkd.key.proof.runallproofs.TestResult; import de.uka.ilkd.key.scripts.ProofScriptEngine; @@ -166,6 +167,7 @@ public TestResult runKey() throws Exception { loadedProof = env.getLoadedProof(); ReplayResult replayResult; + if (testProperty == TestProperty.NOTLOADABLE) { try { replayResult = env.getReplayResult(); @@ -205,6 +207,11 @@ public TestResult runKey() throws Exception { || testProperty == TestProperty.NOTPROVABLE) { ProofSaver.saveToFile(new File(keyFile.toAbsolutePath() + ".save.proof"), loadedProof); + + var path = Paths.get("proofs", + loadedProof.getProofFile().getFileName() + ".proof.xml.gz"); + ProveTest.saveProofXml(loadedProof, path); + LOGGER.info("Stored {}", path); } boolean closed = loadedProof.closed(); success = (testProperty == TestProperty.PROVABLE) == closed;