Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
;; The following works with OPAM 2.0.x
;; Put this piece of code into your .emacs and use it interactively as
;; M-x coq-change-compiler
;; If you change your OPAM installation by e.g. adding more switches, then
;; run M-x coq-update-opam-switches and coq-change-compiler will show the updated set of switches.
(defun opam-ask-var (switch package var)
(ignore-errors (car (process-lines
"opam" "var" "--safe" "--switch" switch (concat package ":" var)))))
(defun opam-installed-switches ()
"Get a list of all installed OPAM switches."
(process-lines "opam" "switch" "--safe" "list" "--short"))
(defun opam-current-switch ()
"Get the current OPAM switch."
(ignore-errors (car (process-lines "opam" "switch" "--safe" "show"))))
(setq opam-current-switch (opam-current-switch))
(setq opam-switches (opam-installed-switches))
;; filter out all OPAM switches not containing Coq installations
(defun coq-opam-switches-with-coq-to-bindir ()
"Returns alist of (<OPAM switch> / <Coq version> . <Coq's binary directory>."
(lambda (sw.bin) (stringp (cdr sw.bin)))
;; (cons ("Local ." . "~/prj/coq/bin/")
(lambda (sw)
; mark the current OPAM switch
; this is all ugly, put I don't want to put more effort in it :(
(if (string= sw opam-current-switch) "-> " " ")
sw " / coq-" (opam-ask-var sw "coq" "version"))
(opam-ask-var sw "coq" "bin")))
(setq coq-bin-dirs-alist (coq-opam-switches-with-coq-to-bindir))
(defun coq-update-opam-switches ()
"Update the alist of OPAM switches with Coq installed"
(setq opam-switches (opam-installed-switches))
(setq coq-bin-dirs-alist (coq-opam-switches-with-coq-to-bindir))
(message "OPAM switches updated."))
(defun coq-change-compiler (coq-bin-dir)
"Change Coq executables to use those in COQ-BIN-DIR."
(list (cdr (assoc (completing-read "Compiler: " coq-bin-dirs-alist)
(when (stringp coq-bin-dir)
(setq coq-compiler (concat coq-bin-dir "/coqc"))
(setq coq-prog-name (concat coq-bin-dir "/coqtop"))
(setq coq-dependency-analyzer (concat coq-bin-dir "/coqdep"))
(message "Using Coq binaries from %s." coq-bin-dir)
(when (proof-shell-available-p)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment