Emacs mode setup is insufficient: opam-share is void
Hello,
When following Why3 documentation to setup Why3 Emacs mode (https://why3.gitlabpages.inria.fr/why3/install.html#emacs), I stumbled on an Emacs error: "opam-share
variable is void". My understanding is that this variable should be defined beforehand. I copied/pasted its definition from Merlin documentation. With below changes, I have no error and expected behavior.
(let ((opam-share (ignore-errors (car (process-lines "opam" "var" "share")))))
(when (and opam-share (file-directory-p opam-share))
(setq why3-share (if (boundp 'why3-share) why3-share (ignore-errors (car (process-lines "why3" "--print-datadir")))))
(setq why3el
(let ((f (expand-file-name "emacs/why3.elc" why3-share)))
(if (file-readable-p f) f
(let ((f (expand-file-name "emacs/site-lisp/why3.elc" opam-share)))
(if (file-readable-p f) f nil)))))
(when why3el
(require 'why3)
(autoload 'why3-mode why3el "Major mode for Why3." t)
(setq auto-mode-alist (cons '("\\.mlw$" . why3-mode) auto-mode-alist)))
))
I think Why3 documentation should be updated with above changes.
Best regards, david