{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7066","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7066/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7066/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7066/events","html_url":"https://github.com/coq/coq/issues/7066","id":308278238,"number":7066,"title":"feature-request: editor-independent incremental compilation and feedback","user":{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-03-24T16:38:53Z","updated_at":"2018-03-24T17:43:05Z","closed_at":null,"author_association":"NONE","body":"This is a feature request, spinned off from https://github.com/coq/coq/issues/7055#issuecomment-375904541 and https://github.com/coq/coq/issues/7055#issuecomment-375905358. In short, I think it would be very useful to have a Coq equivalent of LaTeX `xdg-open *pdf & while : ; do make ; inotifywait -e modify *.tex ; done` that would produce a goal and error display regardless of the editor used for the source file. I think this would be valuable for new users (enabling them to get their feet wet quickly) and as a low-tech option for when the favorite IDE of the day is not available.\r\n\r\nIn particular, it would be cool if just saving the `.v` file triggered\r\n- immediate cancellation of processing of sentences that are no longer present in the file (or whose dependencies have changed)\r\n- backtracking of the proof state to the common prefix document of the processed proof state and the file contents\r\n- parallel processing of new sentences\r\n\r\nThe goals and feedback could be displayed in a separate terminal windows, and perhaps there could be example scripts for running this in the correct layout under tmux/xmonad/emacs/etc.\r\n\r\nThis entire setup should not depend on gtk or anything else not strictly required for proof processing. Even inotifywait might be better connected to stdin instead of compiled into the binary for better portability.\r\n\r\nI would probably be willing to do the implementation work for this if it is considered desirable and I figure out what I would be doing well enough.\r\n\r\n@ejgallego do I understand correctly that currently I need to compile my own copy of Coq if I want to use SerAPI?"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/375911298","html_url":"https://github.com/coq/coq/issues/7066#issuecomment-375911298","issue_url":"https://api.github.com/repos/coq/coq/issues/7066","id":375911298,"user":{"login":"andres-erbsen","id":918403,"avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"created_at":"2018-03-24T17:43:05Z","updated_at":"2018-03-24T17:43:05Z","author_association":"NONE","body":"Thanks for the honest overview of the state of the relevant interfaces.\r\n\r\nI am on Linux. It does look like I would need to build coq to use serapi (I will do it if that's the way we want it to work).\r\n\r\n~~~~~~~\r\nbrowse@ashryn ~/Downloads/coq-serapi (git)-[v8.8] % ocamlbuild -use-ocamlfind -j 4   sertop/sertop.native\r\n+ ocamlfind ocamldep -package cmdliner -package coq.intf,coq.stm,sexplib -modules sertop/sertop.ml > sertop/sertop.ml.depends\r\nocamlfind: Package `coq.intf' not found\r\nCommand exited with code 2.\r\nCompilation unsuccessful after building 1 target (0 cached) in 00:00:00.\r\n\r\nbrowse@ashryn ~/Downloads/coq-serapi (git)-[v8.8] % pacman -Ql coq | grep -i intf\r\ncoq /usr/lib/coq/intf/\r\ncoq /usr/lib/coq/intf/constrexpr.cmi\r\ncoq /usr/lib/coq/intf/constrexpr.cmx\r\n...\r\n~~~~~~~\r\n\r\nHowever, if even serapi would need a shim to track the document state, is there still good reason to use serapi instead of calling `stm` methods directly? I imagine that there would be an argument for that if serapi provided everytihng we need and was more stable than the stm ML interface, but right now it is not obvious to me what would be gained by doing this through serapi.\r\n\r\nRegarding asynchronous error-reporting, I don't actually know how it should work. If just processing until the first error is not good enough for this interface, I can go and learn about async error reporting (I guess I should install coqide and make a document with a bunch of errors and see what it does?). I do not find this feature nearly as important as incremental compilation corner cases like backtracking into sections, though."}}
{"actor":{"display_login":"andres-erbsen"}}