Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Add ontop option seems to be not supported #202

Closed
rashchedrin opened this issue May 22, 2020 · 3 comments · Fixed by #318
Closed

Add ontop option seems to be not supported #202

rashchedrin opened this issue May 22, 2020 · 3 comments · Fixed by #318
Assignees
@ejgallego
Labels
fixed by: flèche kind: documentation kind: upstream
Milestone
next-gen

Comments

@rashchedrin
Copy link

I want to work with different proof branches. It seems that option ontop of Add command is designed specifically for this use case, however, when I try to use it it says that "Stm.add called for a different state (4) than the tip: 5. This is not supported yet, sorry.". Here's input to reproduce this message:

(Add () "Variables A B C : Prop.")
(Exec 2)
(Add () "Goal (A -> B -> C) -> (A -> B) -> A -> C.")
(Exec 3)
(Add () "intro H.")
(Exec 4)
(Add () "intros HStateFive HA.")
(Exec 5)
(Exec 4)
(Add ((ontop 4)(newtip 51)) "intros HStateFiftyOne HA.")

Here's the complete output of this sequence:
https://gist.github.com/rashchedrin/3584eaa4316dc670947bf5501a031a7b
(I entered them in command prompt of rlwrap sertop --printer=human)
My version of sertop is 8.11.0+0.11.0 .
The last (Exec 4) command doesn't change anything: I've tried with and without it with the same result. I've also tried it with and without --deep-edits flag (I have no idea what it does), result is the same.
If there is any workaround for this, please tell me, because utilizing branch switching for faster ATP is the main focus of my work right now.
@ejgallego ejgallego self-assigned this May 22, 2020
@ejgallego ejgallego added this to the 0.11.1 milestone May 26, 2020
ejgallego added a commit that referenced this issue Jun 3, 2020
@ejgallego
[sertop] New (Fork (fifo_in file) (fifo_out file)) command
b4a78a4 
The new experimental command `(Fork (fifo_in file) (fifo_out file))`
will (hard) fork a new SerAPI process and redirect the input / output
towards the given Unix FIFOs.

This API is experimental but should allow quite a few advantages to
some users willing to perform speculative execution.

In particular, it should greatly improve the use case in #202 .
@ejgallego ejgallego mentioned this issue Jun 3, 2020
Merged
@ejgallego
Copy link
Owner

Hi @rashchedrin , indeed this is not supported upstream; unless you are on an "Edit" branch, which we don't really support, I think Coq can only have one document, so you if you have a document:

s1 <- s2 <- s3

and you want to do s1 <- s2 <- s4 you need to cancel s3 first, at least with the current setup.

I propose a different solution for you use case, in PR #210 . With that PR, you can actually call (Fork ...) when constructing s2, and then proceed in parallel with two sertop processes.

How well that will work is unknown, but it could indeed work pretty well. Would you mind testing / reviewing that PR? I can merge it if that will make your testing easier.

ejgallego added a commit that referenced this issue Jun 3, 2020
@ejgallego
[sertop] New (Fork (fifo_in file) (fifo_out file)) command
9a0fd3e 
The new experimental command `(Fork (fifo_in file) (fifo_out file))`
will (hard) fork a new SerAPI process and redirect the input / output
towards the given Unix FIFOs.

This API is experimental but should allow quite a few advantages to
some users willing to perform speculative execution.

In particular, it should greatly improve the use case in #202 .
ejgallego added a commit that referenced this issue Jun 3, 2020
@ejgallego
[sertop] New (Fork (fifo_in file) (fifo_out file)) command
b3df867 
The new experimental command `(Fork (fifo_in file) (fifo_out file))`
will (hard) fork a new SerAPI process and redirect the input / output
towards the given Unix FIFOs.

This API is experimental but should allow quite a few advantages to
some users willing to perform speculative execution.

In particular, it should greatly improve the use case in #202 .
@rashchedrin
Copy link
Author

Thank you for implementing this! This might be a game changer for me. I'll take a closer look at it after 2-3 days (I need to finish some of my experiments first).

@ejgallego ejgallego modified the milestones: 0.11.1, 0.12.1 Aug 26, 2020
ejgallego added a commit that referenced this issue Feb 12, 2021
@ejgallego
[sertop] New (Fork (fifo_in file) (fifo_out file)) command
34ab7cb 
The new experimental command `(Fork (fifo_in file) (fifo_out file))`
will (hard) fork a new SerAPI process and redirect the input / output
towards the given Unix FIFOs.

This API is experimental but should allow quite a few advantages to
some users willing to perform speculative execution.

In particular, it should greatly improve the use case in #202 .
@ejgallego
Copy link
Owner

Will release the Fork workaround in 0.12.1, full speculative execution is delayed to the next-gen engine.

@ejgallego ejgallego modified the milestones: 0.12.1, next-gen Feb 12, 2021
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Mar 12, 2021
@ejgallego
[new release] coq-serapi (8.12.0+0.12.1)
4054a1b 
CHANGES:

* [serapi]  (!) Bump public library versioning [breaking change]
 * [opam]    Bump upper bound on ppx_sexp_conv to 0.15, allowing SerAPI
             to work with the 0.14 set of Jane Street packages.
 * [serapi]  Fix goal printing anomaly (ejgallego/coq-serapi#230, fixes ejgallego/coq-serapi#228 @corwin-of-amber)
 * [sertop ] New `(Fork (fifo_in file) (fifo_out file))` command, that
             will (hard) fork a new SerAPI process and redirect the
             input / output towards the given Unix FIFOs. This API is
             experimental but should allow quite a few advantages to
             some users willing to perform speculative execution.
             (ejgallego/coq-serapi#210 , improves ejgallego/coq-serapi#202 , @ejgallego)
 - [serapi]  Fix missing newline to separate goals (ejgallego/coq-serapi#235, fixes ejgallego/coq-serapi#231, @ejgallego)
@ejgallego ejgallego mentioned this issue Mar 12, 2021
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Mar 12, 2021
@ejgallego
[new release] coq-serapi (8.12.0+0.12.1)
15ba4d7 
CHANGES:

 * [serapi]  (!) Bump public library versioning [breaking change]
 * [opam]    Bump upper bound on ppx_sexp_conv to 0.15, allowing SerAPI
             to work with the 0.14 set of Jane Street packages.
 * [serapi]  Fix goal printing anomaly (ejgallego/coq-serapi#230, fixes ejgallego/coq-serapi#228 @corwin-of-amber)
 * [sertop ] New `(Fork (fifo_in file) (fifo_out file))` command, that
             will (hard) fork a new SerAPI process and redirect the
             input / output towards the given Unix FIFOs. This API is
             experimental but should allow quite a few advantages to
             some users willing to perform speculative execution.
             (ejgallego/coq-serapi#210 , improves ejgallego/coq-serapi#202 , @ejgallego)
 - [serapi]  Fix missing newline to separate goals (ejgallego/coq-serapi#235, fixes ejgallego/coq-serapi#231, @ejgallego)
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[meta] Put SerAPI in maintenance mode.
779ce5e 
Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #13
@ejgallego ejgallego mentioned this issue Feb 14, 2023
Merged
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[meta] Put SerAPI in maintenance mode.
7224c22 
Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #13
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[meta] Put SerAPI in maintenance mode.
946211b 
Thanks to everyone that helped and used this project for almost 7
years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ejgallego ejgallego

Labels
fixed by: flèche kind: documentation kind: upstream
Projects
None yet
Milestone
next-gen
Development

Successfully merging a pull request may close this issue.

[meta] Put SerAPI in maintenance mode. ejgallego/coq-serapi
2 participants
@ejgallego @rashchedrin