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.

Sign up for GitHub

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

Jump to bottom

Significant proof checking refactoring #46

Merged
merged 33 commits into from
Nov 6, 2024
Merged

Significant proof checking refactoring #46

merged 33 commits into from
Nov 6, 2024

Commits on Jul 29, 2024

  1. Implement base use of feature to check proofs. Needs fixes

    @K-dizzled
    K-dizzled committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    2361b69 View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2024

  1. Test and integrte command arg of getGoals to check proofs 

    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
    @K-dizzled
    K-dizzled committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    9e9b6e1 View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2024

  1. Merge main into core-lsp-rework

    @K-dizzled
    K-dizzled committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    415f71d View commit details
    Browse the repository at this point in the history

  2. Upgrade coq-lsp in actions to v0.2.2 for arg in getGoals

    @K-dizzled
    K-dizzled committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    d5c66ac View commit details
    Browse the repository at this point in the history

  3. Change type of CoqLspClient to Interface everywhere possible

    @K-dizzled
    K-dizzled committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    09c957e View commit details
    Browse the repository at this point in the history

  4. Clean CoqLspClientInterface

    @K-dizzled
    K-dizzled committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    e32b7f9 View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2024

  1. Refactor CoqProofChecker 

    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.
    @K-dizzled
    K-dizzled committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    9125619 View commit details
    Browse the repository at this point in the history

  2. Clean-up

    @K-dizzled
    K-dizzled committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    ad795e7 View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. Refactor creating in plugin mode: now once in

    @K-dizzled
    K-dizzled committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    872987b View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2024

  1. Create decorator that logs execution time of the method

    @K-dizzled
    K-dizzled committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    e97e1ec View commit details
    Browse the repository at this point in the history

  2. Make computation of initialGoal optional 

    Now it depends on the particular chosen Ranker. It is computed iff. ranker requires unwrapped notations.
    @K-dizzled
    K-dizzled committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    5baf1f8 View commit details
    Browse the repository at this point in the history

  3. Create permanent status bar button

    @K-dizzled
    K-dizzled committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    9319114 View commit details
    Browse the repository at this point in the history

  4. Add refactor TODO to

    @K-dizzled
    K-dizzled committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    b2c18bf View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2024

  1. Sketch aborting the completion generation through AbortSignal

    @K-dizzled
    K-dizzled committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    3f44690 View commit details
    Browse the repository at this point in the history

  2. Refactor SourceFileEnvironment: remove dirPath and rename 

    fileVersion
    @K-dizzled
    K-dizzled committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    9689e85 View commit details
    Browse the repository at this point in the history

  3. Refactor SourceFileEnvironment: remove fileLines

    @K-dizzled
    K-dizzled committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    095b99b View commit details
    Browse the repository at this point in the history

  4. Refactor checkGeneratedProofs

    @K-dizzled
    K-dizzled committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    df91211 View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2024

  1. Minor changes after sketching completion abort in extension

    @K-dizzled
    K-dizzled committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    632c80a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'core-lsp-rework' into extension-completion-abort

    @K-dizzled
    K-dizzled authored Oct 26, 2024
    Configuration menu
    Copy the full SHA
    7530442 View commit details
    Browse the repository at this point in the history

  3. Merge pull request #45 from JetBrains-Research/extension-completion-a… 

    …bort

Sketch aborting the completion generation through `AbortSignal`
    @K-dizzled
    K-dizzled authored Oct 26, 2024
    Configuration menu
    Copy the full SHA
    e56e10e View commit details
    Browse the repository at this point in the history

  4. Fix merge of abort-completion into core-lsp-refactor

    @K-dizzled
    K-dizzled committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    d8f591f View commit details
    Browse the repository at this point in the history

  5. Add TODOs on LspCoreRefactor

    @K-dizzled
    K-dizzled committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    0ec7316 View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2024

  1. Create SessionExtensionState

    @K-dizzled
    K-dizzled committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    cdd87b3 View commit details
    Browse the repository at this point in the history

  2. Refactor CoqLspClient to CoqLspClientImpl

    @K-dizzled
    K-dizzled committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    34bdfa2 View commit details
    Browse the repository at this point in the history

  3. Finalize aborting coq-lsp gracefully

    @K-dizzled
    K-dizzled committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    bab8a26 View commit details
    Browse the repository at this point in the history

  4. Prepare for v2.3.1 release

    @K-dizzled
    K-dizzled committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    e122675 View commit details
    Browse the repository at this point in the history

Commits on Nov 6, 2024

  1. Fix cosmetics from review in PR#46

    @K-dizzled
    K-dizzled committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    33d1197 View commit details
    Browse the repository at this point in the history

  2. Fix more issues from review in PR#46

    @K-dizzled
    K-dizzled committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    d1d4952 View commit details
    Browse the repository at this point in the history

  3. Code style fixes and core in rankers from review in PR#46

    @K-dizzled
    K-dizzled committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    09a3420 View commit details
    Browse the repository at this point in the history

  4. Refactoring healthStatusIndicator according to review in PR#46

    @K-dizzled
    K-dizzled committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    c58c89f View commit details
    Browse the repository at this point in the history

  5. Renamings according to review in PR#46

    @K-dizzled
    K-dizzled committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    a8ac5b8 View commit details
    Browse the repository at this point in the history

  6. More accurate completionAbortError handling

    @K-dizzled
    K-dizzled committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    0b36cc3 View commit details
    Browse the repository at this point in the history

  7. Refactor coqLsp tests according to review of PR#46

    @K-dizzled
    K-dizzled committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    f5122cd View commit details
    Browse the repository at this point in the history