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

General fixes #11

Merged
merged 27 commits into from
Sep 22, 2023
Merged

General fixes #11

merged 27 commits into from
Sep 22, 2023

Conversation

pcarrott
Copy link
Collaborator

Improvements:

  1. Increase default timeout
  2. Create Timeout exception
  3. Create NotationNotFound exception
  4. Make AST traversals iterative

Main changes and additions:

  1. Add support for new Coq keywords
  2. CoqFile keeps a list of steps instead of plain text and AST
  3. Each step stores the associated diagnostics
  4. Handle where-notations with Unicode characters
  5. Constrain regex expression for notation wildcards

pcarrott and others added 23 commits September 5, 2023 17:36
@pcarrott
Handle Goal keyword
9463524
@pcarrott
Minor fix: index check
40ab1af
@pcarrott
Fix scope of notations to capture list notations
9e2620e
@pcarrott
Minor fix removing whitespace from notations
af7db68
@pcarrott
Fix locate libraries
0457326
@pcarrott
Avoid RecursionError by making traverse_ast iterative
2314648
@pcarrott
Rename traverse_ast as traverse_expr and replace deque with reversed …
f39d7c1 
…list
@pcarrott
Fix bullets and where notations
1f23228
@pcarrott
Handle Unicode characters in where notations
0949e47
@pcarrott
Add more characters in regex wildcard for notations
417cc54
@pcarrott
Add keywords for Setoids and Relations
25c02ec
@pcarrott
Minor refactor: get_id and reversed
ceac087
@pcarrott
Add keywords Function, CoFixpoint and CoInductive
73521f4
@pcarrott
Add keyword Derive
63bcad2
@pcarrott
Increase default timeout, refactor exceptions (new error codes for Se…
08c8212 
…rverTimeout and NotationNotFound)
@pcarrott
Minor fix
2d84bf3
@Nfsaavedra
improve running files with errors but our program became an error
0acc104
@pcarrott
Only copy files from Coq.Init and not all files from Coq
afd67bd
@Nfsaavedra
CoqFile refactor. Add diagnostics to steps
6ccf319
@pcarrott
Fix diagnostic range for steps
69f9bdf
@pcarrott
Comparison operators for Position
22835d2
@pcarrott
Remove lines and AST from CoqFile, keep list of Steps
245c09d
@pcarrott
Temporary fix to anonymous instances
36e048c
@pcarrott pcarrott requested a review from Nfsaavedra September 22, 2023 16:14
Nfsaavedra
Nfsaavedra reviewed Sep 22, 2023
View reviewed changes
README.md Show resolved Hide resolved
pylspclient/lsp_structs.py Outdated Show resolved Hide resolved
@pcarrott pcarrott merged commit 695726b into master Sep 22, 2023
2 checks passed
@pcarrott pcarrott deleted the general_fixes branch September 22, 2023 21:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Nfsaavedra Nfsaavedra Nfsaavedra left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@pcarrott @Nfsaavedra