Significant proof checking refactoring #46
Conversation
Refactored CoqLspClient and CoqProofChecker to use getGoals pretac to check proofs instead of manually modifying the file. ToDo: Get rid of temporary files at all, request completion only on the current document. At least in the plugin iteslf (not in benchmarks) Reference issue: JBRes-1857
Now it doesn't have a responsibility to manage opening/closing files, the outer class calling it should be responsible for it. As we have different scenarios of communication with LSP from Plugin/Becnhmark, this is still in development. Get rid of Aux files.
Now it depends on the particular chosen Ranker. It is computed iff. ranker requires unwrapped notations.
…bort Sketch aborting the completion generation through `AbortSignal`
K-dizzled
changed the title
There was a problem hiding this comment.
As always, great work with nice decisions on code structuring!
Also, the whole love of all Coq-s 🐥, Pilot-s 🧑
I left some comments on improving the code and making it a bit clearer, but in general everything is super solid and shiny 🌟
| args.preparedProofs | ||
| ); | ||
|
|
||
| await coqLspClient.closeTextDocument(fileUri); |
There was a problem hiding this comment.
To make sure we are on the same page: am I right that in the correct implementation this closeTextDocument should be called in the finally case, while checkProofs should be wrapped into try one?
There was a problem hiding this comment.
I am not sure I understood the question( Well, in general, I guess the answer to your question is yes. The promised returned by method checkProofs could be rejected, yet, other errors shall not be thrown.
closeDocument ideally should happen in some wrapper over the coqProofChecker. Btw, would be neat to do smth like:
withOpenAuxFile:
...
...nchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts
Outdated
Show resolved
Hide resolved
...nchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts
Outdated
Show resolved
Hide resolved
| const sourceFileUri = Uri.fromPath(filePath); | ||
| await coqLspClient.openTextDocument(sourceFileUri); | ||
| const abortController = new AbortController(); |
There was a problem hiding this comment.
Another note on modifying the benchmarks, not the best way: new abortController shouldn't be created here, there is already one present at the top of the system, it just needed to be passed here.
There was a problem hiding this comment.
I tried to do that but gave up on executeOnParentProcessCall as I didn't undertand the dependencies going on in the code. I left an TODO for you to do that 👉👈
src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts
Outdated
Show resolved
Hide resolved
The version increment is minor, yet the changes are significant. The main focus of this release was to improve interaction with the
coq-lspserver. We now completely got rid of temporary files in theextensionpart ofCoqPilot. This was done thanks to ejgallego and his improvements incoq-lsp. Now checking of proofs is done via theproof/goalsrequest viacommandparameter, which is much more reliable and faster. Now a singlelspserver is created for the plugin until being explicitly closed, and it tracks changes in the file. If you are usingcoq-lspplugin itself, it will help you to always keep track of whether file is checked or not. WhenCoqPilotis ran on a completely checked file, it will not bring any significant overhead apart from requests to the Completion Services.