Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

reverts the configuration of eglot-move-to-column-function introduced in 0883cce9 #977

Closed Rehan-MALAK closed 3 months ago

Rehan-MALAK commented 1 year ago

The workaround introduced in 0883cce9 to circumvent the utf8/utf16 problem explained in #452, breaks now the lambdapi-mode plugin for emacs ( at least with recent versions of eglot which is now a emacs builtin plugin ).

Many stuff changed since we talked about that (10/2020) : lambdapi lexer (sedlex), parser (menhir/pratter), syntax (ending tactic with semicolon, removed set builtin, ...)

I don't know what should be done : just remove this line ?

(setq eglot-move-to-column-function 'eglot-move-to-column)

@fblanqui @firewall2142 @gabrielhdt @ejgallego @joaotavora

Are there interesting stuffs to "backport" from ejgallego/coq-lsp#193 ?

ejgallego commented 1 year ago

Hi @Rehan-MALAK , actually indeed I was finally able to solved the UTF-8 problems in coq-lsp, and I'm planning to port lambdapi to new fleche code in that repository.

I'm a bit short on time these days but if someone would try to start the port I'd be happy to help, it is actually not hard as I designed the code there to be compatible with lambdapi (and other systems)

There is actually a branch that makes Flèche generic on the language at https://github.com/ejgallego/coq-lsp/pull/66 , it needs a bit of work but you can see the idea there.

fblanqui commented 1 year ago

Hi @Rehan-MALAK . Thank you for your issue. Could you please give more details about the problems you get because of this line, and with which versions of emacs and the packages?

Rehan-MALAK commented 1 year ago

Lambdapi : 3bb9efbe , 7 Apr 2023 Emacs : emacs-mirror/emacs@b8e7061232f, 10 Mar 2023 (so in particular >= 29))

lambdapi emacs mode installed via make install_emacs_mode (+ opam user-setup install + (load "lambdapi-site-file") in emacs init)

then opening tests/OK/boolean.lp, eglot/flymake does not work

error in process filter: eglot--lsp-position-to-point: Symbol’s function definition is void: eglot-move-to-column
error in process filter: Symbol’s function definition is void: eglot-move-to-column

by removing the line in the PR , eglot/flymake do work (but may reintroduce other bugs with utf 8/16, I dont know)

fblanqui commented 1 year ago

Hi. I don't know if it makes a difference but why don't you install the emacs mode from melpa? make install_emacs_mode should be used for local testing only. My own config is currently: emacs 27.1 / lambdapi-mode 20221228.1622 / eglot 20210611.2249. My version of eglot is old. The last version of eglot is 1.14 from April 3, 2023. It does not appear on Melpa but on GNU Elpa. Lambdapi appears on Melpa only. The last version of lambdapi-mode is 20221228.1622 (commit 1f4e1a on December 28, 2022). I don't know why it has not been updated since then. The dependencies of lambdapi-mode are eglot 1.5 / emacs 26.1 / highlight 20190710.1527 / math-symbol-lists 1.2.1. The last version of highlight is 20210318.2248. The last version of math-symbol-lists is 20220828.2047. We have to update the dependencies, especially wrt eglot. eglot seems to be in Emacs core now. I don't know since then. Perhaps this is the reason of the dependencies to be so old. But I don't know how to fix all this. @gabrielhdt @firewall2142 do you have any idea about this?

fblanqui commented 3 months ago

Thank you for your PR @Rehan-MALAK !