Предотвращение того, чтобы разработка 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

Как отмечалось в описании стандартной библиотеки, вам необходимо использовать experimental ветка библиотеки, если вы работаете с masterфилиал Агды. Вы можете получить его, клонировав репозиторий github по адресу https://github.com/agda/agda-stdlib и делаю git checkout experimental.

Для автоматического переключения между версиями библиотек при переключении версий Agda вы можете иметь несколько librariesфайлы, как описано в руководстве пользователя:

Чтобы Agda нашла файл библиотеки, он должен быть указан (с полным путем) в файле библиотеки.

AGDA_DIR/libraries-VERSION, или, если он не существует, AGDA_DIR / libraries

где ВЕРСИЯ - это версия Agda (например, 2.5.1). AGDA_DIR по умолчанию имеет значение ~/.agda в unix-подобных системах и C:\Users\USERNAME\AppData\Roaming\agda или подобное в Windows, и его можно изменить, установив переменную среды AGDA_DIR.

В качестве альтернативы вы можете иметь один libraries файл и проверьте правильную версию библиотеки при переключении версий Agda.