search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Get all debug messages #842

Closed rtetley closed 2 months ago

rtetley commented 2 months ago

Closes #733 #819 #820 #815.

TDiazT commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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