search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

[idris2-mode] "Unused lexical variable 'name'" #543

Closed gergoerdi closed 2 years ago

gergoerdi commented 2 years ago

Precompiling idris2-mode with the included Makefile fails with the following error message:

emacs --batch --no-site-file -q -eval '(add-to-list (quote load-path) "/home/cactus/prog/idris/idris2/bugs/emacs-mode/.emacs.d/elisp/idris2-mode/")' -eval '(require (quote package))' -eval '(add-to-list (quote package-archives) (quote ("melpa" . "http://melpa.org/packages/")) t)' -eval '(package-initialize)' -eval '(progn (require (quote bytecomp)) (setq byte-compile-warnings t) (setq byte-compile-error-on-warn t))' -f batch-byte-compile idris2-commands.el

In toplevel form:
idris2-commands.el:365:1:Error: Unused lexical variable ‘name’

This can be worked around by setting byte-compile-error-on-warn to nil, but of course it would be better if someone actually looked at idris2-commands.el and see if idris2-jump-to-location has some error in it.

jfdm commented 2 years ago

Sorry for the late reply, I have not hat time to do as much maintenance on Idris-mode as I would like. I cannot promise that I will get to this, but PRs are more than welcome. Thanks.

gallais commented 2 years ago

Should this bug report be moved to https://github.com/idris-community/idris2-mode?

jfdm commented 2 years ago

i didn't realise it was Idris2! Then of course it should.

jfdm commented 2 years ago

There is a transfer option! @gallais feel free to do that. You should have privileges.

gallais commented 2 years ago

I don't think it's possible to transfer an issue across organisations.

gallais commented 2 years ago

I'm assuming this has been fixed by https://github.com/idris-community/idris2-mode/pull/9