Alex Sanchez-Stern (Jan 19 2023 at 21:03): Alex Sanchez-Stern (Jan 19 2023 at 21:03):Hey all,
I have a question about plans for future development of Coq/Serapi (hope this is the right stream for that). In coq-serapi currently, states are numbered. When you add a statement, you have to specify what state you're adding it on top of, and it gives you a state number. But currently, it seems like you can only add statements to the "active" state returned by the last interaction. This seems like an incomplete design; if there's only one valid state number to pass to (Add () "..."), then it doesn't make sense to have the user specify it instead of it being inferred. But if there are plans to in the future allow users to "jump" to previously visited states and add statements on top of them, then it makes sense to have the state numbers in the API now. Are there plans to allow that kind of jumping? If so, is there some sort of website or statement somewhere that outlines those plans, or is it more of a "cite the zulip" kind of thing?
Thanks,
Alex Sanchez-Stern
Enrico Tassi (Jan 19 2023 at 21:14):There are no plans to improve the STM (the APIs serapi exposes), we are rather hoping to deprecate it soonish. So it won't get any improvements, but won't disappear either.
I don't know which are the plans of serapi, maybe you should ask it in its dedicated stream.
Last updated: Oct 04 2023 at 20:01 UTC