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.