For those unable to compile Assignment 08_00 in Coq Ide...

[AdamBJ]

In Coq IDE when I selected the compile option for Assignment08_00 the program froze. For others having this problem, I was able to get around it by compiling 00 using Gitbash and make clean; make.

[jeehoonkang]

Thank you for a great advice! I couldn't reproduce your issue, so I think your advice will be the only reasonable one.

[alkaza]

I couldn't resolve this problem with make Assignment08_00.v, what should I do?

On Sat, May 16, 2015 at 4:35 PM, Jeehoon Kang notifications@github.com wrote:

Thank you for a great advice! I couldn't reproduce your issue, so I think your advice will be the only reasonable one.

— Reply to this email directly or view it on GitHub https://github.com/snu-sf/pl2015/issues/99#issuecomment-102584377.

[jeehoonkang]

@alkaza

• I think @AdamBJ 's advice is reasonable and worth to follow. Did you try? Which result you got?
• beyond this, did you try making source files in other ways?

Jeehoon

[AdamBJ]

@alkaza I didn't try to specifically make ..._00, I first wiped everything with make clean then built everything from scratch with make. It takes awhile to execute, but it worked for me.

[qkr0990]

how can i complile in git bash...would you please..?? Thanks

[jeehoonkang]

@qkr0990 I would like to share a lyrics I like: "With love and strength for each new day / we will make a way, we will make a way"

[jaewooklee93]

I guess that freezing phenomenon of CoqIde when trying to make is actually a normal thing. If you wait for enough time (maybe several minutes) then it may work properly. It seems that CoqIde is not implemented as a multi-threaded program, so during the long compile, the whole program goes to freeze.

[AdamBJ]

@qkr0990 If you're using Windows you can check out issue #68 for how to get make working with git bash.

[LeeGyeongGeon]

I tried all the things referenced above. But executing coqc in gitshell says:

File "/home/csehome/crusaderlee/pl/sf/Assignment08_00.v", line 2, characters 0-21: Error: Compiled library SfLib.vo makes inconsistent assumptions over library Coq.Init.Tactics

How can I solve this problem? Would you guys give me a solution?

[alkaza]

For me, when I compile it in CoqIDE, it freezes and nothing happens when i do make clean. I let it "think" for some time (almost a day) and nothing happened. Please help!

[AdamBJ]

@alkaza i can try doing what worked for me on your PC if you bring it to class today

[jaewooklee93]

@alkaza Sorry, I haven't found any problem on Ubuntu Linux, but it seems that Windows version of CoqIde has a real problem.

[LeeGyeongGeon]

I tried again in martini.snu.ac.kr, not in my Win7 environment, and I found that there happens no problem at all. It seems clear that we should not use Windows environment when doing Software Foundations homework..

[ksami]

I have no problems with make on Windows 8 using cygwin.

[alkaza]

So I managed to make clean and make using cygwin, but when I try to run Assignment08_01, I get Error: Cannot find library Assignment08_00 in loadpath. What should I do?

[jeehoonkang]

@alkaza Does your sf directory contain Assignment08_00.vo?

[alkaza]

Only Assignment08_00.glob Assignment08_00.vo wasn't made :(

[jeehoonkang]

@alkaza That means your make fails to compile Assignment08_00.v. Would you please paste the error message of make?

[alkaza]

$ make Assignment08_00.v
make: *** No rule to make target `Assignment08_00.v'.  Stop.

[jeehoonkang]

Do make Assignment08_00.vo.

[alkaza]

$ make Assignment08_00.vo
make: *** No rule to make target `Assignment08_00.vo'.  Stop.

[jeehoonkang]

I think your Makefile is bad.

• What is the current directory?
• What is your Makefile? Is it the same with the one in the snu-sf/pl2015's master? If not, would you please paste it in http://gist.github.com ?

[alkaza]

It should not be different https://gist.github.com/alkaza/4d6a3e6b5097a44fcd30 Worked till now...

[alkaza]

Oh I see it now

[jeehoonkang]

Use this: https://github.com/snu-sf/pl2015/blob/master/sf/Makefile You can find that Assignment08_??.v is not in the $VFILES in your Makefile.

[alkaza]

I changed Makefile but still

$ make Assignment08_00.vo
make: *** No rule to make target `Assignment08_00.vo'.  Stop.

[jeehoonkang]

@alkaza Would you please zip your development and email me?

[alkaza]

I couldn't get any results by using cygwin, but I managed to succeed by using make clean and make in cmd. So now I have Assignment08_00.vo. But when I try to run Assignment08_01.v, I get

Error: Compiled library Assignment08_00.vo makes inconsistent assumptions
over library Coq.Init.Datatypes

[jeehoonkang]

@alkaza I guess you have multiple installation of Coq. Can you check it?

[alkaza]

It doesn't seem like it.

[jeehoonkang]

Please zip and mail your development.

[alkaza]

You mean the whole sf folder?

[jeehoonkang]

@alkaza yes.

[AdamBJ]

@alkaza if what you're doing with Jeehoon doesn't work and you want me to send you my 09_00 let me know

[alkaza]

@jeehoonkang I sent it @AdamBJ I seem to have a different problem now :( no idea what's going on

[AdamBJ]

@alkaza Ok, that's too bad:( Hope you can work it out

[jeehoonkang]

@alkaza I saw your email, and it seems I cannot figure out your problem with only development files. Would you please come to my office tomorrow to figure out what's going on in your machine? Thanks.

[alkaza]

@jeehoonkang Are you available at 2PM?

[jeehoonkang]

@alkaza LGTM see you tomorrow.

[alkaza]

@jeehoonkang Thank you!

[alkaza]

@jeehoobkang I came to your office (301-554-1) but door is closed and no one responds to knocking

[jeehoonkang]

cuz we are on a evacuation exercise. I will be back in 20 minutes.

[jaewooklee93]

How about distributing object file of 00?

[jeehoonkang]

@jaewooklee93 I think that's a good idea. I believe Windows machines can share the object file. Would somebody who uses Windows please upload Assignment08_00.vo so that everybody can download and use it?

[AdamBJ]

https://www.dropbox.com/s/q1gwxeslgdrc18s/Assignment08_00.vo?dl=0