Documenting Coq Code using Org-mode

body

Goal

The approach described here lets you document a development, for instance of Coq code, using a document written in Org-mode. The documentation is supposed to be outside of the source, so that the source does not need to be modified. To avoid copy and paste of the code to be documented, we use a fetch function that fetches the code and insert it in the current buffer, for instance when exporting to LaTeX or html. It can also be used in place to have the code visible.

The fetch function

Here is the source of this function, as part of an org-mode code block.

#+name: fetch
#+header: :results raw
#+header: :var path="../coq/"
#+header: :var file="foo"
#+header: :var ext=".v"
#+header: :var start="Definition"
#+header: :var end="\\. *$"
#+header: :var omitend=()
#+header: :var lang="coq" 
#+BEGIN_SRC emacs-lisp :exports none
(defun fetchlines (file-path search-string &optional search-end omit-last)
  "Searches for the SEARCH-STRING in FILE-PATH and returns the matching line.
   If the optional argument SEARCH-END is provided as a number,
   then this number of lines is printed. If SEARCH-END is a
   string, then it is a regular expression indicating the end of
   the expression to print. If SEARCH-END is omitted, then 10
   lines are printed. If OMIT-LAST is not nil, then only print up
   to the line before."
  (let ((myBuffer (get-buffer-create "fetchTemp")) result)
    (set-buffer myBuffer)
    (insert-file-contents file-path nil nil nil t)
    (goto-char 1)

    (setq result
          (if (search-forward search-string nil t)
              (let ((pos-beg (line-beginning-position))
                    (pos-end
                     (if search-end
                         (cond
                          ((integerp search-end)
                           (line-end-position
                             (if omit-last (- search-end 1) search-end)))
                          ((stringp search-end)
                           (let ((point (re-search-forward search-end nil t)))
                             (if omit-last (line-end-position 0) point)))
                          (t (line-end-position 10)))
                       (line-end-position 10))))
                (buffer-substring pos-beg pos-end))
            ""))

    (kill-buffer myBuffer)
    result))

(let ((src (fetchlines (concat path file ext) start end omitend)))
  (if lang
    (concat "#+begin_src " lang "\n" src "\n#+end_src")
  src))
#+END_SRC

This is actually an emacs-lisp function that is made available to Org code. The arguments of the function are path, the directory were the file leaves (../coq/ by default), the name file of the file without its extension (for the moment the extension is hard-coded), the string start to search for as start of the code to fetch, the string end to search for as end of the code to fetch (the default is the first . followed by spaces and the end of line, you can look at the documentation string in the function for other values possible), whether omitend to include the last line in the fetched code, and the language lang of the source block created (default is coq).

To use it, you write an Org-babel call line:

#+call: fetch(path="",file="test",start="Definition Test")

Longer example

We published a research paper using an older version of this approach. The source is available here.