在 Agda hello-world 中运行时未解析的元数据

Question

我尝试使用Agda 2.6.1.3和Agda stdlib 1.5编译hello-world示例。下面是代码：

module hello-world where

open import IO

main = run (putStrLn "Hello, World!")

用Agda( agda --compile hello-world.agda)编译时，报如下错误：

Unsolved metas at the following locations:
  $HOME/hello-world.agda:5,8-11

报告的位置 ( 5,8-11) 对应于 token run。

我在 Agda 和 Agda-stdlib Issues 中都没有找到任何相关信息，在 SO 或其他网站上也没有找到任何相关信息。文档是否已过时，或者我是否犯了任何错误？

---

笔记：

• Agda 编译器是通过stack install Agda解析器安装的lts-17.5。
• 我还尝试从 GitHub 源（分支）手动编译release-2.6.1.3。
• 在$HOME/.agda/libraries我有：

  $HOME/agda-stdlib/standard-library.agda-lib
  

• 在$HOME/.agda/defaults我有：

  standard-library
  

Answer 1

这是https://github.com/agda/agda/issues/4250#issuecomment-771806949的评论中描述的问题。当前的解决方法是添加一个隐式参数，run如下所示：

\n

module hello-world where\n\nopen import IO\nopen import Level\n\nmain = run {0\xe2\x84\x93} (putStrLn "Hello, World!")\n

\n

此问题将在即将发布的 Agda 2.6.2 和下一版本的标准库中得到修复。

\n