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

[diagnostics] Produce backtraces automatically when an error is an anomaly. #153

Open
ejgallego opened this issue Jan 5, 2023 · 3 comments · May be fixed by #161
Open

[diagnostics] Produce backtraces automatically when an error is an anomaly. #153

ejgallego opened this issue Jan 5, 2023 · 3 comments · May be fixed by #161
Labels
kind: enhancement New feature or request part: lsp server
Milestone
0.4.0

Comments

@ejgallego
Copy link
Owner

ejgallego commented Jan 5, 2023 •
edited
Loading

We can instrument Coq_interp to do so (seems like the easiest way to do it, other approaches maybe good?)
@ejgallego ejgallego added this to the 0.1.3 milestone Jan 5, 2023
@Alizter
Copy link
Collaborator

Alizter commented Jan 6, 2023

We basically want to:

  1. Encounter an anomalous sentence.
  2. Notice it is an anomaly.
  3. Rerun it with a Debug "backtrace". prepended.

This should be similar to the implementation of auto-admitted Qeds right?

@ejgallego
Copy link
Owner Author

We basically want to:

  1. Encounter an anomalous sentence.
  2. Notice it is an anomaly.
  3. Rerun it with a Debug "backtrace". prepended.

Yes.

This should be similar to the implementation of auto-admitted Qeds right?

Good question. I was not thinking of using the error recovery system for this, but actually hooking at a lower level (like in Coq.Protect) so for fleche the process is transparent, i.e. it already gets the right exn, but what you propose could also make sense and maybe be simpler?

I guess we need to try.

@ejgallego
Copy link
Owner Author

Yeah, after thinking a bit more about this, let's try to do this in Coq.Protect. However we'll need to strengthen the invariant of callers as to ensure they are fully pure.

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 9, 2023
Merged
ejgallego added a commit that referenced this issue Jan 9, 2023
@ejgallego
[coq] Enable backtraces on anomaly
0019655 
This means we will re-execute the anomaly sentence, which may not be
very safe.

Fixes #153
@ejgallego ejgallego linked a pull request Jan 9, 2023 that will close this issue
Draft
@ejgallego ejgallego modified the milestones: 0.1.3, 0.2.0 Jan 11, 2023
ejgallego added a commit that referenced this issue Jan 20, 2023
@ejgallego
[coq] Enable backtraces on anomaly
da4399c 
This means we will re-execute the anomaly sentence, which may not be
very safe.

Fixes #153
ejgallego added a commit that referenced this issue Jan 20, 2023
@ejgallego
[coq] Enable backtraces on anomaly
53b6770 
This means we will re-execute the anomaly sentence, which may not be
very safe.

Fixes #153
ejgallego added a commit that referenced this issue Jan 20, 2023
@ejgallego
[coq] Enable backtraces on anomaly
5bf9a6f 
This means we will re-execute the anomaly sentence, which may not be
very safe.

Fixes #153
ejgallego added a commit that referenced this issue Jan 28, 2023
@ejgallego
[coq] Enable backtraces on anomaly
adcc3c8 
This means we will re-execute the anomaly sentence, which may not be
very safe.

Fixes #153
@Alizter Alizter moved this to Todo in coq-lsp roadmap Jan 29, 2023
@ejgallego ejgallego modified the milestones: 0.2.0, 0.4.0 Oct 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement New feature or request part: lsp server
Projects
coq-lsp roadmap
Status: Todo
Milestone
0.4.0
Development

Successfully merging a pull request may close this issue.

[coq] Enable backtraces on anomaly ejgallego/coq-lsp
2 participants
@ejgallego @Alizter