Literate programming of interactive proofs?

Literate programming of interactive proofs?

[Alan Schmitt]

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. 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? 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

Re: Literate programming of interactive proofs?

[Eric Schulte]

Alan Schmitt <alan.schmitt@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

Re: Literate programming of interactive proofs?

[Alan Schmitt]

Eric Schulte <schulte.eric@gmail.com> writes:

> If you do end up writing any level of support for Coq code blocks please
> consider contributing it to Org-mode.

Thanks a lot for these suggestions. I'll explore these options, and will
report back when I get something working.

Alan