Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix-ups for "significant proof checking refactoring" #48

Merged
merged 21 commits into from
Nov 26, 2024

Conversation

GlebSolovev
Copy link
Collaborator

@GlebSolovev GlebSolovev commented Nov 15, 2024

Unfortunately, the last refactoring PR was closed too quickly and without proper review, resulting in several vulnerabilities in the code.

The goal of this PR is to fix the key issues and improve code style where possible.

👮 Fix-ups

  • remove redundant checks for Theorem.proof nullability
  • use ProofGoal alias again instead of Goal<PpString>
  • implement CoqLspClient.getFirstGoalAtPointOrThrow(...) properly: this method should be the only call needed, rather than chained after the getGoalsAtPoint
    • apply it wherever applicable
  • fix imm submodule commit: it should point at the existing commit (as it was made in main), otherwise it won't work in TeamCity
  • wrap working with Coq documents and coq-lsp into correct try-finally-s with actually needed disposal (in hopefully all of the places where coq-lsp is used)
    • document CoqLspClient invariants
  • fix SessionState.restartSession() bug (not all the fields were updated) and remove aborting from its dispose() method
  • fix bugs found inside the internal signatures of the benchmarking framework
    • the most significant one: file URI was serialised incorrectly (non-implemented toString() call) causing the proof-checker to fail
  • move abort utils into the core directory: since core functions use these utils, they shouldn't stay in the extension folder
  • implement proper abort controller passing in the benchmarks
  • narrow down the usage of the abort controller to the abort signal: it makes intentions clearer and helps not to require the controller where it is not accessible

⚠️ Detected vulnerabilities to discuss

  • Is coq-lsp capable of maintaining several docs opened? If not, the document's opening and closing should be performed under the same mutex together
    • Answer: yes, it should be capable of.
  • How does CoqPilot handle the user spamming the abort&restart plugin button (i.e. multiple fast toggles)?
    • Answer: it has not been tested so far. We should test it later.
  • Shouldn't CoqLspClient.dispose() be awaited?
    • Answer: though it should be, we can omit that. CoqLspClient-s starts separate processes that have nothing shared; therefore, it is okay to dispose the old one later asynchronously without waiting for it explicitly.
  • It would be clearer and safer to initialise a new SessionState object instead of restarting the same one; is it possible?
    • Answer: As SessionState has the activeSession boolean trigger, it could not be destructed completely, therefore it is recreated.

👍 General improvements

  • improve namings in SessionState
  • restructure theorem rankers directory
  • update code style of parsedTypes.ts classes
  • introduce CoqLspClient.withTextDocument(...) wrapper to encapsulate opening and closing a document with coq-lsp
    • applied wherever applicable
  • introduce "with-coq-lsp" wrappers to encapsulate correct CoqLspClient disposal
  • refactor legacy benchmarks options, fix empty report creation bug
  • improve naming of CoqProofChecker.checkProofs(...) arguments & get rid of unused CoqProofCheckerInterface
  • structure extension directory: it became pretty hard to use because of a huge number of files inside

@K-dizzled K-dizzled merged commit 9be1b07 into v2.4.0-dev Nov 26, 2024
3 checks passed
@K-dizzled K-dizzled deleted the proof-checking-refactor-fix branch November 26, 2024 10:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants