防止开发 agda 破坏基本标准库的使用？

Question

我正在使用 agda 的开发版本，它现在与基本标准库版本 1.3 不兼容。

wmacmil@w:~/.agda$ agda --version
Agda version 2.6.2-41b6b25

一个基本的failure.agda文件，

module failure where 

open import Data.String

失败：

Checking failure (/home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/failure.agda).
 Checking Data.String (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/String.agda).
  Checking Data.String.Base (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/String/Base.agda).
   Checking Data.List.Extrema (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/List/Extrema.agda).
    Checking Data.List.Membership.Propositional.Properties (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/List/Membership/Propositional/Properties.agda).
     Checking Data.List.Membership.Setoid.Properties (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/List/Membership/Setoid/Properties.agda).
Killed

如何运行同时使用两个版本？我如何运行 stdlib 的实验版本来避免这种情况？有人会建议其他技巧吗？

此外，声望>1500 的人是否会将 agda-stdlib 设为标签？

Answer 1

如标准库的描述中所述，如果您正在使用 Agda 的 master 分支，则需要使用该库的 experimental 分支。您可以通过在 https://github.com/agda/agda-stdlib 克隆 github 存储库并执行 git checkout experimental.

来获取它

要在切换 Agda 版本时自动切换库版本，您可以拥有多个 libraries 文件，如 user manual:

中所述

To be found by Agda a library file has to be listed (with its full path) in a libraries file

AGDA_DIR/libraries-VERSION, or if that doesn’t exist AGDA_DIR/libraries

where VERSION is the Agda version (for instance 2.5.1). The AGDA_DIR defaults to ~/.agda on unix-like systems and C:\Users\USERNAME\AppData\Roaming\agda or similar on Windows, and can be overridden by setting the AGDA_DIR environment variable.

或者，您可以拥有一个 libraries 文件，并在切换 Agda 版本时检查库的正确版本。

防止开发 agda 破坏基本标准库的使用？

Preventing development agda from breaking basic standard library usage?

agda

agda-mode

agda-stdlib