Code

Release v2.4.0+0.2.2+8.19#50

Code

Merged

K-dizzled merged 75 commits intomainJetBrains-Research/coqpilot:mainfrom v2.4.0-devJetBrains-Research/coqpilot:v2.4.0-devCopy head branch name to clipboardNov 27, 2024

+1,902-1,309

Commits

Commits on Jul 29, 2024

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

  K-dizzled

  committed
  2361b69

  Copy full SHA for 2361b69

Commits on Oct 9, 2024

• Test and integrte command arg of getGoals to check proofs

  Show description for 9e9b6e1
  K-dizzled

  committed
  9e9b6e1

  Copy full SHA for 9e9b6e1

Commits on Oct 16, 2024

• Merge main into core-lsp-rework

  K-dizzled

  committed
  415f71d

  Copy full SHA for 415f71d

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

  K-dizzled

  committed
  d5c66ac

  Copy full SHA for d5c66ac

• Change type of CoqLspClient to Interface everywhere possible

  K-dizzled

  committed
  09c957e

  Copy full SHA for 09c957e

• Clean CoqLspClientInterface

  K-dizzled

  committed
  e32b7f9

  Copy full SHA for e32b7f9

Commits on Oct 17, 2024

• Refactor CoqProofChecker

  Show description for 9125619
  K-dizzled

  committed
  9125619

  Copy full SHA for 9125619

• Clean-up

  K-dizzled

  committed
  ad795e7

  Copy full SHA for ad795e7

Commits on Oct 18, 2024

• Refactor creating in plugin mode: now once in

  K-dizzled

  committed
  872987b

  Copy full SHA for 872987b

Commits on Oct 20, 2024

• Create decorator that logs execution time of the method

  K-dizzled

  committed
  e97e1ec

  Copy full SHA for e97e1ec

• Make computation of initialGoal optional

  Show description for 5baf1f8
  K-dizzled

  committed
  5baf1f8

  Copy full SHA for 5baf1f8

• Create permanent status bar button

  K-dizzled

  committed
  9319114

  Copy full SHA for 9319114

• Add refactor TODO to

  K-dizzled

  committed
  b2c18bf

  Copy full SHA for b2c18bf

Commits on Oct 25, 2024

• Sketch aborting the completion generation through AbortSignal

  K-dizzled

  committed
  3f44690

  Copy full SHA for 3f44690

• Refactor SourceFileEnvironment: remove dirPath and rename

  Show description for 9689e85
  K-dizzled

  committed
  9689e85

  Copy full SHA for 9689e85

• Refactor SourceFileEnvironment: remove fileLines

  K-dizzled

  committed
  095b99b

  Copy full SHA for 095b99b

• Refactor checkGeneratedProofs

  K-dizzled

  committed
  df91211

  Copy full SHA for df91211

Commits on Oct 26, 2024

• Minor changes after sketching completion abort in extension

  K-dizzled

  committed
  632c80a

  Copy full SHA for 632c80a

• Merge branch 'core-lsp-rework' into extension-completion-abort

  K-dizzled

  authored
  7530442

  Copy full SHA for 7530442

• Merge pull request #45 from JetBrains-Research/extension-completion-abort

  Show description for e56e10e
  K-dizzled

  authored
  e56e10e

  Copy full SHA for e56e10e

• Fix merge of abort-completion into core-lsp-refactor

  K-dizzled

  committed
  d8f591f

  Copy full SHA for d8f591f

• Add TODOs on LspCoreRefactor

  K-dizzled

  committed
  0ec7316

  Copy full SHA for 0ec7316

Commits on Oct 27, 2024

• Create SessionExtensionState

  K-dizzled

  committed
  cdd87b3

  Copy full SHA for cdd87b3

• Refactor CoqLspClient to CoqLspClientImpl

  K-dizzled

  committed
  34bdfa2

  Copy full SHA for 34bdfa2

• Finalize aborting coq-lsp gracefully

  K-dizzled

  committed
  bab8a26

  Copy full SHA for bab8a26

• Prepare for v2.3.1 release

  K-dizzled

  committed
  e122675

  Copy full SHA for e122675

Commits on Oct 29, 2024

• docs: update README.md

  Show description for 4c276e9
  eltociear

  authored
  4c276e9

  Copy full SHA for 4c276e9

• Merge pull request #47 from eltociear/patch-1

  Show description for 848b762
  K-dizzled

  authored
  848b762

  Copy full SHA for 848b762

Commits on Nov 6, 2024

• Fix cosmetics from review in PR#46

  K-dizzled

  committed
  33d1197

  Copy full SHA for 33d1197

• Fix more issues from review in PR#46

  K-dizzled

  committed
  d1d4952

  Copy full SHA for d1d4952

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

  K-dizzled

  committed
  09a3420

  Copy full SHA for 09a3420

• Refactoring healthStatusIndicator according to review in PR#46

  K-dizzled

  committed
  c58c89f

  Copy full SHA for c58c89f

• Renamings according to review in PR#46

  K-dizzled

  committed
  a8ac5b8

  Copy full SHA for a8ac5b8

• More accurate completionAbortError handling

  K-dizzled

  committed
  0b36cc3

  Copy full SHA for 0b36cc3

• Refactor coqLsp tests according to review of PR#46

  K-dizzled

  committed
  f5122cd

  Copy full SHA for f5122cd

• Merge pull request #46 from JetBrains-Research/core-lsp-rework

  Show description for 75c46d3
  K-dizzled

  authored
  75c46d3

  Copy full SHA for 75c46d3

