Comments (26)
I've pushed it here. Demo @ https://asciinema.org/a/b84ph360841x3c9lwq6pyihm9
from coq-serapi.
Hi Clément, I am a bit confused here, are you are talking about sending the whole document to Coq with Add?
from coq-serapi.
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 --prelude
: Require Import Coq.Init.Prelude.
We could import prelude in a different way without using the Stm, but I much prefer to make prelude loading explicit. Some users like the HoTT folks don't want indeed to load Coq's Prelude.
from coq-serapi.
Oh I think I see what you mean.
from coq-serapi.
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.
Thus I made the ontop
an option type for now instead of getting rid of it.
from coq-serapi.
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?
from coq-serapi.
Actually, thinking more about it, let me backtrack slightly on this. Keeping cd293d8
, we could just make None
throw an exception if there's more than one tip. This way it can be used for the first sentence, and there's no risk of getting into a confusing state in async mode if there are multiple tips.
What do you think?
from coq-serapi.
Umm, I didn't understand why (StmState)
didn't work for you? The initial State is always 1 but Coq doesn't guarantee you can rely on that, you need to use the number coming from Stm.get_current_state
.
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 None
= current tip.
from coq-serapi.
"this very notion of "current state" will go away at some point (right? "
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.
from coq-serapi.
I think None
works very nicely when there are no branches (i.e. a single tip). In async mode with multiple tips, it probably doesn't hurt to have None mean the current tip; but it any case, I think in the long run we can simplify the protocol by not exposing the notion of current state; instead, we can translate any Add
into an EditAt
followed by an Add
(and we can make Add
fail if it's not adding to an actual tip).
Bottom line: I'm happy with cd293d8
:)
from coq-serapi.
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 Add
behaving like EditAt
? Presumably, you first cancel, then allow the user to edit, then Add
. Where would the new input for such an Add
come from?
I'm sure I've been missing something in this issue all the time, maybe a concrete example would help :)
from coq-serapi.
[edit]: This comment doesn't seem to be true.
Note something very important indeed:
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
I'm much afraid this doesn't hold if I understood the Stm
correctly. Imagine:
- You add 10 independent proofs, you observe all of them, 9 check OK, 1 proof fails. The current tip is in the last added sentence, let's say
id = 100
. - You then want to do an
edit_at
at the proper place, let's say35
. This will return afocus = { start = 30; stop = 40; tip = 101}
!! You invalidate the35-40
range. But note the new tip! You add on top of101
until you get anUnfocus 105
fromAdd
. - You want to add at the end of the document. Now, you cannot look at the previous sentence, given the way document versioning works, looking at previous sentence doesn't work anymore.
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 stint
field, but I guess we need to think a bit more.
from coq-serapi.
Hmm. Not sure I understand this in full.
What I could see working well here is changing the semantics of Add in the following way:
- From the IDE perspective, there is no "current tip". There's just a collection of sentences, some that Coq knows about and some that it doesn't.
- The ones that Coq knows about have a state id (except during a small time window after they are are Added, until the response for the Adds comes). The ones that Coq doesn't know about are free form text.
- The way to let Coq know about a sentence is to connect it to a previously known sentence. This is done using Add, passing the state to which the new sentence connects. If there are no previous states, passing None instead of a state ID is fine. (More generally, if there is only one possible addition point, then passing None instead of a state ID is fine. This is useful for the document's very first sentence).
- The way to tell Coq to forget about a sentence is to use
Cancel
on that sentence. - When Coq forgets about a sentence, it may need to forget about others. These are all the ones that don't have a parent anymore. Typically all the ones inside of a Proof-Qed block, but it could be all of the document as well. In the future, it could be more fine grained.
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:
- Add can fail if the sentence that we're trying to attach to is unknown to Coq. This could happen if Coq has issued a Canceled message for that sentence and the IDE hasn't processed it yet. In that case, we mark the sentence that we tried to add as unknown to Coq. The IDE must handle this failure, as it is expected to happen, albeit rarely.
- Add can also fail if we try to add a sentence to a state id that already has children. This would be a logic error in the IDE; it is not an expected failure case.
- Cancel can fail if the state is already unknown to Coq. In that case, Coq can just ignore the stale Cancel message. This doesn't return an error to the IDE; the IDE can expect the cancellation to have succeeded.
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? :)
from coq-serapi.
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.
from coq-serapi.
I think my previous comment about Unfocus
was wrong, however I cannot really test what I want as CoqIDE crashes...
from coq-serapi.
Regarding your comment, I think this is mostly how things are working right now, modulo bugs. Do you see any important deviation?
from coq-serapi.
Hmm, which one was my first comment?
from coq-serapi.
I meant this comment: #14 (comment)
In fact, I'd consider any deviation from it a bug.
from coq-serapi.
Cool :) I think I need more testing. I'll push my work somewhere soon if you want a quick peek :)
But if you agree with that comment, then awesome! This sounds like a simple and sweet protocol.
from coq-serapi.
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.
from coq-serapi.
Amazing!!!!
from coq-serapi.
wrt to the original question in this issue, see also this comment in #11.
from coq-serapi.
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)))
from coq-serapi.
Hi, so I'm thinking of closing this issue soon. My plan of action is:
1
is guaranteed to be the initial state.- A cancel on
1
has no effect. - We usually may need to perform some pre-STM initialization like setting load paths, loading the prelude, options, etc... before creating the initial state (and thus are not reversible). There are two possibilities:
- Add a new
Init
control call to the protocol. Clients will then do(Control (Init (opts)))
and can start sending commads. (No need to wait for the(Feedback ((id (State 1)) (contents Processed) (route 0)))
event.)
- Add a new
- Another option would be to handle "init" by command line arguments, thus clients can assume that SerAPI always starts initialized. This may be indeed simpler.
What do you think?
Cheers,
E.
from coq-serapi.
Almost done, will close when the docs are ready.
from coq-serapi.
A further update on this issue, Coq upstream has gained a new API point new_doc
, thus the root of the document will be chosen by the client in the document creation call.
from coq-serapi.
Related Issues (20)
- How to handle "Needs option -impredicative-set." HOT 3
- installation HOT 4
- what version of coq serapi works with coq 8.10.2? HOT 9
- what is the best version of coq-serapi that works with coq 8.12? HOT 5
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 12
- Segfault on (Query () Goals) with sertop 8.15.0+0.15.3 HOT 4
- What is the purpose of coq-serapi's existance and why can't everything be done in coqtop? HOT 5
- Expose Section Variable Determining API in SerAPI HOT 6
- Incorrect goals when providing -topfile in sertop 8.10.0+0.7.2 HOT 2
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 HOT 1
- Missing conversion functions for types for the extraction plugin? HOT 3
- Can't run `make test` due to an error related to `eqType` HOT 4
- Windows PATH length (again) HOT 21
- macOS: serapi loads Coq .vo from compile time path HOT 5
- Run tests with MC 2 HOT 3
- Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01 HOT 5
- Segmentation fault in coq/getDocument call HOT 4
- New versioning scheme. HOT 1
- License issue HOT 1
- CoqSerapi Usage Question HOT 6
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-serapi.