目前Idris 2的学习资料还是比较少的最新的资料可能就是官方文档了其次就是《Type Driven Development with Idris》这本书虽然是针对Idris 1的但是很多内容还是适用的不适用的部分官方文档也有说明https://idris2.readthedocs.io/en/latest/typedd/typedd.html。即使这样这两个资料加起来还是没有覆盖Idris 2的所有内容比如存在量词需要结合Haskell相关资料学习。好在Haskell跟Idris 2基本上可以无缝切换前提是知晓两者的异同。本篇文章主要介绍Idris 2的编译器安装官方文档已有专门的文章介绍而且写得很详细我就不再赘述了。官方文档地址https://idris2.readthedocs.io/en/latest/tutorial/starting.html我按照官方文档的步骤成功编译并安装了Idris 2的编译器。把遇到的问题记录在这里方便大家参考。Windows安装Windows下没有可用的二进制安装包需要自己编译安装。我遇到的唯一问题就是ChezScheme 10.4.1安装过程没法选择安装路径会默认安装到Program Files目录下。因为目前Idris 2不支持包含空格的路径所以你需要在安装完成后将安装目录移动到不含空格的路径。我把编译好的Idris 2编译器和安装后的ChezScheme文件都放到了网盘里大家可以自行下载。分享的文件.idris2.rar 链接https://pan.baidu.com/s/1ncxWWlJz7uCD-beBIKJSnA?pwdbfh4 分享的文件Chez.rar 链接https://pan.baidu.com/s/1HUaVPPvffyxvvLF7mr4gHQ?pwdbfh4将下载的文件解压到不含空格的路径比如.idris2.rar解压到用户目录下的C:\Users\xxxx\.idris2在PATH环境变量添加C:\Users\xxxx\.idris2\bin比如Chez.rar解压到C:\在PATH环境变量添加C:\Chez\bin\ta6nt非Windows系统安装尽量使用包管理器安装很多系统的软件仓库里已经有了二进制安装包。比如Arch Linux、Fedora、macOS等。虽然其他发行版没有可用的二进制安装包但Nix上有可用的二进制安装包这样就可以曲线救国先安装Nix然后用Nix安装Idris 2的编译器验证安装在终端或命令行敲入idris2如果出现下面的输出说明安装成功了$ idris2 ____ __ _ ___ / _/___/ /____(_)____|__\/ // __ / ___/ / ___/ __/ / Version0.8.0 _/ // /_/ / / /(__)/ __/ https://www.idris-lang.org /___/\__,_/_/ /_/____/ /____/ Type :?forhelpWelcome to Idris2. Enjoy yourself!Main这实际是进入了REPLRead-Eval-Print-Loop环境类似于Haskell的ghci界面所有的命令可以通过输入:?来查看。我们先了解以下几个命令即可:?、:h或:help显示所有命令:t或:type检查变量的类型:q或:quit退出REPL:c或:compile编译为可执行文件:l或:load加载文件:r或:reload重新加载当前文件如下面的操作序列Main:lhello.idrLoadedfilehello.idr Main:r Loadedfilehello.idr Main:t main Main.main:IO()Main:c hello main File build/exec/hello written Main:q Byefornow!编译运行代码这是Idris 2的hello world代码文件名是hello.idrmoduleMainmain:IO()mainputStrLnHello world编译代码比较简单$ idris2 hello.idr-ohello运行代码$ ./build/exec/hello Hello world编译后会生成一系列目录和文件build/ ├── exec │ ├── hello │ └── hello_app │ ├── compileChez │ ├── hello.so │ ├── hello.ss │ └── libidris2_support.so └── ttc └── 2025081600 ├── hello.ttc └── hello.ttm现阶段不用太多关注知道以下几点就够了build/exec— 跟程序执行有关的文件放在该目录build/exec/hello— “可执行文件”实际上它就是个shell或bat脚本调用了hello.so。build/ttc/— 类型检查结果放在该目录
Idris 2教程--编译器安装
目前Idris 2的学习资料还是比较少的最新的资料可能就是官方文档了其次就是《Type Driven Development with Idris》这本书虽然是针对Idris 1的但是很多内容还是适用的不适用的部分官方文档也有说明https://idris2.readthedocs.io/en/latest/typedd/typedd.html。即使这样这两个资料加起来还是没有覆盖Idris 2的所有内容比如存在量词需要结合Haskell相关资料学习。好在Haskell跟Idris 2基本上可以无缝切换前提是知晓两者的异同。本篇文章主要介绍Idris 2的编译器安装官方文档已有专门的文章介绍而且写得很详细我就不再赘述了。官方文档地址https://idris2.readthedocs.io/en/latest/tutorial/starting.html我按照官方文档的步骤成功编译并安装了Idris 2的编译器。把遇到的问题记录在这里方便大家参考。Windows安装Windows下没有可用的二进制安装包需要自己编译安装。我遇到的唯一问题就是ChezScheme 10.4.1安装过程没法选择安装路径会默认安装到Program Files目录下。因为目前Idris 2不支持包含空格的路径所以你需要在安装完成后将安装目录移动到不含空格的路径。我把编译好的Idris 2编译器和安装后的ChezScheme文件都放到了网盘里大家可以自行下载。分享的文件.idris2.rar 链接https://pan.baidu.com/s/1ncxWWlJz7uCD-beBIKJSnA?pwdbfh4 分享的文件Chez.rar 链接https://pan.baidu.com/s/1HUaVPPvffyxvvLF7mr4gHQ?pwdbfh4将下载的文件解压到不含空格的路径比如.idris2.rar解压到用户目录下的C:\Users\xxxx\.idris2在PATH环境变量添加C:\Users\xxxx\.idris2\bin比如Chez.rar解压到C:\在PATH环境变量添加C:\Chez\bin\ta6nt非Windows系统安装尽量使用包管理器安装很多系统的软件仓库里已经有了二进制安装包。比如Arch Linux、Fedora、macOS等。虽然其他发行版没有可用的二进制安装包但Nix上有可用的二进制安装包这样就可以曲线救国先安装Nix然后用Nix安装Idris 2的编译器验证安装在终端或命令行敲入idris2如果出现下面的输出说明安装成功了$ idris2 ____ __ _ ___ / _/___/ /____(_)____|__\/ // __ / ___/ / ___/ __/ / Version0.8.0 _/ // /_/ / / /(__)/ __/ https://www.idris-lang.org /___/\__,_/_/ /_/____/ /____/ Type :?forhelpWelcome to Idris2. Enjoy yourself!Main这实际是进入了REPLRead-Eval-Print-Loop环境类似于Haskell的ghci界面所有的命令可以通过输入:?来查看。我们先了解以下几个命令即可:?、:h或:help显示所有命令:t或:type检查变量的类型:q或:quit退出REPL:c或:compile编译为可执行文件:l或:load加载文件:r或:reload重新加载当前文件如下面的操作序列Main:lhello.idrLoadedfilehello.idr Main:r Loadedfilehello.idr Main:t main Main.main:IO()Main:c hello main File build/exec/hello written Main:q Byefornow!编译运行代码这是Idris 2的hello world代码文件名是hello.idrmoduleMainmain:IO()mainputStrLnHello world编译代码比较简单$ idris2 hello.idr-ohello运行代码$ ./build/exec/hello Hello world编译后会生成一系列目录和文件build/ ├── exec │ ├── hello │ └── hello_app │ ├── compileChez │ ├── hello.so │ ├── hello.ss │ └── libidris2_support.so └── ttc └── 2025081600 ├── hello.ttc └── hello.ttm现阶段不用太多关注知道以下几点就够了build/exec— 跟程序执行有关的文件放在该目录build/exec/hello— “可执行文件”实际上它就是个shell或bat脚本调用了hello.so。build/ttc/— 类型检查结果放在该目录