From mboxrd@z Thu Jan 1 00:00:00 1970 From: Eric Schulte Subject: Re: Literate programming of interactive proofs? Date: Fri, 16 Nov 2012 09:05:32 -0700 Message-ID: <87txspilbm.fsf@gmail.com> References: Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([208.118.235.92]:58719) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1TZOQS-0000eU-9q for emacs-orgmode@gnu.org; Fri, 16 Nov 2012 11:05:55 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1TZOQP-0004Yl-7H for emacs-orgmode@gnu.org; Fri, 16 Nov 2012 11:05:52 -0500 Received: from mail-ia0-f169.google.com ([209.85.210.169]:59682) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1TZOQP-0004YZ-1T for emacs-orgmode@gnu.org; Fri, 16 Nov 2012 11:05:49 -0500 Received: by mail-ia0-f169.google.com with SMTP id r4so2197814iaj.0 for ; Fri, 16 Nov 2012 08:05:48 -0800 (PST) List-Id: "General discussions about Org-mode." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org Sender: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org To: Alan Schmitt Cc: emacs-orgmode Alan Schmitt 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