Experiment with new command to profile axioms
The command would be called on a session. For each valid proof attempt on the session, it would bisect the proof node to find the minimal set of hypotheses required for the proof. Then, for each hypothesis removed by the bisection, it would add it to the minimal set of hypotheses and retry the proof to see how the number of steps differ when adding the hypothesis. In the end, the command would ouptut an HTML file with a table listing all the axioms that are present in the session. For each axiom, there would be the following columns :
- Number of valid proof attempts where the axiom is present
- Number of valid proof attempts where the axiom is in the minimal set of axioms. If this is zero, one could argue that the axiom is not needed at all for this session.
- Number of valid proof attempts that fail when we add the axiom to the mininal set of axioms (it sometimes happen)
- Average variation of steps when we add the axiom to the minimal set of axioms. If the axioms adds a lot of extra steps in average, it might no be a good axiom to give to the prover.
For the beginning only one prover can be supported, but later the support for multiple provers could be added, so we would have different stats for all provers. Also, supporting multiple provers could be useful when only one prover manages to prove a proof node since we could use its minimal set of axioms for the other provers as well (therefore we would be able to get the steps variations metrics for the other provers as well).