Error: Cannot find library D in loadpath

HanInSeoung commented 8 years ago

P01.v를 IDE로 실행하자 제목의 에러문구가 뜹니다. loadpath를 어디서 어떻게 설정해야하나요?

taehwoi commented 8 years ago

make를 먼저 한번 실행한 다음 P01.v를 실행하시면 아마 될거에요.

HanInSeoung commented 8 years ago

우와아 감사합니다 .. 어떻게 아셨나요 !!

taehwoi commented 8 years ago

저도 비슷한 증상을 겪어서 이것저것 해보다가 알게됐네요 ㅋㅋ 해결 하셨다니 다행입니다.

HanInSeoung commented 8 years ago

그러면 혹시 P02.v에서 Error: Compiled library D.vo makes inconsistent assumptions over library Coq.Init.Notations는 어떻게 해결하셨나요?..

taehwoi commented 8 years ago

글쎄요 저는 그런 에러는 못 봤네요. 근데 예전에 ocaml에서 비슷한 오류가 foo.ml를 컴파일한 ocaml의 버젼과 현재 실행하는 ocaml의 버젼이 달라서 생긴 적이 있는데 혹시 coq를 컴파일 하는데 사용된 ocaml의 버젼이랑 make에서 실행한 ocaml(이나 coq)의 버젼이 다른 게 아닐까요?

jeehoonkang commented 8 years ago

@indiofish IDE로 실행하기 전에 make하라는 내용을 README에 넣었습니다. 감사합니다.
@HanInSeoung
- coqc --version 하면 어떻게 나오나요?
- 쓰시는 IDE 종류 및 버전은 무엇인가요?
- make clean; make 한 번 해보시겠어요?

HanInSeoung commented 8 years ago

<버전> The Coq Proof Assistant, version 8.4pl6 (October 2015) compiled on Oct 12 2015 11:33:44 with OCaml 4.02.3

CoqIDE_8.4pl5입니다. 역시 같은 오류가 발생합니다 ㅜ

jeehoonkang commented 8 years ago

제 생각에, 터미널에서는 버전이 8.4pl6이고, CoqIDE에서는 버전이 8.4pl5라서 생기는 오류인 것 같습니다.
터미널에서 PATH를 설정해서 8.4pl5가 실행되도록 고치시면 잘 되리라 생각합니다.

HanInSeoung commented 8 years ago

PATH는 어떻게 설정하나요?

jeehoonkang commented 8 years ago

https://github.com/snu-sf-class/pl2016#coq "Add the directory that contains Coq binaries in the PATH variable."

HanInSeoung commented 8 years ago

아래 경로를 nano ~/.bashrc해서 만들어서 추가했는데 여전히 버전이 8.4pl6으로 나와요;; export PATH=$PATH:/Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/ 제가 경로를 올바르게 설정한게 맞나요??

taehwoi commented 8 years ago

주소:$PATH 이런 식으로 해야 8.4.pl5를 우선 실행할 것 같습니다.

HanInSeoung commented 8 years ago

아 .bashrc말고 .bash_profile에서 주소를 추가하니까 되네요 ㅎㅎ 감사합니다! 해결되었습니다.

snu-sf-class / pl2016

Error: Cannot find library D in loadpath #25