Stream: Coq devs & plugin devs

Topic: parsing separation API


view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 14:26):

https://github.com/coq/coq/pull/18178#issuecomment-1768580471 @Emilio Jesús Gallego Arias

IMHO we should try to make staging more robust by typing, still having to rely on the current system is gonna later or sooner create bugs. I still think that using an existential that passes to the plugin the parsing state to update is worth it.

I mostly agree but not sure what you mean by existential

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:30):

Actually is not very important in the current context, sorry for the noise (it is important in other tho). current libobjects are already existentials.

What I meant is:

What I don't like about the first (current) model is that for the same object we have to indexes, IMHO we could benefit from having a more canonical model, but I still need to solve some questions you asked. The second model is also much more flexible. For example in coq-lsp we aim for an engine that for a particular vernac, can check if it has separate phases or not, and if it has, take advantage of it.

But for the purpose of making the phasing more robust it is not very relevant, sorry for the noise.

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 14:38):

somewhat related I've been thinking of changing the API so you need a handle to read from / write to the summary
so eg instead of Summary.ref : 'a -> 'a ref you would have Summary.ref : 'a -> (read_handle -> 'a) * (write_handle -> 'a -> unit)
I think it can be made to work, except I'm not sure how to deal with the cdebug and cwarning states
The difference between those states and about everything else being that it's accessed in the kernel where I don't think we want to have random functions taking a summary handle. Maybe the kernel should just take the warning/debug state instead of the summary blob? not sure

thoughts?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:42):

That for sure looks like an improvement!

Indeed about CDebug I have been thinking what to do, because the current system doesn't work for my use case (re-execute commands automatically in coq-lsp with debug=on when there is an anomaly)

Best would be for the kernel to take indeed a record with the set of read-only flags. I like that because it also documents what warnings commands may raise.

Debug maybe could be non-summary flag, and the summary in the upper layers handles the option?

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 14:43):

Debug maybe could be non-summary flag, and the summary in the upper layers handles the option?

not sure what you mean

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:43):

I mean that debug options are not stored in the summary.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:44):

"Non-synchronized" as we used to say

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 14:44):

what about "the summary in the upper layers handles the option"?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:44):

I need to think about that indeed.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:44):

It is similar to printing options actually

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:45):

Emilio Jesús Gallego Arias said:

I need to think about that indeed.

I'm struggling with this problem: when I set some debug option, sometimes I want the file to be rechecked, sometimes I don't

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:46):

For example for my use case, summary does the wrong thing:


Last updated: Oct 13 2024 at 01:02 UTC