• Change v2.3.1 to v2.4.0 as changes are major

  K-dizzled

  committed
  d72fa49

  Copy full SHA for d72fa49

Commits on Nov 15, 2024

• Refactor SessionState & highlight vulnerabilities

  GlebSolovev

  committed
  f70deac

  Copy full SHA for f70deac

• Restructure theorem rankers, add comments

  GlebSolovev

  committed
  5b5abb1

  Copy full SHA for 5b5abb1

• Remove redundant null-checks for theorem proof

  GlebSolovev

  committed
  e64f491

  Copy full SHA for e64f491

• Make code style of parsedTypes.ts consistent

  GlebSolovev

  committed
  1d158bc

  Copy full SHA for 1d158bc

• Format code

  GlebSolovev

  committed
  66d0d43

  Copy full SHA for 66d0d43

• Use ProofGoal instead of Goal<PpString>

  GlebSolovev

  committed
  16831af

  Copy full SHA for 16831af

• Implement getFirstGoalOrThrow wrapper properly

  GlebSolovev

  committed
  ca16531

  Copy full SHA for ca16531

• Improve code style of coq-lsp tests

  GlebSolovev

  committed
  34d48f3

  Copy full SHA for 34d48f3

• Introduce withTextDocument wrapper

  GlebSolovev

  committed
  8b3a621

  Copy full SHA for 8b3a621

• Fix imm submodule commit

  GlebSolovev

  committed
  8abe2eb

  Copy full SHA for 8abe2eb

• Introduce with-coq-lsp wrappers, dispose client correctly

  GlebSolovev

  committed
  ea7805b

  Copy full SHA for ea7805b

Commits on Nov 16, 2024

• Fix SessionState bugs, improve its code style

  GlebSolovev

  committed
  b0c20a4

  Copy full SHA for b0c20a4

• Fix coq-lsp usage in legacy benchmarks, refactor args

  GlebSolovev

  committed
  da02a28

  Copy full SHA for da02a28

• Prevent legacy benchmarks from creating empty report on start

  GlebSolovev

  committed
  1cc6ffd

  Copy full SHA for 1cc6ffd

• Fix coq-lsp usage at parsing stage of benchmarks

  GlebSolovev

  committed
  649402d

  Copy full SHA for 649402d

• Document CoqLspClient invariants

  GlebSolovev

  committed
  729153b

  Copy full SHA for 729153b

• Improve CoqProofChecker code style

  GlebSolovev

  committed
  09f914a

  Copy full SHA for 09f914a

• Fix bugs in internal signatures of benchmarks

  Show description for a129ca9
  GlebSolovev

  committed
  a129ca9

  Copy full SHA for a129ca9

• Move abort utils into core

  GlebSolovev

  committed
  78dd974

  Copy full SHA for 78dd974

• Structure extension directory

  GlebSolovev

  committed
  7c3d5d6

  Copy full SHA for 7c3d5d6

Commits on Nov 17, 2024

• Support abort signal set-up in coq-lsp client wrappers

  Show description for 3a8ffc2
  GlebSolovev

  committed
  3a8ffc2

  Copy full SHA for 3a8ffc2

Commits on Nov 26, 2024

• Merge pull request #48 from JetBrains-Research/proof-checking-refactor-fix

  Show description for 9be1b07
  K-dizzled

  authored
  9be1b07

  Copy full SHA for 9be1b07

• Update CHANGELOG with major updates from PR#48

  K-dizzled

  committed
  28d4826

  Copy full SHA for 28d4826

• Small code-style issue refactor in GrazieService

  K-dizzled

  committed
  43e676f

  Copy full SHA for 43e676f

• Fix failing Date parsing tests on Mac

  K-dizzled

  committed
  0ec4392

  Copy full SHA for 0ec4392

• Fix issue with systemMessage for gpt-o1

  K-dizzled

  committed
  cff44b9

  Copy full SHA for cff44b9

• Clarify abort controller usage at parsing stage of benchmarking

  GlebSolovev

  committed
  0fc8d1d

  Copy full SHA for 0fc8d1d

• Support initial_goal being optional inside benchmarking

  GlebSolovev

  committed
  e867f00

  Copy full SHA for e867f00

• Get initial_goal cached more often

  GlebSolovev

  committed
  7dcd906

  Copy full SHA for 7dcd906

• Make needsTheoremInitialGoals required

  GlebSolovev

  committed
  35130f8

  Copy full SHA for 35130f8

• Fix bug with different o1 class models name in Grazie

  K-dizzled

  committed
  2eb29a1

  Copy full SHA for 2eb29a1

• Update README with Related Papers and update future plans

  K-dizzled

  committed
  3aff82a

  Copy full SHA for 3aff82a

Commits on Nov 27, 2024

• Add TODO for initial-goals flag support inside benchmarking

  GlebSolovev

  committed
  477a0e8

  Copy full SHA for 477a0e8

• Fix multi-workspaces "pre" script

  GlebSolovev

  committed
  b1cd890

  Copy full SHA for b1cd890

• Provide benchmark-test task for faster development

  GlebSolovev

  committed
  86ec217

  Copy full SHA for 86ec217

• Add notes on COQ_LSP_PATH to benchmarking docs

  GlebSolovev

  committed
  d5dda34

  Copy full SHA for d5dda34

• Update info on coq-lsp via nix usage

  K-dizzled

  committed
  b4c0a3b

  Copy full SHA for b4c0a3b

• Merge pull request #49 from JetBrains-Research/benchmarking-hotfixes

  Show description for 1048803
  K-dizzled

  authored
  1048803

  Copy full SHA for 1048803