Commit e15f8db2 authored by Michael Sammler's avatar Michael Sammler
Browse files

added emacs setup to readme

parent b4c72e88
......@@ -367,7 +367,10 @@ the `dune` environment one should not call `dune`.
# !!!INVALID!!!
dune exec -- refinedc check examples/queue.c
# Equivalent valid command sequence.
# Alternative
./ examples/queue.c
# Equivalent to the following valid command sequence.
dune exec -- refinedc check --no-build examples/queue.c
cd examples/proofs/queue
dune build
......@@ -378,6 +381,27 @@ To generate the Coq code for all the examples of the repository you can run
`make generate_all`. You can also force the generation of all the generated
code using `make -B generate_all`.
## Emacs setup
The following elisp function enables direct execution of the `` script in this repo from emacs.
It searches for a `` file in parent directories of the current file and executes it with the name
of the current file. A similar functionallity should be easy to add to other editors as well.
This script binds `build` to the keys `C-c c`. Use at your own risk!
(setq build-file-name "")
(defun build ()
"Search in the current and parent directories for a file with the name of variable `build-file-name' and execute the first file it find."
(save-some-buffers t) ; save all buffers
(let ((buildfile (locate-dominating-file default-directory build-file-name)))
(unless buildfile (error "No build file found!"))
(let ((default-directory buildfile))
(compile (concat buildfile build-file-name " " (buffer-file-name))))
(select-window (get-buffer-window "*compilation*"))))
(global-set-key (kbd "C-c c") 'build)
## Structure of the repository
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment