[Searching for program: no such file or directory, coqtop] OSX에서 emacs 오류

[HanInSeoung]

설치방법대로 emacs를 맥에 깔아서 course/C20160303.v 파일을 시험삼아 컴파일 해봤는데..

Searching for program: no such file or directory, coqtop이라는 오류때문에 자꾸 컴파일이 안됩니다.

음.. coqtop이 보니까 /Applications/CoqIdE_8.4pl5.app/Resources/bin/ 위치에 있는거 같아서

.bash_profile에 export PATH=/Applications/CoqIdE_8.4pl5.app/Resources/bin/:$PATH라고 환경변수를 맨 아래에 추가해 줬는데도 계속 같은 오류가 뜹니다 ㅜㅠ

어떻게 해야할까요?;;

[swchoi06]

Though it is ok to use coqtop installed with CoqIDE, if you want to use emacs as a editor I think it's better to install Coq with Homebrew.

Try brew install coq

If brew command doesn't work, check http://brew.sh/index_ko.html and install Homebrew first.

[Ailrun]

Emacs 실행 Path가 따로 있습니다, 올바른 path를 exec-path라는 변수에 저장하시면 됩니다

[jeehoonkang]

문제가 여전히 남아있나요?

[HanInSeoung]

네.. 그냥 부트캠프로 리눅스 깔아서 하려했다가 귀찮아서 포기하고 그냥 기본 IDE를 쓰고있습니다 ㅜ ㅋㅋ

[jeehoonkang]

Try (custom-set-variables '(coq-prog-name "PATH/TO/coqtop") '(proof-three-window-enable t)) in .emacs: http://superuser.com/questions/771442/configuring-proof-general-for-coq-in-emacs