Sanity check refactor patch - Githubissues

coq-tactician / coq-tactician-api

An API for interfacing with Coq through Tactician by external agents

https://coq-tactician.github.io/api/introduction

MIT License

2 stars 1 forks source link

Sanity check refactor patch #3

Closed pestun closed 2 years ago

pestun commented 2 years ago

making labelled_graph_sanity_check compatibly with new capnp schema regarding ProofSteps (adressing https://github.com/coq-tactician/coq-tactician-reinforce/pull/2#discussion_r775227477)
making labelled_graph_sanity_check running in multiprocessing mode (speed up by factor of number of cores), 4 times on my laptop
making labelled_graph_sanity_check callable by `pytact-check
--jobs

Could you discard the other PR https://github.com/coq-tactician/coq-tactician-reinforce/pull/2 and merge this one ?

LasseBlaauwbroek commented 2 years ago

Thanks @pestun, looks good.

I did not realize that you were not allowed to manage issues and PR requests. I've upgraded everyone's rights from 'Write' to 'Maintain', so that should be fixed.