search

snu-sf-class / pl201602

SNU 2016 Fall 4190.310 Programming Language
22 stars 10 forks source link

coq path 문제. (make 실행시) #14

Closed choigyumin closed 8 years ago

choigyumin commented 8 years ago

zshrc 에 환경변수는 추가를 해주었습니다. coqmake 등이 들어있는 경로로... 그런데 make eval 이나 make clean 명령어를 실행할때 아래와 같은 메세지가 나오네요. 혹시 맥북을 사용하시는 분들 중 아래와 같은 증상을 겪으신 분 안계신가요? PATH 설정이 잘못된 건가 싶기도 하네요..아시는 분 답변 부탁드립니다.

(echo -R . Assignment D.v P01.v P02.v P03.v P04.v P05.v E01_01.v E02_01.v E03_01.v E04_01.v E05_01.v) > _CoqProject coq_makefile -f _CoqProject -o Makefile.coq make: coq_makefile: No such file or directory make: *\ [Makefile.coq] Error 1

jeehoonkang commented 8 years ago

다음 커맨드 결과는 무엇인가오?

which coq_makefile echo $PATH

choigyumin commented 8 years ago

순서대로

coq_makefile not found

/Applications/CoqIDE_8.4pl5.app/Contents/Resources/bin/:/Users/choigyumin/bin:/usr/local/bin:/Users/choigyumin/bin:/usr/local/bin:/Library/Frameworks/Python.framework/Versions/3.5/bin:/usr/local/bin:/usr/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/opt/local/bin:/opt/local/sbin:/Library/Frameworks/Mono.framework/Versions/Current/Commands:/Library/TeX/texbin

입니다.

Gyumin Choi 최규민 Seoul National University - Statistics, CS +82 10 5195 2047 / choigyumin@gmail.com

      1. 오후 8:38, Jeehoon Kang notifications@github.com 작성:

echo $PATH

jeehoonkang commented 8 years ago

일단 coq 8.5pl2를 깔고 다시 해보길 바랍니다.

choigyumin commented 8 years ago

설치는 되어있는 것 같습니다..삭제하고 다시 설치하라는 말씀이신가요? https://github.com/snu-sf-class/pl2016/issues/15 https://github.com/snu-sf-class/pl2016/issues/15 환경변수 문제인것 같아서 위의 이슈를 참고하여 bash_profile을 수정하였습니다.

직접 경로로 들어가보면 coq_makefile 이 있는 것은 확인했는데, 커맨드창에서 입력시에 안되는 것 같습니다...

Gyumin Choi 최규민 Seoul National University - Statistics, CS +82 10 5195 2047 / choigyumin@gmail.com

      1. 오후 8:43, Jeehoon Kang notifications@github.com 작성:

일단 coq 8.5pl2를 깔고 다시 해보길 바랍니다.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/snu-sf-class/pl201602/issues/14#issuecomment-250967227, or mute the thread https://github.com/notifications/unsubscribe-auth/ANb6JWBwaMAspsUfhTtErCb12dtNFm3rks5qv5jIgaJpZM4KL_KL.

choigyumin commented 8 years ago

방금 문제가 해결되었습니다.

경로 설정할때 오타 였던 것으로 확인되었습니다.. 귀찮게 해드려서 죄송합니다…ㅠ ㅠ yumin Choi 최규민 Seoul National University - Statistics, CS +82 10 5195 2047 / choigyumin@gmail.com

      1. 오후 8:45, Gyumin Choi choigyumin@gmail.com 작성:

<스크린샷 2016-10-02 오후 8.43.55.png>

설치는 되어있는 것 같습니다..삭제하고 다시 설치하라는 말씀이신가요? https://github.com/snu-sf-class/pl2016/issues/15 https://github.com/snu-sf-class/pl2016/issues/15 환경변수 문제인것 같아서 위의 이슈를 참고하여 bash_profile을 수정하였습니다.

직접 경로로 들어가보면 coq_makefile 이 있는 것은 확인했는데, 커맨드창에서 입력시에 안되는 것 같습니다...

Gyumin Choi 최규민 Seoul National University - Statistics, CS +82 10 5195 2047 / choigyumin@gmail.com mailto:choigyumin@gmail.com

      1. 오후 8:43, Jeehoon Kang <notifications@github.com mailto:notifications@github.com> 작성:

일단 coq 8.5pl2를 깔고 다시 해보길 바랍니다.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/snu-sf-class/pl201602/issues/14#issuecomment-250967227, or mute the thread https://github.com/notifications/unsubscribe-auth/ANb6JWBwaMAspsUfhTtErCb12dtNFm3rks5qv5jIgaJpZM4KL_KL.

Ashtroid commented 8 years ago

Could anyone please explain the solution to the Error 127 (coq_makefile: Command not found) in English?

han-minhee commented 8 years ago

His problem was because of just some typos. And TA recommended reinstallation of coq as a solution.

Ashtroid commented 8 years ago

Thanks!