The README's advice for installing idris2-mode can break emacs startup

[rntz]

The README suggests adding the following to .emacs.d/init.el:

(add-to-list 'load-path "~/.emacs.d/idris2-mode/")
(require 'idris2-mode)

However, idris2-mode requires prop-menu, and if this package is not installed this will break, which will break emacs startup.

[rntz]

I suggest listing use-package instead of (or as an alternative to) require here, eg:

(add-to-list 'load-path (locate-user-emacs-file "idris2-mode"))
(use-package idris2-mode)

which will warn instead of erroring if idris2-mode fails to load.

[Luexa]

Additionally, with straight.el you can use the following use-package declaration:

(use-package idris2-mode
  :straight (idris2-mode :type git :host github
                         :repo "idris-community/idris2-mode"))

This will automatically fetch idris2-mode and all dependencies, and provide the same experience as packages on (M)ELPA. It will also automatically byte-compile (and native-compile if possible) the package and generate autoloads for more efficient startup in the future. Of course, using straight.el requires a few changes to your init-file if you currently rely on package.el.