Interactive prover that stops when oracle returns nothing

[felixlinker]

I implemented a proof-method for the interactive prover that autoproves unless the oracle returns no ranking. I often had to deal with complicated theories that don't terminate in one case. Finding this case was a pain. This method should help in these cases.

I also think that the new Ranking type can be extended with more interesting "instructions" as I call them alter as well, i.e., this typing framework is desirable in its own right. For example, backtracking could be implemented using this framework.

[cascremers]

Does it makes sense to display and provide this option if there is no oracle file? Should we maybe check if the oracle file exists beforehand?

[felixlinker]

We could. If there's no oracle, it just behave like pressing a, though. I'll look into it!

[felixlinker]

@cascremers Implemented! The only downside now is though that the key combo o still "works". When you press it on a file that does not have an oracle, you jump back to the proof's root. Not the worst, but also not ideal, and could confuse/annoy users. What do you think? Keep the change or don't? Alternatively, I'd suggest to add a comment in parentheses saying that it does the same as pressing a if there's no oracle/tactic).

From how I understand the JavaScript code, there's no easy way to fix this behavior. It's required in other contexts (#249).

tamarin-prover/data/js/tamarin-prover-ui.js

Line 740 in 779f683

if(firstStep.length >= 1) {

[cascremers]

This looks fine, thanks!