Open isutare412 opened 8 years ago
The same error occurred to me, so I updated the assignment 01. Would you please re-pull (or re-download) and try again?
@jeehoonkang
After going through the same error, I did make
then it worked. Is there any major change which may effect evaluation? Cause I already submitted my assignment yesterday.
@lsc2687 if the server says you got 50 pts, then that's fine. If not, you can just resubmit.
It was due to an error in Makefile
. In assignment 02 it wouldn't happen.
Does this problem still happen? @lsc2687
@aqjune Just same error happens when I run with the assingment02 that I just pulled....
Would you please try make
and open CoqIDE again?
@aqjune
I pulled the repository and did make clean
and make
again.
Even after this, CoqIDE still cannot run the code....
May I go to the lab with my laptop tomorrow?
@isutare412 Sure. you can visit here (301-416) at 4:00 pm ~ 6:00 pm
The problem was that CoqIde ignored options defined in _CoqProject by default. To solve this problem, go to Edit -> Preferences and change option 'ignored' into 'taken instead of arguments'.
@aqjune thank you so much for your hard work.
The error occurs like this when I load homework on a CoqIDE and try to proceed forward.
Error: The file /Users/LSH/Coding/SNU_files/Program_Languages/pl201602/assignments/01/D.vo contains library Assignment.D and not library D
My develop environment is macOS and I installed CoqIDE_8.5pl2 by binary file from the link. I don't understand why this error occurs.... I cannot find solution even if I googled it.