Emacs org-mode integration

[coquser]

Hi,

I have been using org-mode to take all my notes. As you may know, org has a feature called babel, which allows you to run/extract code from an org file.

The now replaced coq-mode from the official coq distribution provided a certain file, called inferior-coq.el (​https://github.com/coq/coq/blob/d651b97b23bb827aaaf109e9bf29da244cd41704/tools/inferior-coq.el)

This file provided a command "run-coq" which in turn is used by ob-coq. A lisp file from the emacs distribution. (​https://git.sr.ht/~bzg/org-contrib/tree/master/item/lisp/ob-coq.el)

This allowed users, to have a source block in their org files, and with C-c C-c to run coq, and get their result under the source block.

But since all emacs coq files from the official coq distribution have been removed in favor of Proof General, this no longer works. Which is sad, as it was a great feature.

My question is, would it be possible to add support for the run-coq command? Or some version of ob-coq, maybe even more general, that would allow to send queries to Proof General, similiar how C-c C-n now works in .v files. It would allow a greater integration with org mode and it's superb literate programming facilities and I would gladly appreciate it.

I tried to add it myself, but I realised that Proof General does things quite differently and I cannot implement it with some hack.

With all the best wishes, Maya