Agda : 스택과 함께 설치할 때 std-lib를 찾을 수 없습니다.

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

표준 라이브러리를 어디에서 찾을 수 있습니까? Stack 때문에이 문제가 있습니까?

나는 우분투 17.10을 사용하고 있습니다.

출처

2017-10-27 jmite

명시 적으로'--library = standard-library'를 명령 행 옵션으로 전달하면 어떻게됩니까? – gallais

@gallais 추가 할 때 오류가 발생합니다.'최상위 모듈의 이름이 파일 이름과 일치하지 않습니다. 모듈 자동은 다음 파일 중 하나에 정의해야합니다. /home/joey/agda/agda-stdlib/src/Auto.agda '. 표준 라이브러리 대신 내 프로젝트를 표준 라이브러리로 취급하려는 것 같습니다. – jmite

오 그렇지만 이제는 표준 라이브러리의 위치를 알고있는 것 같습니다! 나는'-i .' ('Auto.agda '가 프로젝트의 루트에 실제로 존재한다면)를 추가하는 것이 효과가 있다고 생각한다. 나는 디폴트의 문제가 무엇인지 모르지만'~/.agda/libraries'의 이름을'~/.agda/libraries-VERSIONNUMBER'로 바꾸고 싶을 수도 있습니다. – gallais

루트 디렉토리에 .agda-lib 파일이 있으면 기본값 파일을 완전히 무시합니다. 따라서 핵심은 해당 파일에 standard-library을 명시 적으로 포함시키는 것이 었습니다.

내가보기에 멍청한 일이지만, 같은 문제가있는 다른 사람들이이 대답을 찾을 수 있기를 바랍니다.

출처

2017-10-31 21:15:14 jmite

Agda : 스택과 함께 설치할 때 std-lib를 찾을 수 없습니다.

답변

관련 문제