Alan Schmitt <alan.schm...@polytechnique.org> writes:
> Hello,
>
> I want to use org-mode to write a paper about a development in Coq. Coq
> is an interactive proof system, which can be run (among other ways)
> interactively through emacs. The interactive part is very important, as
> doing or maintaining proofs often requires exploring many different
> direction.
>
> I'm wondering if it's still possible to use org-mode to write such a
> paper.
Yes, this is possible. See here [1] for a paper demonstrating the use
of Org-mode to support both literate programming and reproducible
research.
> I see two ways of doing it: - either be able to interactively interact
> with Coq from org-mode - or write the development separately, and have
> a way to include parts of the file (for instance identified by special
> markers in some comments) into the final paper.
>
> Is any of this possible?
Either will be possible with a little bit of work.
In either case I think you will want to implement Org-mode code block
support (see [2]) for Coq. Code blocks allow Org-mode to interact with
external processes and programming languages, and can be used for simple
things like running external shell commands or more complex cases like
interacting with a persistent R process through ESS. Interactive use of
code blocks are called "sessions" in the Org-mode documentation.
Assuming that there exists (or can be easily written) a function which
passes commands to the Coq process and returns results, e.g., something
that would be used to drive an interactive Coq console, lets call this
function `coq-eval' for the purpose of this email. Then the following
elisp snippet would be sufficient to provide minimal Coq code block
support.
(defun org-babel-execute:coq (body params)
(coq-eval body))
If you do end up writing any level of support for Coq code blocks please
consider contributing it to Org-mode.
Hope this helps,
> The second option would probably require some custom code, but I don't
> know if it would be very complex.
>
> Thanks a lot,
>
> Alan Schmitt
>
Footnotes:
[1] http://www.jstatsoft.org/v46/i03
[2] http://orgmode.org/manual/Working-With-Source-Code.html
--
Eric Schulte
http://cs.unm.edu/~eschulte
