Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

How can we import beq_nat from Basics.v #43

Closed
jaewooklee93 opened this issue Mar 27, 2015 · 10 comments
Closed

How can we import beq_nat from Basics.v #43

jaewooklee93 opened this issue Mar 27, 2015 · 10 comments

Comments

@jaewooklee93
Copy link

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
Copy link
Contributor

Do you have Basics.vo file in the directory?

@jaewooklee93
Copy link
Author

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
Copy link
Contributor

  • 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
Copy link
Author

After make, git status gave the following.

screenshot from 2015-03-27 21 47 24

@jeehoonkang
Copy link
Contributor

  • 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
Copy link
Author

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
Copy link
Contributor

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
Copy link
Author

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
Copy link
Contributor

@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
Copy link
Author

Thank you for your great caring.

Jaewook Lee

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants