-
Notifications
You must be signed in to change notification settings - Fork 39
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
State id to Add
the first sentence to
#14
Comments
Hi Clément, I am a bit confused here, are you are talking about sending the whole document to Coq with Add? |
With regards to (STM == Coq) states, State 1 is the root state, State 0 is reserved for the "dummy" state (o_o) SerAPI does indeed add a command if you use |
Oh I think I see what you mean. |
Is cd293d8 what you had in mind? Note that in the async case, you may have several tips where to add stuff to I think. |
Hmm no, that's not exactly what I meant (sorry for the delayed answer). In fact, I'm not sure it's too good to allow this default, since it indirectly exposes to the user the fact that there exists a "current state". Thus I think that ontop should be mandatory :) My suggestion was a bit different. In almost all cases I know which state to attach to: the one that's (textually) the closest before the current edition point. There's just one case where I don't know; namely, when I'm at the very beginning of the document and I haven't sent any sentences yet. I'd just like to have a way to know to which state ID I should attach the first sentence that I send :) Sorry for not making this clear :/ Is it better now? |
Actually, thinking more about it, let me backtrack slightly on this. Keeping What do you think? |
Umm, I didn't understand why I think keeping cd293d8 is OK, you can always use (Some stateid) if you want to be explicit; and None if you want to add at the end of the document. IMHO throwing an exception is overkill. The current "tip" of the Stm is a perfectly well defined notion even in async mode, so I'd say let's just make |
Current state here really means the end of the document, so indeed, you are right that even if internally the Stm needs to keep track of it, it is useless for the document. I see what you mean now and I'm not sure what is the cleanest way... It looks like we need a special case one way or another. |
I think Bottom line: I'm happy with |
Oh that is interesting; I didn't think so much of the async mode yet so excuse me if I look lost there. What would be the case for I'm sure I've been missing something in this issue all the time, maybe a concrete example would help :) |
[edit]: This comment doesn't seem to be true.
I'm much afraid this doesn't hold if I understood the
I think it works this way but I am not 100% sure yet, so please bear with any error. I am not sure either what this implies for the IDE design, certainly a possibility would the to split the document pointer into a "version" field and a |
Hmm. Not sure I understand this in full.
This is the basic logic. When looking for a sentence to attach to, the closest preceeding "known to Coq" one is always the right one, I think. There are multiple possible failures:
The underlying Stm has a notion of current state, but it doesn't seem useful to expose it to the outside world. Add (as specified in this proposal) doesn't need it; Cancel doesn't either. Goals doesn't, as long as its allowed to pass a state id. What do you think? If this more understandable? :) |
Thanks, I think I see what you mean, but honestly I don't understand the STM well enough. I need to think more about this. There is a DAG, an internal VCS, the states (that are kind of chronologically ordered). I guess a possible way to proceed would be to assemble a set of interesting examples, and have a "tracing" mode to see what the STM does. |
I think my previous comment about |
Regarding your comment, I think this is mostly how things are working right now, modulo bugs. Do you see any important deviation? |
Hmm, which one was my first comment? |
I meant this comment: #14 (comment) In fact, I'd consider any deviation from it a bug. |
Cool :) I think I need more testing. I'll push my work somewhere soon if you want a quick peek :) |
Cool thanks! I'd love to see it! I'm not an expert on elisp but I'll be able to survive I think :D Yeah, I think that the protocol you've proposed is something sensible to strive for, let's see what we find with async, etc... and how we can manage to connect to the STM. |
I've pushed it here. Demo @ https://asciinema.org/a/b84ph360841x3c9lwq6pyihm9 |
Amazing!!!! |
wrt to the original question in this issue, see also this comment in #11. |
Note that older versions of SerAPI had a bug and didn't forward to the client the initial feedback. Indeed, when SerAPI starts the STM will emit a feedback message providing the location of the root state: (Feedback ((id (State 1)) (contents (ProcessingIn master)) (route 0)))
(Feedback ((id (State 1)) (contents Processed) (route 0))) |
Hi, so I'm thinking of closing this issue soon. My plan of action is:
What do you think? Cheers, |
Command line options shouldn't affect the initial state, we guarantee it to be 1 after STM initialization. Thus, we make the prelude option to atomically load the prelude before the STM init. If the user wants to have more control over it, it can just add the desired `Require Import` manually. Refs #14, but we need to close: - Import the `Cancel 1` handling from jsCoq. - Provide a `--no-init` option plus an Init control command.
Almost done, will close when the docs are ready. |
Command line options shouldn't affect the initial state, we guarantee it to be 1 after STM initialization. Thus, we make the prelude option to atomically load the prelude before the STM init. If the user wants to have more control over it, it can just add the desired `Require Import` manually. Refs ejgallego#14, but we need to close: - Import the `Cancel 1` handling from jsCoq. - Provide a `--no-init` option plus an Init control command.
A further update on this issue, Coq upstream has gained a new API point |
TL;DR: can we get a special ID for the root state? Currently I need to attach to state 2 when sending the first sentence (I guess this is because SerAPI sends two commands before giving me control?)
Background: When I need to
Add
a new sentence, I need to know the ID of the immediately preceding sentence. With the XML protocol I do anEditAt(stateid)
and then I add to that same statestteid
. With SerAPI, IIUC, I'll just do anAdd
(there won't be a stateful notion of "current tip", yay!). ((Of course I'll get an error if that state wasn't a leaf of the DAG.))Now the question is: how do I figure out which ID to
Add
to? It's pretty easy to just look at the previous sentence if there is one, but for the very first sentence? I can currently get it using a synchronous(Control StmState)
query, but hopefully this very notion of "current state" will go away at some point (right? I hope I'm not missing anything here).The text was updated successfully, but these errors were encountered: