Eli Dupree (Feb 04 2021 at 17:19): Eli Dupree (Feb 04 2021 at 17:19):I posted about this idea on IRC, and someone said I should come here to get input from Coq devs about it.
I've been using coqide for a while, and I love the interactivity of "step back and forth" and proof state display. But I can envision something I would like much better. I have a rough plan to make a GUI that automatically attempts lots of different tactics and displays relevant parts of the output, so as soon as you write the . at the end of a Lemma, you don't have to click "Forward one command", it has already gone forward and is now suggesting a bunch of tactics. Things like: mouse over a hypothesis H and it shows you a whole panel of "destruct H will get you this, injection H will get you that, etc".
Ultimately this might want to be an editor extension where you can click on the suggestions to immediately insert them into your code. But for practical reasons, I'm thinking I'll start with something simpler so I can get started on experimenting with possible designs. I personally use a system that alsosaves my code whenever I edit it, so I'm thinking I'll make a file watcher that notices changes and sends the changes to coqtop using the XML protocol, then displays whatever I want in a GUI.
Eli Dupree (Feb 04 2021 at 17:29):My top barrier to "just throwing something together" is the fact that I don't understand how to use the XML protocol yet. I've read through https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md , but I don't know how to actually use the protocol (Pasting the XML examples into coqtop doesn't do anything; someone in a Reddit thread said that you need to pass the commandline argument -xml, but that argument doesn't exist)
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:37):Unfortunately the base implementation of Coq will work not very well for your use case regardless of the protocol to use.
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:39):I'd suggest you try raw access to the document manager using for example SerAPI, which will be much more immediate than the XML protocol, and provide quite more flexibility in some regards, but even after you do that, you will quickly find many limitations in the underlying document layer (called STM) as for example as to what you can do regarding document versioning etc...
Eli Dupree (Feb 04 2021 at 17:40):I'm not sure why you say that? It seems to me like everything I'm imagining can be done using just stepping forward and backwards, so there don't have to be multiple internal states or even a DAG
Eli Dupree (Feb 04 2021 at 17:40):It might be a little less efficient but I don't have to care about that at this early stage
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:42):Of course if snappiness / efficiency is not a concern you could do like that, but that's IMHO an important point
Eli Dupree (Feb 04 2021 at 17:43):It is definitely a concern – for example rebuilding the whole file for each tactic attempted would be far too slow. But for example, if you have a current proof state and want to try the 1000 different tactics from there, all you have to do is try each one and then revert it
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:45):Yes you can do that, but current API won't allow you to try in paralell for example. Also interruption may be tricky
Eli Dupree (Feb 04 2021 at 17:45):Even if I wanted to the UI to let you switch back and forth between different parts of a tree of possible tactics, I would only have to keep a tree of tactic commands internally in my own tool, and use linear rollback to switch between them in coqtop. The difference in speed between that and "actually store both states" is trivial if the tactics themselves don't take a long time to run, which is true for many tactics
Eli Dupree (Feb 04 2021 at 17:46):what's tricky about interruption?
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:46):OCaml doesn't provide the best interface to handle signals / etc...
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:47):Anyways, after the warning about the state of Coq itself in this regard, it is a very cool project to try
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:48):You may want to look into peacoq, alectryon, also quite a few of machine-learning people have built interfaces with python thru serapi
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:48):but serapi should be pretty easy to use [or the OCaml API]
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:49):jscoq is another interesting option
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:49):protocol in all cases is pretty simple, SerAPI will get you running just by doing (Add () "Sentence(s)")
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:49):you may want to pass some options, then you have Exec and Cancel
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:50):and that basically is
Eli Dupree (Feb 04 2021 at 17:50):yeah serapi looked at first glance like it might be suitable, although I'll need to spend some time to undersatnd it
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:51):@Eli Dupree let me know of any question you may have, but it is quite similar to the xml protocol, just using a more straighfoward encoding, and a more regular syntax
Emilio Jesús Gallego Arias (Feb 04 2021 at 17:51):definitively much easier to get an example running
Eli Dupree (Feb 04 2021 at 17:51):cool
Eli Dupree (Feb 04 2021 at 17:54):is there complete documentation of the SerAPI commands anywhere? the github readme is pretty vague about them
Gaëtan Gilbert (Feb 04 2021 at 18:02):Eli Dupree said:
My top barrier to "just throwing something together" is the fact that I don't understand how to use the XML protocol yet. I've read through https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md , but I don't know how to actually use the protocol (Pasting the XML examples into coqtop doesn't do anything; someone in a Reddit thread said that you need to pass the commandline argument
-xml, but that argument doesn't exist)
xml protocol is used by coqidetop I think
Théo Zimmermann (Feb 04 2021 at 18:38):It's also used by the vim editor support coqtail (https://github.com/whonore/Coqtail).
Gaëtan Gilbert (Feb 04 2021 at 18:41):through coqidetop
Daniel Garcia (Feb 04 2021 at 18:43):Théo Zimmermann said:
It's also used by the vim editor support coqtail (https://github.com/whonore/Coqtail).
Question about that plugin, as I haven't heard of it before. How does it compare to the vim plugins Coquile <https://github.com/the-lambda-church/coquille> or coq-au-vim <https://framagit.org/manu/coq-au-vim> ? I am looking for a plugin for vim >=8 myself, and was using coq-au-vim but I couldn't get it running on a new machine easily.
Théo Zimmermann (Feb 04 2021 at 18:44):It's a fork of the venerable coquille.
Théo Zimmermann (Feb 04 2021 at 18:44):And it has been actively maintained for years.
Théo Zimmermann (Feb 04 2021 at 18:45):So this is definitely the one to use.
Daniel Garcia (Feb 04 2021 at 18:45):Gotcha, thanks. They're stating their support is for Coq 8.4 - 8.13, is Coq or coqtop going to break compatibility for future releases?
Théo Zimmermann (Feb 04 2021 at 18:48):8.13 is the latest release. They do not make claims on future releases. There can be small changes to adapt to, but most releases are very smooth to update to, the XML protocol has been very stable. If you use SerAPI, then you are also provided a very stable protocol (even though SerAPI itself requires some changes to be adapted to new versions of Coq).
Daniel Garcia (Feb 04 2021 at 18:49):Gotcha. Also now, I get the joke of the name: screenshot_2021_02_04_12_48.png
Emilio Jesús Gallego Arias (Feb 04 2021 at 18:54):Eli Dupree said:
is there complete documentation of the SerAPI commands anywhere? the github readme is pretty vague about them
Documentation is far from good, http://ejgallego.github.io/coq-serapi/coq-serapi/Serapi_protocol/index.html contributions are welcome
Emilio Jesús Gallego Arias (Feb 04 2021 at 18:55):Note that SerAPI is more of a playground, than something meant to be stable, at some point it will likely change, however protocol is simple enough we could keep compat for a long time.
Eli Dupree (Feb 04 2021 at 22:32):that's alright, my project isn't expected to be stable soon either :stuck_out_tongue: I'm firmly in "throwing something together to get my ideas in order" territory right now.
So I'm starting to write some Rust code that parses SerAPI feeback, but the rust S-expressions library I'm using has a bug and failed to parse them :joy: I see the front page of SerAPI says it can use JSON rather than S-expressions, but I can't figure out how to tell it to do that (Is JSON actually supported yet? I see this says "Support for JSON is currently under development.")
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:36):@Eli Dupree unfortunately JSON is not availabe at a protocol driver yet, see the corresponding issue :S
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:37):https://github.com/ejgallego/coq-serapi/issues
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:37):Did you manage to do some basic tests by hand?
Eli Dupree (Feb 04 2021 at 22:37):Alas. Anyway, I've hacked it with line.replace("(", " (") and I'm making progress again lol
Eli Dupree (Feb 04 2021 at 22:37):yeah
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:37):Like adding some sentences, executing them, printing the goals, cancelling and adding a new one?
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:37):If you know how to do that then you know 99% of the protocol
Emilio Jesús Gallego Arias (Feb 04 2021 at 22:38):Maybe that'd make for a good tutorial:
(Add () "Sentences") where () is the set of options, this is usually important and you want to use ((newtip 2) (ontop 1)) for example, where the numbers are the sentence id(Exec 2) for example(Query ((sid 2)) Goals)(Cancel 2) Eli Dupree (Feb 05 2021 at 00:26):3 hours and 3 bug reports later, I still haven't managed to parse a single Feedback, this time because SerAPI represents struct fields as (name value) while serde_lexpr insists on representing them as (name . value) :sob:
Emilio Jesús Gallego Arias (Feb 05 2021 at 14:35):Yeah it seems sexp is not so well supported :S I will try to finish the json protocol branch, tho you could try to do some very simple sexp parsing yourself
Emilio Jesús Gallego Arias (Feb 05 2021 at 14:35):or wrap sertop in a small python sexp -> json converter which I understand can be written very easily
Eli Dupree (Feb 05 2021 at 16:02):Hmm... I'm not sure writing a python wrapper would be that easy. Converting from sexp to json would probably be straightforward, but for the other direction, it might be complicated to get Rust's serde_json to emit json enum representations that will convert into the same sum-type representations used by SerAPI sexps...
Eli Dupree (Feb 05 2021 at 17:14):Meanwhile, I've forked serde_lexpr and successfully hacked it to parse the initial messages from sertop :smiley:
Eli Dupree (Feb 05 2021 at 19:28):@Emilio Jesús Gallego Arias Where should I look to find the definitions of the other types used in the SerAPI protocol, like Pp.t? I've started making some Rust types corresponding to the OCaml types of the protocol, but I'm not familiar with OCaml / where to look for other types OCaml imported
Gaëtan Gilbert (Feb 05 2021 at 19:35):you can look around here https://coq.github.io/doc/master/api/coq/Pp/index.html although it seems we messed up the doc comment formatting x_x
or use https://github.com/coq/coq/find/master to find the right file (pp.mli)
or ask here
Emilio Jesús Gallego Arias (Feb 05 2021 at 19:41):@Eli Dupree some types such as Pp.t are not meant to be inspected in full if you don't want, for example, given an object that serializes a Pp.t, you can use (Print ((pp_format PpStr)) obj) to obtain a string representation.
If you want to manipulate it directly, indeed you need to refer to the datatype's definition; now that you say it, it would be a good idea to build SerAPI's documentation in a way that links to Coq's documentation.
Emilio Jesús Gallego Arias (Feb 05 2021 at 19:41):There is an unfinished project to actually do this process automatically using meta-programming.
Emilio Jesús Gallego Arias (Feb 05 2021 at 19:42):That'd be the ideal situation; note by the way that @Shachar Itzhaky wrote a rendered Pp.t -> HTML which is available in jsCoq's repository, but it is done in javascript
Emilio Jesús Gallego Arias (Feb 05 2021 at 19:42):The print approach generalizes to other datatypes, such as Coq's AST, etc...
Emilio Jesús Gallego Arias (Feb 05 2021 at 19:43):https://github.com/jscoq/jscoq/blob/v8.12/ui-js/format-pprint.js
Eli Dupree (Feb 05 2021 at 19:43):It's fairly likely that I'll want to render this stuff as HTML, so that may be relevant, thanks!
Shachar Itzhaky (Feb 05 2021 at 19:51):Great, I'm happy to refine the rendering guided by scenarios that you might encounter; I did not have a large sample of Pp.t instances to try this on when I wrote this pretty-printer.
Shachar Itzhaky (Feb 05 2021 at 19:52):@Clément Pit-Claudel how is Alectryon generating HTML for displaying goals?
Clément Pit-Claudel (Feb 05 2021 at 19:54):Shachar Itzhaky said:
Clément Pit-Claudel how is Alectryon generating HTML for displaying goals?
Check out the implementation at https://github.com/cpitclaudel/alectryon/blob/eef43826b3b8c13704c049933dab91a883c62cd1/alectryon/html.py#L195
Shachar Itzhaky (Feb 05 2021 at 19:55):Neat! :octopus:
Clément Pit-Claudel (Feb 05 2021 at 19:55):A fragment is either Text or a RichSentence; the latter has outputs which are either Messages or Goals
Shachar Itzhaky (Feb 05 2021 at 20:00):Do you get hyp.type, hyp.body, and goal.conclusion with (Print ((pp_format PpStr)) obj) like Emilio said?
Clément Pit-Claudel (Feb 05 2021 at 20:11):Shachar Itzhaky said:
Do you get
hyp.type,hyp.body, andgoal.conclusionwith(Print ((pp_format PpStr)) obj)like Emilio said?
Eli Dupree (Feb 05 2021 at 22:48):So, I'm not quite sure how to read the pp.mli code. I can tell we've got an opaque type t, and I guess the things below it must define the possible ways of constructing a t? But one of the S-expressions I'm seeing for a Pp.t is (Pp_glue((... and I don't see Pp_glue defined anywhere
Shachar Itzhaky (Feb 06 2021 at 13:18):You can access the internal representation of Pp.t using Pp.repr : Pp.t -> Pp.doc_view. It is a data type with Ppcmd_* constructors, one of which is Ppcmd_glue. For some reason SerAPI is translating the Ppcmd_* to Pp_* (https://github.com/ejgallego/coq-serapi/blob/2d53744fa2ba4005644e19444216824700d691da/serlib/ser_pp.ml#L41).
As for the semantics, I only know that they are somewhat based on OCaml's Format boxes (https://ocaml.org/releases/4.08/htmlman/libref/Format.html), and I think "glue" is just a means to represent a sequence of boxes.
(see Pp.string_of_ppcmds https://github.com/coq/coq/blob/16765871394a81975047b37f15a902fcc112dc40/lib/pp.ml#L211 and pp_with https://github.com/coq/coq/blob/16765871394a81975047b37f15a902fcc112dc40/lib/pp.ml#L182.)
Eli Dupree (Feb 06 2021 at 14:22):thanks!!
Eli Dupree (Feb 07 2021 at 01:20):omfg SerAPI is emitting the sexpr (Pp_string .), intending to mean the string ".", and serde_lexpr is interpreting that as a cons with missing cdr :joy:
Eli Dupree (Feb 08 2021 at 00:46):@Emilio Jesús Gallego Arias Question about this line from the SerAPI docs:
In particular, [Cancel] will force execution up to the previous sentence; thus it is not possible to parse a list of sentences and then replace them without incurring in the cost of executing them.
Cancel takes a list of state ids, so what is "the previous sentence"? I would hope that if I Add 100 sentences and then Cancel sentences 10-100, it would only need to execute up to sentence 9, but that sentence seems like it might be implying that it would have to execute up to sentence 99. Which is correct?
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:10):Pp_ vs Ppcmd_: indeed that's an unfortunate mismatch, and the renaming was a mistake in retrospective; we could fix it but I'm not sure it is worth the compatibility breakage:. as a string: this is the choice made by the printer we are using, it would be good to improve it, there is an issue open about it alreadyCancel: unfortunately cancel will indeed execute up to the previous command, that's a bug in Coq's document manager itself and unfortunately not trivial to fix so it seems, hopefully newer versions of Coq can get around that limitation. Eli Dupree (Feb 08 2021 at 14:30):So you're saying that it will execute up to command 99 in my example?
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:35):Unfortunately yes :( unless I'm missing something; this is out of SerAPI control's as of today
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:36):It is a bug in Coq but the code involved (in a component called STM) is beyond my understanding
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:36):We could try our luck submitting a bug report in Coq but I think people is just busy rewriting that component.
Eli Dupree (Feb 08 2021 at 14:43):(I suppose I could work around this by only Adding small chunks at a time, extending them until they get parsed into commands. But right now the performance cost of that case isn't my top concern yet.)
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:56):Actually I'm sorry, in your example only sentence 9 would be executed, current code should handle that OK.
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:57):Tho it is a bit hard to predict sometimes, when SerAPI calls Coq, sometimes Coq will decide to execute things depending on a few factors, for example whether the mode is interactive
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:58):re-execution can happen for several reasons, like the parser needs update, or because the state for a particular document point was not cached due to optimization of memroy
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:58):so the current semantics for cancel kind of work as Cancel is supposed to be used when an editing region is invalidated
Emilio Jesús Gallego Arias (Feb 08 2021 at 14:59):so usually you could assume the user is at the right point, but even so, not ideal for many other cases
Emilio Jesús Gallego Arias (Feb 08 2021 at 15:02):you gotta be careful tho as in (Cancel (st1 st2)) , st1 will be cancelled first, so if it newer than st2, st2 may end up being exectued
Eli Dupree (Feb 08 2021 at 15:21):knowing that the order is important is relevant
Eli Dupree (Feb 08 2021 at 15:22):[tweaks some code]
Emilio Jesús Gallego Arias (Feb 08 2021 at 15:31):Also note that if you cancel a sentence, all the depending ones will be also cancelled (and returned in the list), however being explicit saves you from some work if you want [namely having to wait for the Cancelled answer)
Emilio Jesús Gallego Arias (Feb 08 2021 at 15:32):But this code is a bit tricky due to the mismatch between the serapi model and Coq's model of document [Coq itself doesn't have Cancel]
Eli Dupree (Feb 08 2021 at 15:36):I dream of the day when there will be a perfect language where the global state is a persistent data structure so you can just try all branches with zero backtracking cost :stuck_out_tongue:
Emilio Jesús Gallego Arias (Feb 08 2021 at 20:24):@Eli Dupree what do you have in mind concretely ? :) Are you talking about speculative execution?
Eli Dupree (Feb 08 2021 at 20:32):I mean, for my proof exploration, it would be optimal if I didn't even have to think about "reverting" to previous proof states, but could just try any tactic from any previously visited proof state. Which I think is something like what the API is doing by having state ids? But it's much less straightforward than I would hope for
Emilio Jesús Gallego Arias (Feb 08 2021 at 20:48):@Eli Dupree I totally agree, I have been working on this capability in a new document manager for a while; I call it "speculative execution" but indeed it is just a different model than the one implemented today.
Emilio Jesús Gallego Arias (Feb 08 2021 at 20:49):If your proof exploration is kinda "heavy" , you could try the PR proposed here: https://github.com/ejgallego/coq-serapi/pull/210
Eli Dupree (Feb 08 2021 at 22:05):As of right now, I'm not actually struggling with performance at all (the goal of this project isn't proof search, it's more like "try a moderately large number of tactics with mostly trivial costs so the programmer can see the output more conveniently")
Eli Dupree (Feb 08 2021 at 22:07):Hmm... the PpStr representation of a proof state with multiple goals isn't great (the first hypothesis of the second goal is displayed on the same line as the conclusion of the first goal)
Eli Dupree (Feb 08 2021 at 22:09):Sorry to mostly be posting complaints! I'm making good progress on my project and SerAPI has definitely been helpful compared to whatever other API I would be fighting with right now :sweat_smile:
Wolf Honore (Feb 08 2021 at 22:41):@Eli Dupree Is your code available anywhere yet? I'd like to track this project since I think it's a great idea. I've briefly thought about doing something like it in Coqtail, but I wasn't brave enough to get very far with actually trying it. If you figure out the hard parts I'd love to steal port it
Eli Dupree (Feb 08 2021 at 22:43):Yup! It's right here on github. Not exactly useful yet of course :stuck_out_tongue:
Wolf Honore (Feb 08 2021 at 22:44):Thanks
Emilio Jesús Gallego Arias (Feb 08 2021 at 22:49):Cool to see the source code!
If the PpStr output is bad please file a bug report with an example so we can fix it.
Emilio Jesús Gallego Arias (Feb 08 2021 at 22:51):Actually your use case for "speculative execution" could be even better supported in SerAPI
Emilio Jesús Gallego Arias (Feb 08 2021 at 22:52):We could have SerAPI emulate multiple documents, this is going to be much easier to do in OCaml than from the client side; main drawback, we likely have to patch Coq
Emilio Jesús Gallego Arias (Feb 08 2021 at 22:52):so you will have it "officialy" in Coq 8.14
Emilio Jesús Gallego Arias (Feb 08 2021 at 22:52):as I don't expect any trouble with the patch
Eli Dupree (Feb 08 2021 at 23:36):ooh interesting, the behavior depends on pp_margin... I'll report it now
Emilio Jesús Gallego Arias (Feb 08 2021 at 23:38):The parameters are those of OCaml's format module, unfortunately these are not very easy to understand :/
Eli Dupree (Feb 08 2021 at 23:42):submitted! https://github.com/ejgallego/coq-serapi/issues/231
Emilio Jesús Gallego Arias (Feb 08 2021 at 23:49):Thanks @Eli Dupree , does indeed seem like a bug
Eli Dupree (Feb 08 2021 at 23:53):(I was running it with pp_margin = 999999 to make diffing them simpler, since I haven't gotten around to handling full Pp stuff yet)
Emilio Jesús Gallego Arias (Feb 08 2021 at 23:54):Think of Pp as Coq's own version of HTML
Emilio Jesús Gallego Arias (Feb 08 2021 at 23:54):almost the same age actually :)
Emilio Jesús Gallego Arias (Feb 08 2021 at 23:54):eventually Coq's will replace Pp for the printing stuff for something that should be a subset of HTML
Eli Dupree (Feb 08 2021 at 23:54):almost the same age actually :smile:
:joy:
Eli Dupree (Feb 09 2021 at 00:25):So I'm looking at format-pprint.js right now, and it looks like goals2DOM already has an array of goals that are nicely divided into hypotheses, each containing a Pp.t - as if it was a Pp.t Serapi_goals.reified_goal Serapi_goals.ser_goals. That's what I want, but I don't see a way to get such a thing from the API – there's only PpSer, which gets you that structure but with Constr/Constrexpr instead of Pp.t, and PpCoq, which gets you a Pp.t that's not divided into goals
Emilio Jesús Gallego Arias (Feb 09 2021 at 00:59):You can indeed get the goals in PpSer format, then print each constr individually
Emilio Jesús Gallego Arias (Feb 09 2021 at 00:59):that's a bit the philosophy of the API
Emilio Jesús Gallego Arias (Feb 09 2021 at 00:59):handle stuff gradually
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:00):so you can just access the structure of the goals
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:00):and at each node, for example a constr
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:00):you delegate printing [as you may not want to do it]
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:00):Tho, writing a native printer for Coq would be _very_ interesting
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:00):but that's a whole new project
Eli Dupree (Feb 09 2021 at 01:06):oh, using the Print command on the Constr or Constrexpr?
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:48):Yup!
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:48):You can use it on both; just pass the correct object tag
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:48):Constr are turned into Constrexpr before printing
Emilio Jesús Gallego Arias (Feb 09 2021 at 01:48):this process is called, first, detyping, second, externalization
Eli Dupree (Feb 10 2021 at 02:09):Been hard at work on this! Here's a screenshot of the current state. The screen is kind of a mess of tactics right now, but I've got plans for how to start organizing them...
Eli Dupree (Feb 10 2021 at 02:11):You can click on any of the tactics to move to the state after running that tactic, and you can click on earlier tactics in the list of the top (which, in that screenshot, only has intuition idtac. in it) to move back to earlier states
Eli Dupree (Feb 10 2021 at 02:12):Current plan is to make a column of the current hypotheses on the left, and you can click on a hypothesis to display tactics that act on that particular hypothesis
Eli Dupree (Feb 10 2021 at 02:18):Any project like this has to reckon with the fact that any proof state has loads of useless tactics, and thus the program needs to decide on priorities for which tactics get screen space. Which, in some sense, is the same problem as automated proof search! In both cases you have to guess which tactics are useful to explore. But there are also differences, of course.
Emilio Jesús Gallego Arias (Feb 10 2021 at 16:14):Pretty cool!
Shachar Itzhaky (Feb 11 2021 at 19:57):Oh wow that looks so nice! I like the diff view!! :glowing_star: :glowing_star:
Eli Dupree (Feb 15 2021 at 22:57):More progress! proof_explorer_2.png
Eli Dupree (Feb 15 2021 at 22:59):There's still loads of stuff I should add to it, but it's in a somewhat complete state for the basic idea of what it's supposed to be
Eli Dupree (Feb 15 2021 at 23:00):So I'm officially interested in people trying it out if they're daring enough to try such an early-stage project!
Eli Dupree (Feb 15 2021 at 23:02):Again, it's here on GitHub; to run it, you need Rust, Sass, and SerAPI
Emilio Jesús Gallego Arias (Feb 15 2021 at 23:36):Wow so cool! There is some page where you can advertise it more widely, also once it is more mature both discourse and in coq-club are good places.
How's SerAPI working out for you? I plan to have a look at your tool and hopefully try to improve some things, but don't hesitate to ask for improvements.
Emilio Jesús Gallego Arias (Feb 15 2021 at 23:38):By the way I'd be very happy to make your SerAPI crate part of the official serapi distribution [including a test suite] if you think that'd help
Eli Dupree (Feb 16 2021 at 00:02):SerAPI's working pretty well for what I'm doing with it. I've now got my thing automatically fetching the new goals state, printing all the hypotheses/conclusion, and running Show Proof to get an estimate of the size of the generated proof (incidentally, is the SerAPI Proof query supposed to do something like this? I don't understand what it does/maybe it's incomplete?)
Eli Dupree (Feb 16 2021 at 00:02):I keep running into more gotchas with the S-expression parsing, though, so I'd definitely appreciate it if you got the JSON support working!
Eli Dupree (Feb 16 2021 at 00:03):I'd be very happy to make your SerAPI crate part of the official serapi distribution [including a test suite] if you think that'd help
Like taking my serapi_protocol.rs and making it into a separate crate to help support Rust tools using SerAPI? That sounds like a good idea!
Eli Dupree (Feb 16 2021 at 00:06):Right now my code for that isn't complete (not all the types are fully written down as Rust types) and also as a full-fledged crate it'd probably want to also include the de/serialization part, which... in my current version, doesn't even parse all the sexprs correctly even after I forked serde_lexpr and made a bunch of hacky changes
Eli Dupree (Feb 16 2021 at 00:08):(The most recent issue is that Show Proof. on a slightly-complex proof produces a Pp with more than 128 layers of nested lists, and serde_lexpr is hardcoded to be unable to parse more than 128 recursion levels, because it's implemented using recursive functions that will overflow the call stack, so I'd basically have to refactor the entire sexpr parsing if I wanted to make it work...)
Eli Dupree (Feb 16 2021 at 00:17):Right now my "...but these tactics make larger proofs" is based on the rather silly metric of "length of the string representing the proof", and it would be nice to be more principled, but I couldn't find a way to fetch the proof in a more fundamental form using SerAPI.
Eli Dupree (Feb 16 2021 at 00:25):Anyway, I'm looking forward to what you'll say once you've had a look at my tool!
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:40):incidentally, is the SerAPI Proof query supposed to do something like this? I don't understand what it does/maybe it's incomplete
Good point, actually is sending the current proof / goal, but in all cases this is an existential variable. Open a ticket and I may give you something better, even we could add a size fucntion in OCaml which is always going to be easier to maintain.
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:42):I keep running into more gotchas with the S-expression parsing, though, so I'd definitely appreciate it if you got the JSON support working!
Sorry to hear that, json is gonna take a while [did some progress but I need to discuss a bit with ocaml maintainers] We choose sexp for two reasons: a) most mature serializer in OCaml [industrail tested] and it is usually super-simple to parse. Don't hesitate to complain about the problems you are facing.
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:43):Definitively low-level proofs are huge in Coq, it would be a great improvement for you to request for the size directly.
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:44):Having different proof metrics seems like a good idea, and quite easy to do in OCaml [and much faster than sending the huge, printed expr]
Eli Dupree (Feb 16 2021 at 00:45):and it is usually super-simple to parse.
yeah, I'm sure I'd be capable of writing a parser for it, that's just ... not what I want to be doing with my time and energy :sob:
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:47):Yeah I understand :/
Eli Dupree (Feb 16 2021 at 00:47):a "proof size" query would be neat. I've also been thinking about (optionally) displaying proof diffs the same way I display goal diffs, because it's cool to be able to see the terms that are being generated
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:47):Actually after some changes I did this week, it would be easy to add a super silly mode where the input / output is filtered by a Sexp <-> Json converter
Eli Dupree (Feb 16 2021 at 00:48):on the OCaml end? That'd be a good stopgap!
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:48):This is far from ideal as it doesn't preserve records and other stuff, but it that would help please open a ticket
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:48):yeah it is quite easy to do so, open a ticket because otherwise I forget :)
Eli Dupree (Feb 16 2021 at 00:49):ok, I'll get to that in a bit!
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:49):Actually I am discussing with OCaml upstream, as I have a branch that is adding a Python API, a JSON API, now Rust, and I feel that something is wrong w.r.t. serialization as I have to use 3 different serializers for that, each one of them with their gotchas, and they are doing essentially the same
Eli Dupree (Feb 16 2021 at 00:49):speaking of diffs, doing diffs on the term structure would be better than my current lazy approach of diffing the string representations, although that's probably not something I can get to immediately (I'd have to do a bunch of work to understand the term structure, which is meaningful work, but there's easier stuff I should be doing first)
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:50):Json done the way above will be very ugly but at least you can work with it.
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:50):Yup, diffs on the term structure it is an interesting concept, we could implement it OCaml side of Rust side, in general we want a tree-diff algoritm, there are a few
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:51):A few people have implemented their own diffs for Coq terms already, PeaCoq, company-coq, Coq's diff mode, but none of them are fully satisfactory, I also like patdiff
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:51):A query to diff terms would be something I'd welcome
Eli Dupree (Feb 16 2021 at 00:51):oh now that I think about it, the messy JSON would actually be troublesome to work with, I'd like to be able to lean on serde_json automatically deserializing it into Rust types, but if the JSON isn't in the natural format for the data, I'd have to write custom Deserialize impls for everything
Eli Dupree (Feb 16 2021 at 00:53):serde's got a bit of easy customization of how to deserialize enums, but bigger customization is a lot of work
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:53):Indeed, that'd be messy
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:53):I will try to push the json support a bit more, but not this week for sure
Eli Dupree (Feb 16 2021 at 00:53):got it
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:53):What would be the data type most interesting for you?
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:54):To have in Json?
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:54):Because all the core datatypes are in Json already, so I could add a parameter to some queries to actually return a json
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:54):that would be quicker
Eli Dupree (Feb 16 2021 at 00:54):huh
Eli Dupree (Feb 16 2021 at 00:55):On first thought it feels like it would be a huge mess to have only part of the API be in JSON
Eli Dupree (Feb 16 2021 at 00:55):I'd be happy to just postpone the issue, coping with the current awkwardness until it can be done properly
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:56):It would be a hack until proper support lands
Eli Dupree (Feb 16 2021 at 00:56):For the "proof size" thing I just made a hardcoded special case where if serde_lexpr can't parse it then I assume it's huge
Eli Dupree (Feb 16 2021 at 00:57):I don't want to do the work of converting to a JSON API _twice_
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:57):It is just a bit sad that the Json serializers have been there for a while, however the protocol itself is not yet ported
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:57):Ok
Emilio Jesús Gallego Arias (Feb 16 2021 at 00:57):Note that I am talking now about "definitive" json objects, that is to say, the format wouldn't change
Eli Dupree (Feb 16 2021 at 01:00):That's less bad, but still. Better to focus your efforts on getting things done the clean way
Eli Dupree (Feb 16 2021 at 01:16):and yeah a term diff query would be a nice feature. Shall I open an Issue about it?
Emilio Jesús Gallego Arias (Feb 16 2021 at 01:21):Sure, I'm not sure if there is already something about it tho.
Emilio Jesús Gallego Arias (Feb 16 2021 at 01:24):Some discussion about it here https://github.com/jscoq/jscoq/issues/90
Eli Dupree (Feb 16 2021 at 01:26):well, a search of the SerAPI issues for "diff" didn't turn up anything, so, posted! https://github.com/ejgallego/coq-serapi/issues/233
Eli Dupree (Feb 16 2021 at 16:29):Here's another thing I'd like, but don't see a straightforward way to do: I'd like to have a string representation of a term where I also know which substrings represent subterms and which do not (e.g., in foo (bar baz quux), both bar baz quux and bar baz are also terms, but foo (bar and baz quux are not). I think a Constrexpr contains enough information to do that, but it seems nontrivial to convert Constrexpr to string, except through the Print command which doesn't preserve the information about subterms
At my level of understanding, I'm not 100% sure whether this is always well-defined given the generality of Notations, but in practice it seems like it would be useful
Eli Dupree (Feb 16 2021 at 16:35):(Specifically, I'm thinking of a UI where the user can select any subterm and see a menu of tactics like destruct (bar baz), exact (bar baz), unfold bar, etc.. As a UI convenience, I would want to automatically expand their selection to the nearest enclosing term, to save the confusion and extra clicks if they accidentally selected something like ar baz)
Eli Dupree (Feb 16 2021 at 16:43):maybe the right thing for me to do is get around to writing the Rust types for Constrexpr and learning how to process them
Emilio Jesús Gallego Arias (Feb 16 2021 at 16:58):There are two issues here IMO:
Emilio Jesús Gallego Arias (Feb 16 2021 at 17:01):CAst.t nodes; that way, you don't need to understand constrexpr, only the generic tree nodes and you can do something very similar to what you propose without a lot of effort. Emilio Jesús Gallego Arias (Feb 16 2021 at 17:02):By the way, some time ago I started a tool with the idea of actually writing Typescript types from OCaml type definitions, so people don't have to maintain those manually. Sadly it got stuck due to 2020 but we could resurrect it and add Rust support
Emilio Jesús Gallego Arias (Feb 16 2021 at 17:03):The tool itself is quite simple, you have OCaml's AST, and then Typescript AST, and you transform those.
Eli Dupree (Feb 24 2021 at 02:42):Took a break from this project for a week, but I'm back on it now, cleaned up my code, and I'm starting to implement more features
Eli Dupree (Feb 24 2021 at 02:43):Right now I'm trying to implement interrupting tactics that are taking a significant amount of time (EDIT: and generally interrupting commands when UI input invalidates them)
Eli Dupree (Feb 24 2021 at 02:43):I've been sending SIGINT to the child process, which usually seems to work fine, but sometimes after I send SIGINT, sertop seems to just stop responding
Eli Dupree (Feb 24 2021 at 02:46):oh hang on, it's sending back Sys.Break, it's my own code that just didn't report it
Eli Dupree (Feb 24 2021 at 02:51):but there's something weird going on on sertop's end I think
Eli Dupree (Feb 24 2021 at 02:53):Based on my output, I think it gets confused when I interrupt it while it's still parsing the command sexpr
Eli Dupree (Feb 24 2021 at 02:54):my code sent one command and then a SIGINT, and sertop sent back 8 sexp errors
Eli Dupree (Feb 24 2021 at 02:59):guess the natural idea is to wait for the Ack before sending SIGINT
Eli Dupree (Feb 24 2021 at 03:04):haha, there's another possible race condition where I send SIGINT during a command, but sertop completes the command before the SIGINT takes effect, and then my code sends another command, but the second command gets hit by the SIGINT. So I guess my code also needs to wait for sertop to acknowledge the SIGINT before proceeding
Eli Dupree (Feb 24 2021 at 03:26):alright, fixed that. Now I've got a situation where I receive an Ack, send SIGINT, and then really don't receive anything from sertop after that
Eli Dupree (Feb 24 2021 at 03:41):so my code is waiting for sertop to send back either a User interrupt. exception or Sys.Break (which seem like the ways it normally responds to SIGINT) but sertop's not sending anything so my code doesn't know it's safe to proceed
Eli Dupree (Feb 24 2021 at 03:43):at this point I'm not really sure what precautions I could take to make the behavior more consistent. I could introduce an explicit delay (of, say, 10ms) to hide the race conditions, but that would only avoid hitting race conditions about the command starting, and would still have potential race conditions about command completion, which I can't predict
Eli Dupree (Feb 24 2021 at 03:43):@Emilio Jesús Gallego Arias any input on this?
Eli Dupree (Feb 24 2021 at 14:05):Just looked up the code...
(* Follow the same approach than coqtop for now: allow Coq to be
* interrupted by Ctrl-C. Not entirely safe or race free... but we
* trust the IDEs to send the signal on coherent IO state.
*)
https://github.com/ejgallego/coq-serapi/blob/v8.12/sertop/sertop_sexp.ml#L219-L223
So the good news is, it's a relief to know I'm not just making a mistake somehow - it's definitely sertop that does not actually support this right now. I guess I should submit an issue
Emilio Jesús Gallego Arias (Feb 24 2021 at 14:59):Indeed @Eli Dupree even the core Coq implementation has some trouble being interrupted, SerAPI master provides a (Fork ...) command that while pretty heavy is more reliable. In many cases the problem of Ctrl-C not being acknolegded is due to because the OCaml runtime only processes interrupts in certain cases, such as when the GC is triggered, Coq manually inserts some check_for_interrupt to help with that, but it is fairly easy to have some tactics that get stuck in an inner loop. The problem with check_for_interrupt too often is that we measured a slowdown.
The other race is when sending Ctrl-C when for example we are printing, but those are easier to handle.
Emilio Jesús Gallego Arias (Feb 24 2021 at 15:00):So absolutely please open an issue with the concrete Coq code that is failing to be interrupted, and we'll try to improve it.
Eli Dupree (Feb 24 2021 at 15:02):just opened https://github.com/ejgallego/coq-serapi/issues/234
Eli Dupree (Feb 24 2021 at 15:04):wait, you think it's looping on the Coq end without checking for interrupts? I suppose that could be an additional issue but I don't think it's most of what I've been running into so far
Eli Dupree (Feb 24 2021 at 15:08):of course maybe it is, since I can only observe the system from the outside
Eli Dupree (Feb 24 2021 at 15:09):but that doesn't account for sending Completed while also not acknowledging the interrupt
Eli Dupree (Feb 24 2021 at 15:09):and I don't have any commands that are infinite-looping without the interrupt
Emilio Jesús Gallego Arias (Feb 24 2021 at 16:33):I'll check, but it is very likely that it is Coq itself looping.
Eli Dupree (Feb 24 2021 at 17:29):An interrupt would cause it to start looping when it wasn't looping before that?
Eli Dupree (Feb 24 2021 at 17:31):hmm, that does line up with what I'm seeing in my latest test
Eli Dupree (Feb 24 2021 at 17:32):no wait, if sertop is looping then shouldn't it be using a lot of CPU? it's not
Eli Dupree (Feb 24 2021 at 17:33):right now I have sertop being unresponsive but not using much CPU
Eli Dupree (Feb 24 2021 at 17:37):I wish I could give you a repeatable test case but so far I've only reproduced this by clicking around in my custom GUI a bunch
Eli Dupree (Feb 24 2021 at 18:04):I do have a 246200-line file of commandline output, which lists all the commands my program sent to sertop, if you're interested.
Eli Dupree (Feb 24 2021 at 18:07):turns out it only sent SIGINT 16 times before hitting a problem
Eli Dupree (Feb 24 2021 at 18:09):(because I started enforcing a 10ms delay from receiving Ack to sending SIGINT)
Eli Dupree (Feb 24 2021 at 18:11):The ultimate failure was during an Exec of progress eauto with *, which doesn't necessarily mean anything bad about that specific tactic, just that it was the tactic that lasted long enough to outlast the delay.
Eli Dupree (Feb 24 2021 at 18:17):Overall my current impression (based on the observed behavior and what you've told me) is "Coq was never designed to be safely interrupted, and retrofitting safe interruption onto it would be an enormous labor that I can't expect anyone to complete, so as I proceed with my proof explorer design, I should assume that I can never safely interrupt a command". Which, I guess, means there's no need for you to prioritize this issue for my sake
Emilio Jesús Gallego Arias (Feb 24 2021 at 21:38):Thanks so much for the careful bug report, I'm gonna investigate more as there are several possible issues, but indeed cleaning up the break handling was on the todo list for a long time, it is likely we have some issues.
Emilio Jesús Gallego Arias (Feb 24 2021 at 21:39):Regarding your last comment, it is IMHO a mix of both Coq and OCaml semantics, in fact OCaml has handled the way they handle interruptions a few times not so long ago IIANM. But I think that interrupting Coq properly is an essential feature so hopefully we can make it reliable.
Eli Dupree (Feb 25 2021 at 00:11):That makes sense. It's definitely a worthy feature to work on!
Paolo Giarrusso (Feb 25 2021 at 21:21):@Eli Dupree interrupting Coq safely would also be useful in all IDEs, including vscoq. Coqide could be more stable, not sure.
Eli Dupree (Mar 07 2021 at 14:45):@Emilio Jesús Gallego Arias How does sertop handle loadpaths/environment variables? I'm having trouble loading a second .v file. To debug, I've set COQPATH=/some/path, and when I run Print LoadPath. in coqtop, it shows /some/path, but when I run (Query () (Vernac "Print LoadPath. ")) in sertop, my custom path isn't listed
Emilio Jesús Gallego Arias (Mar 07 2021 at 16:39):Good question, I don't have the code of SerAPI in front of me right now, but I think COQPATH it is not just properly handled, I suggest you use -Q / -R options instead.
Emilio Jesús Gallego Arias (Mar 07 2021 at 16:40):This will be fixed in 8.14 for sure, as we have made enough progress on a huge refactoring including the build system so all tools [including SerAPI] will share the same code for loadpath handling
Emilio Jesús Gallego Arias (Mar 07 2021 at 16:41):as of today the situation is disastrous, with each tool handling it separately, but the make-based build system had bootstrapping issues due to coqdep , so I wasn't willing to improve it until we could use dune, which solves this bootstrapping problem.
Emilio Jesús Gallego Arias (Mar 07 2021 at 20:49):That being said, I'd be happy to add a patch for COQPATH if you need it .
Last updated: Feb 09 2023 at 00:03 UTC