Printing a module has no new lines or component disambiguation

[Alizter]

Printing a module does not use any new lines or disambiguate between components:

These should be bulleted and newlined.

Module A.
Axiom A : Type.
Axiom B : Type.
Axiom C : Type.
Axiom D : Type.
Axiom E : Type.
End A.

Print A.

[LasseBlaauwbroek]

I just ran into this issue as well while trying Tactician with coq-lsp. No newlines are being printed in any of the messages.
(Otherwise, the two seem to be working well together. I'm a bit surprised because Tactician has some dependencies on the SMT. I'd have expected coq-lsp not to use the STM.)

[ejgallego]

@LasseBlaauwbroek , indeed the pretty printer needs more work, you can workaround that by setting the "Coq-Lsp: Pp_type" setting to 0. But that loses some nice rending. I'll have a look soon.

I'm a bit surprised because Tactician has some dependencies on the SMT. I'd have expected coq-lsp not to use the STM.

coq-lsp has its own plugin loader, if your plugin requires the stm I think it should be capable of loading it indeed.

[ejgallego]

Thanks a lot for the feedback by the way!

[LasseBlaauwbroek]

coq-lsp has its own plugin loader, if your plugin requires the stm I think it should be capable of loading it indeed.

I'm a bit confused by how this works. My understanding is that lsp bypasses the stm completely right? But Tactician relies on the stm to retrieve the current vernacular command is (for the purpose of evil hacks). How does the stm know this information when it is being bypassed?

[ejgallego]

I have no idea how this may be working indeed, the Stm will be loaded but no code will be called.

Do you have a pointer to the code where you call the Stm?

[LasseBlaauwbroek]

Here is the main usage:
https://github.com/coq-tactician/coq-tactician/blob/9310c3d0bbfbe146f8ef8e56b94efce7a31019a9/src/ltacrecord.ml#L926-L933
I guess it is possible that with Flèche, this code path is actually completely avoided. (I don't know what to call Flèche and what to call coq-lsp.)

Second use is here, during discharging of sections:
https://github.com/coq-tactician/coq-tactician/blob/9310c3d0bbfbe146f8ef8e56b94efce7a31019a9/src/inline_private_constants.ml#L74-L79
But I didn't test sections yet, so perhaps this is indeed broken.

[ejgallego]

I see thanks! In this case things are fine by chance tho, both calls are indeed done, I think, but they return None, and the inlining stuff is not needed as I use a simpler semantics for incremental proof checking.

I don't know what to call Flèche and what to call coq-lsp.

Flèche is the protocol-independent checking engine, main entry points are fleche/{doc,theory}.mli.

For example the command line fcc compiler we have uses it.

coq-lsp is a thin layer over Flèche implementing the LSP protocol. This is easy as we designed Flèche's API to work well in LSP.

Indeed this repository has several components, it'd be nice to split them eventually, but for now that'd be a bit of a PITA in terms of submodules etc...

Any suggestion on how to makes this less confusing is much appreciated!

[LasseBlaauwbroek]

I was wrong about the section discharging. The second snippet is used for inlining of constants generated by abstract.

I tested all this again, and magically, no error is ever thrown about any of this. It seems that the code path is indeed avoided.

However, this does bring up a potential bug in abstract for coq-lsp:

Theorem k : 0 = 0.
Proof.
abstract reflexivity.
Qed.
Print k.
(* k = k_subproof
: 0 = 0 *)

When you try the same thing in Coqide or coqc, you get

(fun k_subproof : 0 = 0 => k_subproof) eq_refl
     : 0 = 0

Coq-lsp is not inlining these definitions.

[ejgallego]

By the way, the equivalent API in Fleche to query this info is in fleche/info.ml .

However something like tactician would not call this API directly, it would register for example "tell me when the user imports the new tactic", so you'd get the Ast directly in the callback.

[ejgallego]

Coq-lsp is not inlining these definitions.

Indeed, the semantics are a bit different, but I'm not sure Coq's current behavior is the sane one tho. There are some issues upstream about what to do with this. AFAICT inling was done due to limitations on the Stm, not because it is the "right thing to do". On the contrary, Defined will not inline. I find this puzzling.

Does the inlining matter for Tactician?

[LasseBlaauwbroek]

The abstract tactic is horrible for Tactician. So many hours and lines of code have been devoted to it... I'd rather see it gone completely.

Does the inlining matter for Tactician?

Only in the sense that if Coq inlines a definition, then Tactician has to do it too. I need to be consistent, and it appears that it is indeed so.

On the contrary, Defined will not inline. I find this puzzling.

Indeed, and this is exactly why I have to query the stm. I need to know if we are doing Qed or Defined to decide wether I need to inline.

[ejgallego]

I see.

Indeed a better situation for Tactician would be the Stm letting you register your hooks. We had to rewrite the Stm, but the idea with coq-lsp is that you don't need to care about this anymore hopefully.

I can see how much pain this has been, I'm amazed by all the code you have written!

[ejgallego]

Indeed, and this is exactly why I have to query the stm. I need to know if we are doing Qed or Defined to decide wether I need to inline.

In coq-lsp we have simpler semantics, never inline. This may indeed be the right thing to do, but it is indeed not fully backwards compatible, we will see what it is done upstream.

[LasseBlaauwbroek]

Indeed a better situation for Tactician would be the Stm letting you register your hooks.

Yes. I just never have the time to try to upstream some PRs that let me fix some of my evil hacks.

it would register for example "tell me when the user imports the new tactic", so you'd get the Ast directly in the callback.

Where would I register this? Not that I need it now, but good to know.

In coq-lsp we have simpler semantics, never inline.

Great, all the more easy for me :-)

[ejgallego]

Where would I register this? Not that I need it now, but good to know.

In this case you'd call Doc.Register, but I have not added this API to main yet. But I'm very happy to do so.

There are for now only two plugin API that have landed in main, fleche/theory.ml:Register and one for LSP hover in rq_hover.ml.

The policy I have is that I don't add any extension point until at least there is an interest for the client.

The actions of interest for documents are:

• Errors
• New sentence
• New structural element (3 options here, to call on open, on close)
• New tactic

etc... Registration can add data to document nodes (see fleche/doc.mli for the Node.t type)

If you can describe the hooks tactician needs in terms of functions, I can put them in the next release next week.

[ejgallego]

Great, all the more easy for me :-)

It seems to me that you should not have to take care of this in the first place, right?

[LasseBlaauwbroek]

If you can describe the hooks tactician needs in terms of functions, I can put them in the next release next week.

See conversation in the other thread.

It seems to me that you should not have to take care of this in the first place, right?

Ideally, no. But in practice, I have to do rewriting and inlining of my data in multiple places. One is inlining of abstract, but this also happens during section discharge and module functor instantiation. Module functors are fairly easy to deal with, but section discharging is a pain because Coq is intentionally hiding all the discharging implementation code. I tried to get this exposed more, but I was unsuccessful.

[ejgallego]

The reason you are handling discharge yourself is because you need to attach structure-specific data?

[LasseBlaauwbroek]

Yeah, for each lemma, we record information about the execution of tactics. This includes the proof state it was run on, the proof states it has generated and the partial proof term it has created. Since this information contains terms, those terms need to be discharged properly in order to remain valid.

[ejgallego]

I see, thanks for the info!