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

Release v2.4.0+0.2.2+8.19 #50

Merged
merged 75 commits into from
Nov 27, 2024
Merged

Release v2.4.0+0.2.2+8.19 #50

merged 75 commits into from
Nov 27, 2024

Conversation

K-dizzled
Copy link
Collaborator

No description provided.

K-dizzled and others added 30 commits July 29, 2024 16:05
@K-dizzled
Implement base use of feature to check proofs. Needs fixes
2361b69
@K-dizzled
Test and integrte command arg of getGoals to check proofs
9e9b6e1 
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
Merge main into core-lsp-rework
415f71d
@K-dizzled
Upgrade coq-lsp in actions to v0.2.2 for arg in getGoals
d5c66ac
@K-dizzled
Change type of CoqLspClient to Interface everywhere possible
09c957e
@K-dizzled
Clean CoqLspClientInterface
e32b7f9
@K-dizzled
Refactor CoqProofChecker
9125619 
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
Clean-up
ad795e7
@K-dizzled
Refactor creating in plugin mode: now once in
872987b
@K-dizzled
Create decorator that logs execution time of the method
e97e1ec
@K-dizzled
Make computation of initialGoal optional
5baf1f8 
Now it depends on the particular chosen Ranker. It is computed iff. ranker requires unwrapped notations.
@K-dizzled
Create permanent status bar button
9319114
@K-dizzled
Add refactor TODO to
b2c18bf
@K-dizzled
Sketch aborting the completion generation through AbortSignal
3f44690
@K-dizzled
Refactor SourceFileEnvironment: remove dirPath and rename
9689e85 
fileVersion
@K-dizzled
Refactor SourceFileEnvironment: remove fileLines
095b99b
@K-dizzled
Refactor checkGeneratedProofs
df91211
@K-dizzled
Minor changes after sketching completion abort in extension
632c80a
@K-dizzled
Merge branch 'core-lsp-rework' into extension-completion-abort
7530442
@K-dizzled
Merge pull request #45 from JetBrains-Research/extension-completion-a…
e56e10e 
…bort

Sketch aborting the completion generation through `AbortSignal`
@K-dizzled
Fix merge of abort-completion into core-lsp-refactor
d8f591f
@K-dizzled
Add TODOs on LspCoreRefactor
0ec7316
@K-dizzled
Create SessionExtensionState
cdd87b3
@K-dizzled
Refactor CoqLspClient to CoqLspClientImpl
34bdfa2
@K-dizzled
Finalize aborting coq-lsp gracefully
bab8a26
@K-dizzled
Prepare for v2.3.1 release
e122675
@eltociear
docs: update README.md
4c276e9 
instrustion -> instruction
@K-dizzled
Merge pull request #47 from eltociear/patch-1
848b762 
docs: fix typo in README.md
@K-dizzled
Fix cosmetics from review in PR#46
33d1197
@K-dizzled
Fix more issues from review in PR#46
d1d4952
GlebSolovev and others added 29 commits November 15, 2024 12:14
@GlebSolovev
Fix imm submodule commit
8abe2eb
@GlebSolovev
Introduce with-coq-lsp wrappers, dispose client correctly
ea7805b
@GlebSolovev
Fix SessionState bugs, improve its code style
b0c20a4
@GlebSolovev
Fix coq-lsp usage in legacy benchmarks, refactor args
da02a28
@GlebSolovev
Prevent legacy benchmarks from creating empty report on start
1cc6ffd
@GlebSolovev
Fix coq-lsp usage at parsing stage of benchmarks
649402d
@GlebSolovev
Document CoqLspClient invariants
729153b
@GlebSolovev
Improve CoqProofChecker code style
09f914a
@GlebSolovev
Fix bugs in internal signatures of benchmarks
a129ca9 
Caused by recent refactoring
@GlebSolovev
Move abort utils into core
78dd974
@GlebSolovev
Structure extension directory
7c3d5d6
@GlebSolovev
Support abort signal set-up in coq-lsp client wrappers
3a8ffc2 
Pass abort signal into coq-lsp client correctly in benchmarks
@K-dizzled
Merge pull request #48 from JetBrains-Research/proof-checking-refacto…
9be1b07 
…r-fix

Fix-ups for "significant proof checking refactoring"
@K-dizzled
Update CHANGELOG with major updates from PR#48
28d4826
@K-dizzled
Small code-style issue refactor in GrazieService
43e676f
@K-dizzled
Fix failing Date parsing tests on Mac
0ec4392
@K-dizzled
Fix issue with systemMessage for gpt-o1
cff44b9
@GlebSolovev
Clarify abort controller usage at parsing stage of benchmarking
0fc8d1d
@GlebSolovev
Support initial_goal being optional inside benchmarking
e867f00
@GlebSolovev
Get initial_goal cached more often
7dcd906
@GlebSolovev
Make needsTheoremInitialGoals required
35130f8
@K-dizzled
Fix bug with different o1 class models name in Grazie
2eb29a1
@K-dizzled
Update README with Related Papers and update future plans
3aff82a
@GlebSolovev
Add TODO for initial-goals flag support inside benchmarking
477a0e8
@GlebSolovev
Fix multi-workspaces "pre" script
b1cd890
@GlebSolovev
Provide benchmark-test task for faster development
86ec217
@GlebSolovev
Add notes on COQ_LSP_PATH to benchmarking docs
d5dda34
@K-dizzled
Update info on coq-lsp via nix usage
b4c0a3b
@K-dizzled
Merge pull request #49 from JetBrains-Research/benchmarking-hotfixes
1048803 
Benchmarking framework hot-fixes
@K-dizzled K-dizzled merged commit 40142f2 into main Nov 27, 2024
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@K-dizzled @eltociear @GlebSolovev