ob-coq.el (2803B)
1 ;;; ob-coq.el --- Babel Functions for Coq -*- lexical-binding: t; -*- 2 3 ;; Copyright (C) 2010-2021 Free Software Foundation, Inc. 4 5 ;; Author: Eric Schulte 6 ;; Maintainer: Luc Pellissier <luc.pellissier@crans.org> 7 ;; Keywords: literate programming, reproducible research 8 ;; Homepage: https://git.sr.ht/~bzg/org-contrib 9 10 ;; This file is not part of GNU Emacs. 11 12 ;; GNU Emacs is free software: you can redistribute it and/or modify 13 ;; it under the terms of the GNU General Public License as published by 14 ;; the Free Software Foundation, either version 3 of the License, or 15 ;; (at your option) any later version. 16 17 ;; GNU Emacs is distributed in the hope that it will be useful, 18 ;; but WITHOUT ANY WARRANTY; without even the implied warranty of 19 ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 20 ;; GNU General Public License for more details. 21 22 ;; You should have received a copy of the GNU General Public License 23 ;; along with GNU Emacs. If not, see <https://www.gnu.org/licenses/>. 24 25 ;;; Commentary: 26 27 ;; Rudimentary support for evaluating Coq code blocks. Currently only 28 ;; session evaluation is supported. Requires both coq.el and 29 ;; coq-inferior.el, both of which are distributed with Coq. 30 ;; 31 ;; https://coq.inria.fr/ 32 33 ;;; Code: 34 (require 'ob) 35 36 (declare-function run-coq "ext:coq-inferior.el" (cmd)) 37 (declare-function coq-proc "ext:coq-inferior.el" ()) 38 39 (defvar coq-program-name "coqtop" 40 "Name of the coq toplevel to run.") 41 42 (defvar org-babel-coq-buffer "*coq*" 43 "Buffer in which to evaluate coq code blocks.") 44 45 (defun org-babel-coq-clean-prompt (string) 46 (if (string-match "^[^[:space:]]+ < " string) 47 (substring string 0 (match-beginning 0)) 48 string)) 49 50 (defun org-babel-execute:coq (body params) 51 (let ((full-body (org-babel-expand-body:generic body params)) 52 (session (org-babel-coq-initiate-session)) 53 (pt (lambda () 54 (marker-position 55 (process-mark (get-buffer-process (current-buffer))))))) 56 (org-babel-coq-clean-prompt 57 (org-babel-comint-in-buffer session 58 (let ((start (funcall pt))) 59 (with-temp-buffer 60 (insert full-body) 61 (comint-send-region (coq-proc) (point-min) (point-max)) 62 (comint-send-string (coq-proc) 63 (if (string= (buffer-substring (- (point-max) 1) (point-max)) ".") 64 "\n" 65 ".\n"))) 66 (while (equal start (funcall pt)) (sleep-for 0.1)) 67 (buffer-substring start (funcall pt))))))) 68 69 (defun org-babel-coq-initiate-session () 70 "Initiate a coq session. 71 If there is not a current inferior-process-buffer in SESSION then 72 create one. Return the initialized session." 73 (unless (fboundp 'run-coq) 74 (error "`run-coq' not defined, load coq-inferior.el")) 75 (save-window-excursion (run-coq coq-program-name)) 76 (sit-for 0.1) 77 (get-buffer org-babel-coq-buffer)) 78 79 (provide 'ob-coq) 80 81 ;;; ob-coq.el ends here