Idris 1.3.2版和Atom已成功安装在Ubuntu Linux的Kubuntu版本上。 idris二进制文件的正确路径已放入Atom的程序包设置中。 REPL在Atom中可以正常工作。idris二进制文件的位置是/ home / tom / Documents。我的1行源文件称为WordLength.idr文件，该文件保存在Atom中，由以下文件给出：
allLengths : List String -> List Nat
（如布雷迪书第56页所述。保存此文件的位置是/home/tom/.cabal/bin/idris。
[当我在Linux命令窗口中启动idris时，类型检查将按要求进行，并且正确报告了“ holes Main.allLengths”。
然而，在第57页所述的'Define'阶段，我的问题是，当我在Atom编辑器中用光标突出显示所有长度并按第57页上的说明按Ctrl-Alt-A时，Atom没有响应。将多余的行作为骨架定义添加到编辑器中的源文件中。
我曾试图将各种其他路径添加到$ PATH文件中，但徒劳地希望这可以解决问题。
这是一些Linux / Window Manager发行版中的一种已知问题，我们不愿意为idris插件进行修复，因为所有的键绑定都在Edwins关于Idris的书中提到。目前，您的解决方法是更改键绑定。另请参见https://github.com/idris-hackers/atom-language-idris/pull/204
请根据您的需要将Atom中的键绑定更改为适合您的内容（命令面板：显示键绑定）