Flycheck is broken.

[jfdm]

The flycheck instance has been created to work with Idris1.

With the rise of Idris2 we need to make sure both Idris and Idris2 are supported.

[jfdm]

I think this has been resolved with #609, however, I have experienced issues from the default configuration.

1. idris2 executable cannot be found;
2. both idris2 and idris flycheckers are registered for idris-mode with the default being idris;

It would be prudent to either think about sane defaults, or produce advice on a good starting configuration.

[keram]

1. idris2 executable cannot be found;

Hi @jfdm
What is the output when invoking M-x flycheck-verify-setup in some *.idr file?

2. both idris2 and idris flycheckers are registered for idris-mode with the default being idris;

It would be prudent to either think about sane defaults, or produce advice on a good starting configuration.

in my .emacs.d/init.el file to enable the flycheck mode i have currently explicit:

(require 'idris-mode)
(require 'flycheck-idris)
(add-hook 'idris-mode-hook #'flycheck-mode)

And M-x flycheck-verify-setup produces:

Syntax checkers for buffer MakeLemma.idr in idris-mode:

First checker to run:

  idris2
    - may enable: yes
    - executable: Found at /home/mXidris2/bin/idris2

Checkers that could run if selected:

  idris  select
    - may enable: yes
    - executable: Found at /home/X/.cabal/bin/idris

Flycheck Mode is enabled. Use C-u C-c ! x to enable disabled checkers.

--------------------

Flycheck version: 33snapshot (package: 20221213.107)
Emacs version:    28.2

The list of enabled checkers is stack (lifo) meaning the last defined Idris2 is selected as first to be used by default.
If executable is not found the checker should be automatically disabled and next one selected.

  idris2 (automatically disabled) reset
    - may enable: no
    - executable: Not found

Agree that some documentation/readme update may begg needed.

[jfdm]

My issues seem to resolve around finding the Idris2 executable. It might be that some other customisations I have done when configuring idris-mode interferes with the default operation.

[keram]

Over weekend I played with my setup and converted it to use use-package which is what I assume 90% users use to install packages.

(use-package idris-mode
  ;; :ensure t ;; Installing from (M)ELPA

  ;; Loading local source from https://github.com/idris-hackers/idris-mode
  :init (require 'idris-mode)
  :load-path "vendor/idris-mode"

  :config
  (require 'flycheck-idris) ;; Syntax checker
  (add-hook 'idris-mode-hook #'flycheck-mode)

  (require 'idris-format) ;; Prettification commands
  (add-to-list 'completion-ignored-extensions ".ibc") ;; Idris 1 artefacts

  ;; save keys
  (key-chord-define idris-mode-map "e." ">>= ")
  (key-chord-define idris-mode-map "w=" "=> ")
  (key-chord-define idris-mode-map "w." "-> ")
  (key-chord-define idris-mode-map "w," "<- ")

  :custom
  (idris-interpreter-path "idris2")
  ;; minimise distraction
  (idris-hole-show-on-load nil)
  (idris-repl-show-repl-on-startup nil)

  ;; does not work with Idris2 but one day should
  (idris-enable-elab-prover t)
  
  ;; for development and debugging
  (idris-log-events t)

  ;; custom key binding for commands that do not have
  ;; pre defined key binding 
  :bind (:map idris-mode-map
              ("C-c h" . idris-list-holes)))