Artiweb > Pull Request #3030

Removal of the Proof Collection Parser #3030

Github

Description

The Proof Collection Parser is an antlr3 parser, which reads text files -- the proof collections -- and translates them into a data structure used for executing run all proofs tests. In order of switching from antlr3 to antlr4, it seems that rewriting of this parser is not beneficial, as its grammar can easily mapped to a Java-DSL without loss of readability and gaining all nice IDE features (syntax highlighting, code assist etc) for writing these files.

:exclamation: So this PR removes the collection and also all dependencies of ANTLR2 and ANTLR3 in the source code of KeY.

Sides effects are that unused exception classes are removed.

This PR also repairs wrong paths of Information flow statistics and adds the run-all-proofs to the uploaded build artifacts.

The impact is limited to run all proofs. This MR also changes the path, where the statistics are written to---in particular the folder key.core.test does not exists anymore; leading to changes in the Jenkins config.

Artifacts