3
Agdaファイルをコンパイルしようとしていますが、標準ライブラリを見つけることができません。私は文書hereを見ました。Agda：スタックでインストールするときにstd-libを見つけることができません
私はそれをインストールするために、スタックを使用しました：
> 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
標準ライブラリを探す場所をAgdaに教えるにはどうすればよいですか？スタックのせいでこれは問題ですか？
私はUbuntu 17.10を使用しています。
明示的に '--library = standard-library'をコマンドラインオプションとして渡すとどうなりますか？ – gallais
@gallaisこれを追加すると、エラーが表示されます。 '最上位モジュールの名前がファイル名と一致しません。 モジュールAutoは、 /home/joey/agda/agda-stdlib/src/Auto.agda 'のいずれかのファイルで定義する必要があります。標準ライブラリではなく、標準ライブラリとしてプロジェクトを扱おうとしているようですが、 – jmite
ああ、今は 'standard-library'の場所が分かりました。私は追加の '-i .'（' Auto.agda'が実際にプロジェクトの根源にある場合）を投げ入れることでそれを有効にするべきだと思います。私はデフォルトの問題は何か分かりませんが、 '〜/ .agda/libraries'の名前を'〜/ .agda/libraries-VERSIONNUMBER'に変更したいかもしれません。 – gallais