Re: [O] Literate programming of interactive proofs?

[Eric Schulte]

Alan Schmitt <address@hidden> 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