Error: cannot find library D in load path

snu-sf-class / pl2016

14 stars 17 forks source link

Error: cannot find library D in load path #43

Open wonheejo opened 8 years ago

wonheejo commented 8 years ago

2번째 과제를 할려고 터미널에서 git pull을 하고 과제를 실행 하니까 Error: Cannot find library D in loadpath 문제가 생겨서 nano ~/.bash_profile 에다가 주소를 export PATH=$PATH:/Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/ 이렇게 입렵을 해도 which coqc 치면 위치는 계속 /usr/local/bin/coqc 이렇게 뜹니다 .. ㅜㅜ 어디서 문제인가요?

jeehoonkang commented 8 years ago

이미 설치된 다른 Coq이 있을 가능성이 있습니다. 지워보세요.

OS X에서 하신다면, 다음과 같이 입력해보세요:

export PATH=/Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/:$PATH

wonheejo commented 8 years ago

다른 Coq는 어떻게 지울 수 있나요?

wonheejo commented 8 years ago

Basics.v를 열어서 compile buffer를 하면 이런 문제가 떠요... /bin/sh: coqc: command not found.. 이거는 어떻게 해결하나요?

jeehoonkang commented 8 years ago

아.. 답이 늦어 죄송합니다. 곧 답글 달겠습니다.

jeehoonkang commented 8 years ago

아 연구실에 있구나 ㅜㅜ 주무셔서 못봤읍니다. . . !

추가: 죄송합니다. 댓글을 잘못 달았습니다..

jeehoonkang commented 8 years ago

다른 Coq은 어떻게 설치하셨는지 알아야 지울 수 있을 것 같습니다. brew로 설치하셨다면 brew remove coq이 될지도 모르겠습니다.
CoqIDE에서 compile buffer를 잘 하는 방법은 저도 잘 모르겠습니다.. Shell에서 make로 컴파일해주시기 부탁드립니다.

jeehoonkang commented 8 years ago

문제가 지속되나요?

wonheejo commented 8 years ago

고쳤습니다!! brew에서 coq 지우고 pl2016 파일도 지우고 다시 다운 받아서 깐 다음에 숙제 있는 폴더에서 make한뒤 돌리니까 잘 됬습니다

On Fri, Apr 1, 2016 at 8:56 PM, Jeehoon Kang notifications@github.com wrote:

문제가 지속되나요?

— You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub https://github.com/snu-sf-class/pl2016/issues/43#issuecomment-204367262