At the top of sertop.el, this variable is said to point to Coq's stdib, but the comment at definition-time says it's about the sources... I suspect the first one is right, but I'll rather ask than be proven wrong.
I was wondering if instead of nil the Debian package shouldn't point it to where the Coq stdlib is installed. And since I don't know anything about emacs, is s/nil/"/usr/lib/ocaml/coq"/ what I need to do?
I just tried to load sertop.el in emacs, run M-x eval-buffer then M-x sertop, and
Process Sertop exited abnormally with code 127 (and changing sertop-coq-directory like I suggested doesn't change that).
(Well, to be honest, I do know how to use emacs for simple things, so I'm not completely in the dark, but I never dug into its lisp)
127 may mean "command not found"
@Gaëtan Gilbert That was also my first thought ; but my sertop.el reads:
(defvar sertop-executable-path "/usr/bin/sertop" "Path to sertop.") (defvar sertop-coq-directory "/usr/lib/ocaml/coq" "Location of the directory containing Coq's sources, or nil.")
so I don't think that's it :-/
Oh, I had a big doubt, closed emacs, retried, and now the error number is 1 -- my changes hadn't been taken into account!
Ah, ha, and if I set
sertop-executable-path and not
sertop-coq-directory, it looks like the prelude gets loaded!
And indeed, if I type in
(Add () "Lemma addn0 n : n + 0. Proof. now induction n. Qed."), it looks like something gets done.
Following up with
(Exec 5) gives a segmentation fault, though.
defvar only sets the variable if it is unset
@Gaëtan Gilbert sertop is in my path, so it's strange it doesn't get found if I don't set sertop-executable-path.
It's been a while I dont' use sertop.el , maybe @Clément Pit-Claudel who is the author has a hint?
Last updated: Jun 11 2023 at 01:30 UTC