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.

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

Get all debug messages #842

Merged
merged 4 commits into from
Jul 24, 2024
Merged

Get all debug messages #842

merged 4 commits into from
Jul 24, 2024

Conversation

rtetley
Copy link
Collaborator

@rtetley rtetley commented Jul 23, 2024

Closes #733 #819 #820 #815.

rtetley added 2 commits July 23, 2024 16:16
Right now the idea is to forward the debug messages to an output channel.
The Info level messages are displayed in the goal view but do not trigger a diagnostic.
@TDiazT
Copy link
Contributor

TDiazT commented Jul 23, 2024

Not sure if intended, but debug logs are printed only once apparently.
For instance, in the example of #815 :

Class A.
Instance a : A := {}.

Set Typeclasses Debug.
Goal A. apply _. Qed.

The first time apply _ is interpreted, it shows the log, but subsequent executions do not.
Not sure if this a Coq or a vscoq thing.

@TDiazT
Copy link
Contributor

TDiazT commented Jul 23, 2024

Not sure if intended, but debug logs are printed only once apparently. For instance, in the example of #815 :

Class A.
Instance a : A := {}.

Set Typeclasses Debug.
Goal A. apply _. Qed.

The first time apply _ is interpreted, it shows the log, but subsequent executions do not. Not sure if this a Coq or a vscoq thing.

Not sure if intended, but debug logs are printed only once apparently. For instance, in the example of #815 :

Class A.
Instance a : A := {}.

Set Typeclasses Debug.
Goal A. apply _. Qed.

The first time apply _ is interpreted, it shows the log, but subsequent executions do not. Not sure if this a Coq or a vscoq thing.

Actually, nvm, I think it's smart enough that it only shows on code change haha. I was trying it out without any code change but then it works when one does change the file.

@rtetley
Copy link
Collaborator Author

rtetley commented Jul 24, 2024

I'll merge and will find a way to get the Document URI later

@rtetley rtetley merged commit 83586ad into main Jul 24, 2024
23 checks passed
@rtetley rtetley deleted the debug-messages branch July 24, 2024 12:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Ltac printing - where is it displayed?
3 participants