How can we import beq_nat from Basics.v

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring

11 stars 6 forks source link

How can we import beq_nat from Basics.v #43

Closed jaewooklee93 closed 9 years ago

jaewooklee93 commented 9 years ago

screenshot from 2015-03-27 21 27 14

Even though Assignment03.v is located in the same folder with Basics.v, CoqIde cannot pass through Check beq_nat.

jeehoonkang commented 9 years ago

Do you have Basics.vo file in the directory?

jaewooklee93 commented 9 years ago

Okay, after make, it works fine.

Also, I guess that it is the first time that I've compiled the Coq sources, that is, I've never tried to compile Assignment01~02.v and just checked it with Coqide only. Could it be a problem? Is my submission valid until now?

And then, after I did make, I could see a large list of untracked files at git status. Do I have to git add them?

jeehoonkang commented 9 years ago

If coqide does not complain about the source code, it is very likely that coqc (used in Makefile) also does not complain about the source code. Practically, you may assume that their behaviors are the same.
Would you please give me some examples of untracked files? If they are auto-generated files, it would be better to ignore by specifying filenames in .gitignore.

jaewooklee93 commented 9 years ago

After make, git status gave the following.

screenshot from 2015-03-27 21 47 24

jeehoonkang commented 9 years ago

If you would like to post code, use Markdown's support for code snippet, or GitHub Gist.
Your status is absolutely strange. Have you pushed everything you committed to your GitHub repository? Then I will examine your repo and will give you some advice, soon (maybe before this weekend...)

jaewooklee93 commented 9 years ago

Ah, I found the reason. I did git status at /pl2015/sf above, in that position git status showed a large list like that. When I did git status at /pl2015, it seems quite fine like this.

jaewooklee@lee-pc:~/pl2015$ git status
On branch master
You have unmerged paths.
  (fix conflicts and run "git commit")

Changes to be committed:

    new file:   sf/Assignment03.v
    modified:   sf/Makefile

Unmerged paths:
  (use "git add <file>..." to mark resolution)

    both modified:      README.md

Changes not staged for commit:
  (use "git add <file>..." to update what will be committed)
  (use "git checkout -- <file>..." to discard changes in working directory)

    modified:   fetch-homework.sh
    modified:   sf/Assignment03.v

I think I've done accidently git init at pl2015/sf and I guess that is the reason of this problem.

jeehoonkang commented 9 years ago

In that case, I guess your sf directory contains its own .git directory. That is strange, since sf is not a repository on its own...

jaewooklee93 commented 9 years ago

The world of git is quite complex for me as a beginner...

But still, it seems that I successfully finished and submitted sf/Assignment03.v without any problem. Is it right?

jeehoonkang commented 9 years ago

@jaewooklee93 LGTM. Git is, in my humble opinion, the single most important software for modern software development. Thus I believe it is worth trying to learn in depth.

Jeehoon

jaewooklee93 commented 9 years ago

Thank you for your great caring.

Jaewook Lee