Where can we see the result of type or compute in VSCode mode?

[amelieled]

I don't know if it's a missing feature or something to clarify in the documentation.

[fblanqui]

The type of symbols is given by hoover I think. The result of compute is not provided I think. This could be given by hoover too. Perhaps @firewall2142 could add this feature?

[amelieled]

The type of symbols is given by hoover I think

Yes, so the command type isn't useful.

[amelieled]

The result of compute is not provided I think.

Exactly.

[amelieled]

How do you activate hoover?
And where do you want the result will be display? As in CoqIde/ProofGeneral (hybrid mode)?
I think it's very important to split debug console (~"set debug"), goal display, and "queries" results (~type, compute, assert, assertnot).

[firewall2142]

How do you activate hoover?

I assume everyone meant hover, it should be active by default in vscode

I think it's very important to split debug console (~"set debug"), goal display, and "queries" results (~type, compute, assert, assertnot).

OK, I will keep that in mind if I implement the feature

[amelieled]

I assume everyone meant hover, it should be active by default in vscode

Yes, I understand now. Thanks.

[amelieled]

OK, I will keep that in mind if I implement the feature

Ask @fblanqui before, in order to understand what he prefers exactly.
In my opinion, something like this is perfect:
https://coq.inria.fr/refman/practical-tools/coqide.html :)

[fblanqui]

For setting the verbose level, the debug flags, etc. it could be nice to have menus. But would it be possible to send these commands without writing them in the source file?

[firewall2142]

I managed to implement the debug and hover features over the weekend (though I need to fix a few things). Now that the debug logs are done, the menus shouldn't be much of a problem as I can change the default values of those variables.

[fblanqui]

The results of type and compute is now printed in a new log tab. See #518 for more details.