[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [O] Literate programming of interactive proofs?

From: Eric Schulte
Subject: Re: [O] Literate programming of interactive proofs?
Date: Fri, 16 Nov 2012 09:05:32 -0700
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3.50 (gnu/linux)

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

> 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

    (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

[1]  http://www.jstatsoft.org/v46/i03

[2]  http://orgmode.org/manual/Working-With-Source-Code.html

Eric Schulte

reply via email to

[Prev in Thread] Current Thread [Next in Thread]