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

Improve error handling for Coq internal errors #91

Closed
ejgallego opened this issue Dec 8, 2022 · 5 comments · Fixed by #157, #160 or ocaml/opam-repository#22956
Closed

Improve error handling for Coq internal errors #91

ejgallego opened this issue Dec 8, 2022 · 5 comments · Fixed by #157, #160 or ocaml/opam-repository#22956
Milestone
0.1.3

Comments

@ejgallego
Copy link
Owner

ejgallego commented Dec 8, 2022 •
edited

If we get an anomaly from Fleche (usually from Coq), the way the server behaves is far from ideal.

We are also not very well protected for exceptions happening in the request code.
@ejgallego ejgallego added this to the 0.1.1 milestone Dec 8, 2022
@ejgallego ejgallego modified the milestones: 0.1.1, 0.1.2 Dec 26, 2022
@ejgallego
Copy link
Owner Author

Postponed as I forgot of an example where this bad behavior occurs.

@Alizter
Copy link
Collaborator

Alizter commented Dec 26, 2022

Aren't there known ways to get anomlies just by searching Coq issues?

@Alizter
Copy link
Collaborator

Alizter commented Dec 26, 2022

Also just load a plugin which raises an exception if you want to test.

@ejgallego
Copy link
Owner Author

Good ideas! Thanks.

@ejgallego ejgallego modified the milestones: 0.1.2, 0.1.3 Jan 4, 2023
@ejgallego
Copy link
Owner Author

ejgallego commented Jan 8, 2023 •
edited

I know have a precise description of the problem:

If we are serving a didOpen notification for example, and we get an anomaly in some path that is not handled by Coq protect, sometimes we won't add a document handler for this, then further requests fail.

The correct behavior would be I guess to cancel the request? But didOpen is just a notification, umm.

@artagnon 's patch to replace find by find_opt would already help here.

Also, we should protect the calls to Coq.Init in the same way we do with Coq interp. So really there are two thing to do here.

ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[controller] Handle failing requests better.
cf2ff0b 
This is a start to handle Coq Internal errors better. Some changes
were already in different form in the first versions of #145

c.f. #91
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[controller] Handle failing requests better.
a50e3d6 
This is a start to handle Coq Internal errors better. Some changes
were already in different form in the first versions of #145

c.f. #91
@ejgallego ejgallego mentioned this issue Jan 8, 2023
Merged
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[fleche] Protect Coq document creation
9d8b967 
`Coq.Init` will actually often `Require` Coq's prelude and perform
arbitrary actions, we now reflect this on the type.

We still have a way to improve here, but for now the code is clear and
the server will rarely crash.

Closes #91
@ejgallego ejgallego mentioned this issue Jan 8, 2023
Merged
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[fleche] Protect Coq document creation
68c227c 
`Coq.Init` will actually often `Require` Coq's prelude and perform
arbitrary actions, we now reflect this on the type.

We still have a way to improve here, but for now the code is clear and
the server should not crash anymore unless there is a real bug in
coq-lsp.

Closes #91
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[coq] Protect all base API calls
985a0ff 
Indeed I didn't realize that goal printing could raise an anomaly, due
to setting state; thus #91 is not fully fixed.

So we go full principled and make `Protect` mandatory on the exported
APIs.

TODO:
- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[coq] Protect all base API calls
113c38a 
Indeed I didn't realize that goal printing could raise an anomaly, due
to setting state; thus #91 is not fully fixed.

So we go full principled and make `Protect` mandatory on the exported
APIs.

TODO:
- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[coq] Protect all base API calls
e8acb1b 
Indeed I didn't realize that goal printing could raise an anomaly, due
to setting state; thus #91 is not fully fixed.

So we go full principled and make `Protect` mandatory on the exported
APIs.

TODO:
- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[coq] Protect all base API calls
eaae650 
Indeed I didn't realize that goal printing could raise an anomaly, due
to setting state; thus #91 is not fully fixed.

So we go full principled and make `Protect` mandatory on the exported
APIs.

TODO:
- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 8, 2023
@ejgallego
[coq] Protect all base API calls
aac9dac 
Indeed I didn't realize that goal printing could raise an anomaly, due
to setting state; thus #91 is not fully fixed.

So we go full principled and make `Protect` mandatory on the exported
APIs.

TODO:
- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
@ejgallego ejgallego mentioned this issue Jan 8, 2023
Merged
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
e4c996f 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
813a8e0 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
4043f01 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
0095b8b 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
01569ee 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
8819101 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
b0001cc 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Protect all base API calls, stop checking on anomaly
5435734 
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO: protect calls to admit, but we leave this for a further PR as it
is quite tricky due to error recovery needing rework to fully account
for `Protect.R` results.
@ejgallego ejgallego mentioned this issue Jan 13, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jan 15, 2023
@ejgallego
[new release] coq-lsp (0.1.3+v8.16)
2e26ba0 
CHANGES:

----------------------

 - Much improved handling of Coq fatal errors, the server is now
   hardened against them (@ejgallego, ejgallego/coq-lsp#155, ejgallego/coq-lsp#157, ejgallego/coq-lsp#160, fixes ejgallego/coq-lsp#91)
 - `coq-lsp` now follows the LSP specification regarding
   initialization strictly (@ejgallego, ejgallego/coq-lsp#168)
 - New setting for goals to be updated when the selection changes due
   to a command; this makes VsCodeVim cursor tracking work; thanks to
   Cactus (Anton) Golov for detailed bug reporting and testing
   (@ejgallego, @jesyspa, ejgallego/coq-lsp#170, fixes ejgallego/coq-lsp#163)
 - `coq-lsp` will now warn the user when two files have been opened
   simultaneously and the parser may go into a broken state :/
   (@ejgallego, ejgallego/coq-lsp#169)
 - Implement request postponement and cancellation. Thus
   `documentSymbols` will now be postponed until the document is
   ready, (@ejgallego, ejgallego/coq-lsp#141, ejgallego/coq-lsp#146, fixes ejgallego/coq-lsp#124)
 - Protocol and VS Code interfaces now support shelved and given_up
   goals (@ejgallego, ejgallego/coq-lsp#175)
 - Allow to postpone requests to wait for data to become available on
   document points; this is implemented to provide a nicer "show goals
   while I type" experience. Client default has been changed to "show
   goals on mouse, click, typing, and cursor movement) (@ejgallego,
   ejgallego/coq-lsp#177, ejgallego/coq-lsp#179)
 - Store stats per document (@ejgallego, ejgallego/coq-lsp#180, fixes ejgallego/coq-lsp#173)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.1.3
2 participants
@ejgallego @Alizter