Clément Pit-Claudel
Clément Pit-Claudel
Hi John, This bit in `alert` seems fishy: ``` lisp (catch 'finish (dolist (config (append alert-user-configuration alert-internal-configuration)) (let* ((style-def (cdr (assq (or style (nth 1 config)) alert-styles))) ``` The body...
Recently (days/weeks?) ago, the listing format changed from a grep-like filename-on-every-line format to a grouped listing. THis seems to have broken wgrep editing of results. Repro: - `package-install`of `ag` and...
Hi Emilio. This is a follow up to https://github.com/coq/coq/issues/4834#issuecomment-655766329 (thanks for the quick response!) One thing Alectryon is missing compared to coqdoc is hyperlinking abilities. I'd like to (1) be...
Hey @ejgallego, How hard would it be to expose parent-child relationships between goals in the API? At the moment SerAPI prints less information than `coqtop -emacs` (the latter has a...
Hi Emilio, Hope you're doing OK despite the crazy times. In the project I'm workig on, it would be very useful to be able to get comments boundaries in addition...
I'm not sure what the proper way is to do this without breaking existing code. It's just a bit unfortunate that SerAPIs options are not spelled the same as Coq's
Repro: ``` coq Definition bullets: True \/ (True \/ True) -> True. Proof. - intros. destruct H. + { apply I. } + idtac. apply I. (* Try folding here...
This offers a measure of protection against potential ympd vulnerabilities. See https://www.freedesktop.org/software/systemd/man/systemd.exec.html for documentation.
Hi there, LSPdiagnostics have a relatedInformation field that LSP-mode does not seem to be using yet. How hard would it be to display these related locations? This was briefly discussed...
Is there a source for the following warning? ``` misc.but No paragraph should start with a 'But'. ``` Here's what Garner says on the subject (but, 3rd edition, p 121):...