Stream: SerAPI

Topic: sertop.el's sertop-coq-directory


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (May 25 2022 at 21:35):

127 may mean "command not found"

view this post on Zulip 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 :-/

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Julien Puydt (May 26 2022 at 05:54):

Following up with (Exec 5) gives a segmentation fault, though.

view this post on Zulip Gaëtan Gilbert (May 26 2022 at 09:05):

defvar only sets the variable if it is unset

view this post on Zulip 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.

view this post on Zulip 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: Feb 06 2023 at 06:29 UTC