Julien Puydt (May 25 2022 at 20:34): Julien Puydt (May 25 2022 at 20:34):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?
Julien Puydt (May 25 2022 at 21:26):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)
Gaëtan Gilbert (May 25 2022 at 21:35):127 may mean "command not found"
Julien Puydt (May 26 2022 at 05:49):@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 :-/
Julien Puydt (May 26 2022 at 05:50):Oh, I had a big doubt, closed emacs, retried, and now the error number is 1 -- my changes hadn't been taken into account!
Julien Puydt (May 26 2022 at 05:52):Ah, ha, and if I set sertop-executable-path and not sertop-coq-directory, it looks like the prelude gets loaded!
Julien Puydt (May 26 2022 at 05:54):And indeed, if I type in (Add () "Lemma addn0 n : n + 0. Proof. now induction n. Qed."), it looks like something gets done.
Julien Puydt (May 26 2022 at 05:54):Following up with (Exec 5) gives a segmentation fault, though.
Gaëtan Gilbert (May 26 2022 at 09:05):defvar only sets the variable if it is unset
Julien Puydt (May 26 2022 at 09:16):@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.
Emilio Jesús Gallego Arias (May 26 2022 at 10:38):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