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
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.
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?
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?
Debug maybe could be non-summary flag, and the summary in the upper layers handles the option?
not sure what you mean
I mean that debug options are not stored in the summary.
"Non-synchronized" as we used to say
what about "the summary in the upper layers handles the option"?
I need to think about that indeed.
It is similar to printing options actually
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
For example for my use case, summary does the wrong thing:
foo
.Last updated: Oct 13 2024 at 01:02 UTC