Had a very odd bug today while installing Prover9. Figured I'd record it for my (and maybe others') future reference. (The current version as of this writing is 2011-11A; at least one older version had the same behavior on my machine.)
Background: I'm messing around currently on a lightweight Linux called Puppy. Like most (all?) flavors of Linux, one is encouraged, when adding software, to compile it from source when possible. I've used gcc, the out-of-the-box GNU compiler, to compile a couple of little C++ exercises; but not until today had I decided to compile anything nontrivial.
Prover9 is designed to be downloaded as a tarball, unpacked, and then compiled without requiring any smarts on the part of the user. The unpacking was easy.
The process of compilation was supposed to be accomplished by simply giving the command
Much to my frustration, after a big bunch of output lines had scrolled across my terminal, make halted and caught fire. The topmost error in the stack, as much headscratching finally elucidated, was
Google sent me to this Stackoverflow question, which was thankfully not voted down (though a few people apparently tried). I still don't quite understand the details: basically, older versions of C core libraries don't come with certain obvious functions (in this case, round and ceil), and getting the compiler to pull in appropriate definitions for these functions requires issuing some extra instructions.
What's interesting is that the author of the compile (make) script issued (one version of) these extra instructions. If you unpack the archive and open up /path/to/archive/LADR-2009-11A/provers.src/Makefile, you will see at line 66
The user can of course go into a text editor and manually edit Makefile so that -lm follows $(OBJECTS) (separated by a space on both sides). This worked for me: compilation completed successfully and all three included tests passed.
Background: I'm messing around currently on a lightweight Linux called Puppy. Like most (all?) flavors of Linux, one is encouraged, when adding software, to compile it from source when possible. I've used gcc, the out-of-the-box GNU compiler, to compile a couple of little C++ exercises; but not until today had I decided to compile anything nontrivial.
Prover9 is designed to be downloaded as a tarball, unpacked, and then compiled without requiring any smarts on the part of the user. The unpacking was easy.
The process of compilation was supposed to be accomplished by simply giving the command
make allto the shell. Now, keep in mind that at the start of this process I have only the slightest idea what is supposed to happen when I issue this command.
Much to my frustration, after a big bunch of output lines had scrolled across my terminal, make halted and caught fire. The topmost error in the stack, as much headscratching finally elucidated, was
undefined reference to roundwhile gcc was trying to compile one of the C sources.
Google sent me to this Stackoverflow question, which was thankfully not voted down (though a few people apparently tried). I still don't quite understand the details: basically, older versions of C core libraries don't come with certain obvious functions (in this case, round and ceil), and getting the compiler to pull in appropriate definitions for these functions requires issuing some extra instructions.
What's interesting is that the author of the compile (make) script issued (one version of) these extra instructions. If you unpack the archive and open up /path/to/archive/LADR-2009-11A/provers.src/Makefile, you will see at line 66
prover9: prover9.o $(OBJECTS)
$(CC) $(CFLAGS) -lm -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a
The part that I'm interested in is the -lm instruction flag. It basically is needed in the course of linking libraries (like the math library containing round). However, my version of gcc wants this flag to be at the end of the line -- it complains (and more importantly, compilation halts and catches fire) with the flag in its current location.The user can of course go into a text editor and manually edit Makefile so that -lm follows $(OBJECTS) (separated by a space on both sides). This worked for me: compilation completed successfully and all three included tests passed.
I've tried every syntax I can think of and still no luck. How did you write that line 66 exactly??
ReplyDelete