search

snu-sf-class / pl201602

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

숙제 2를 제출하는데, 숙제 서버에서 P10.v 에 문제가 발생합니다. #20

Open sangjaekang opened 8 years ago

sangjaekang commented 8 years ago

저의 로컬 컴퓨터에서 coqide로 디버그했을 때는 P10.v는 성공적으로 통과되는데, 숙제 제출하면 compile error가 발생합니다 어떻게 하면 해결할 수 있을까요? 제 coq의 version은 coqc : 8.4pl3 Ocaml 4.01.0 입니다.

jeehoonkang commented 8 years ago

Coq 8.5pl2를 쓰세요.

DE-Kim commented 8 years ago

안녕하세요, 저도 과제 2의 10번에서 같은 문제가 발생합니다. coqide와 make, make eval 모두 아무 문제 없었으나, 과제를 제출하고 나면 compile error가 발생합니다. 저는 coq 8.5.2 [4.03.0]을 사용하고 있습니다. 만약 문제를 해결하셨으면, 조언 부탁드립니다.

soochan-lee commented 8 years ago

저는 다른 문제에서 같은 증상이 있었는데 이전 문제에서 제가 따로 정의한 lemma를 사용해서 그런 거였더군요. 한번 확인해보세요.

jeehoonkang commented 8 years ago

What's the error message?

DE-Kim commented 8 years ago

The problem got solved. It occurred because there was no definition of rev function which was included in distr_rev, the problem function. (I thought.) Thank you for your help.