Closed LasseBlaauwbroek closed 2 years ago
@pestun I have removed the RPC part of the protocol and moved to a manual protocol as we discussed. This comes with some downsides, because we now have to manually manage some bookkeeping like synchronization between processes. However, it seems to mostly be working well. At some point I'll have to improve some of the error handling, but otherwise everything seems reasonably stable.
I have also aligned the tactics to a new dataset v8-global
. For simple Coq developments, both tactics and definitions should now be aligned. Let me know if you encounter any problems. Note that for developments that include module functors or sections the alignment is still not complete. This will require yet another change in the dataset that I'm working on now.
I'm going to merge this PR, as it is now the basis of the latest dataset v8
.
This is just the wireframe, nothing is implemented yet.
In this proposal, the initial handshake would work as follows (this is similar to before, except that the Python process is now started by Coq instead of the other way around).
Main.initialize
function (as it was already doing before).synth
tactic is executed in Coq (or when we run a benchmark), Coq will call thePushReinforce.predictionContext
function to initialize the Python process for doing search. (Yes,PushReinforce
is a terrible name, feel free to come up with a better one).