From mboxrd@z Thu Jan 1 00:00:00 1970 From: Alan Schmitt Subject: Literate programming of interactive proofs? Date: Thu, 15 Nov 2012 16:52:43 +0100 Message-ID: Mime-Version: 1.0 Content-Type: text/plain Return-path: Received: from eggs.gnu.org ([208.118.235.92]:36266) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1TZ1kH-0007s5-5v for emacs-orgmode@gnu.org; Thu, 15 Nov 2012 10:52:52 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1TZ1kE-0007TZ-3H for emacs-orgmode@gnu.org; Thu, 15 Nov 2012 10:52:49 -0500 Received: from mail4-relais-sop.national.inria.fr ([192.134.164.105]:8041) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1TZ1kD-0007SK-TR for emacs-orgmode@gnu.org; Thu, 15 Nov 2012 10:52:46 -0500 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: emacs-orgmode 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