Idris ver 1.3.2 и Atom были успешно установлены на версию Ubuntu Kubuntu Linux. В настройках пакета в Atom указан правильный путь к двоичному файлу idris. REPL работает нормально в Atom. Расположение двоичного файла idris: / home / tom / Documents. Мой исходный файл в 1 строку под названием WordLength.idr, который сохраняется в Atom, имеет вид:
allLengths : List String -> List Nat
(как описано на стр. 56 книги Брэди). Местоположение, в котором сохранен этот файл: /home/tom/.cabal/bin/idris.
Когда я запускаю idris в командном окне Linux, проверка типа работает как требуется, и 'отверстия Main. Все длины указаны правильно.
Однако на этапе «Определить», как описано на стр. 57, моя проблема заключается в том, что я выделяю курсором все длины с помощью курсора в редакторе Atom и нажимаю Ctrl-Alt-A, как требуется на странице. 57 нет ответа от Atom, когда он должен добавить дополнительную строку в качестве определения каркаса к исходному файлу в редакторе.
Я пытался добавить различные дополнительные пути к файлу $ PATH в тщетной надежде, что это вылечит проблему.