Agda: Не удается найти std-lib при установке с помощью стека

Question

Я пытаюсь скомпилировать файл Agda, но у меня не получается найти стандартную библиотеку. Я видел документацию здесь.

Я использовал Stack для его установки:

> which agda
/home/joey/.local/bin/agda

И я установил переменную окружения для моего каталога Agda:

> echo $AGDA_DIR
/home/joey/.agda

Который заполнен правильными файлами:

/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/libraries
/home/joey/agda/agda-stdlib/standard-library.agda-lib

> cat "$AGDA_DIR"/defaults
standard-library

> cat /home/joey/agda/agda-stdlib/standard-library.agda-lib
name: standard-library
include: src

Однако, когда я иду к компиляции файла Agda, я получаю следующую ошибку:

Failed to find source of module Function in any of the following
locations:
  /home/joey/agda/AutoInAgda/src/Function.agda
  /home/joey/agda/AutoInAgda/src/Function.lagda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.agda
  /home/joey/.stack/snapshots/x86_64-linux-nopie/lts-8.14/8.0.2/share/x86_64-linux-ghc-8.0.2/Agda-2.5.2/lib/prim/Function.lagda
when scope checking the declaration
  open import Function

Как я могу сказать Агде, где искать стандартную библиотеку? Это проблема из-за стека?

Я на Ubuntu 17.10, если это имеет значение.

Answer 1

Оказывается, если у вас есть корневой файл.agda-lib в корневом каталоге, он полностью игнорирует файл по умолчанию. Таким образом, ключ должен был включить standard-library явно в этом файле.

Глупая вещь для меня, чтобы пропустить, но, надеюсь, другие с такой же проблемой найдут этот ответ.

Answer 2

Для всех, у кого есть эта проблема, это решается добавлением следующей строки в ваш файл .agda-lib:

      depend: standard-library