Building on Windows
aa755 opened this issue · 3 comments
Earlier, I had compiled c-corn on Ubuntu and everything worked perfectly.
Today, I tried to build c-corn on windows and ran into some issues. The scons system was trying to compile a .v file before compiling its dependencies. I guess the supplied SConstruct file is not designed to work natively on Windows? If so, should the README instruct folks running Windows to use Cygwin?
Indeed, the scons problem was solved by using cygwin, i.e. installing python and scons in cygwin and then running scons in the cygwin terminal.
Also, I ran into some filename case-insensitivity issues on windows: https://coq.inria.fr/bugs/show_bug.cgi?id=2554. I fixed some of them. Even the MathClass repository needs to be fixed. I'll create a pull request as soon as I do that.
Also, coqc aborts without any error message while compiling reals/faster/ARAlternatingSum.v at the
following line:
https://github.com/c-corn/corn/blob/master/reals/faster/ARAlternatingSum.v#L209
Changing 50000 to 50 fixed this problem.
Did you get this error when compiling on Windows?
coqc model\structures\QnonNeg -R . CoRN -R math-classes/src MathClasses
File "...\corn/model\structures\QnonNeg.v", line 56, characters 13-22:
Error: The reference Q.min_glb was not found in the current environment.
scons: *** [model\structures\QnonNeg.vo] Error 1
scons: building terminated because of errors.
Yes. look at aa755/corn@0eed30a
If you are building in windows, my commits might be useful for you.
I have fixed many but not all such errors.
That solves the problem! Thanks a lot!
I actually got it compiled successfully on Windows 7.
On Mon, Nov 17, 2014 at 10:26 PM, Abhishek Anand notifications@github.com
wrote:
Yes. look at aa755@0eed30a
aa755/corn@0eed30a
If you are building in windows, my commits might be useful for you.
I have fixed many but not all such errors.Reply to this email directly or view it on GitHub
#6 (comment).