Vellvm Installation

[sepehram]

I have tried to install the earlier version of the package from http://www.cis.upenn.edu/~stevez/vellvm/release.tgz, using "Dependencies" from README file, on an Ubuntu 14.04 machine.
But I get error message, when I try to compile Float from extralib directory.
~/release/vol/extralibs/Float$ make
coqc -dump-glob Faux.glob -q -I . -I ./Ct2 -I ./Expansions -I ./FnElem -I ./Others Faux
File "./Faux.v", line 314, characters 8-39:
Error: Illegal application (Non-functional construction):
The expression "(p1 ?= q1)%positive" of type "comparison"
cannot be applied to the term
"Eq" : "comparison"
make: *** [Faux.vo] Error 1

Moreover, I am a bit confused about the version of LLVM to be installed in further steps. The README file residing in release.tgz suggests LLVM 2.6, but the link is unreachable. On the other hand, http://www.cis.upenn.edu/~stevez/vellvm/README.txt suggests LLVM 3.0. In this regard, I tried to download and install LLVM 3.0 from http://llvm.org/releases/3.0/llvm-3.0.tar.gz. I was able to compile the code with minor modifications, but still have problems installing it.

I'd be very grateful if you let me know whether there exists any later versions of Vellvm and accompanying LLVM that I can install more straightforwardly.

[dgarbuzov]

Yes, the version of Vellvm in this repository is newer and should be easier to get started with. However, it's incomplete and needs some more work to make it possible to extract LLVM passes with newer versions of LLVM/Coq.

If you need to be able to extract and run Vellvm passes and have to use the version in release.tgz:

1. I'm not sure the Floats plugin is actually necessary, you can try compiling without it
2. You should be using LLVM 3.0

Hope that helps!