search

vellvm / vellvm-legacy

33 stars 1 forks source link

Remove Coq-Equations plugin dependency #4

Open dgarbuzov opened 10 years ago

dgarbuzov commented 10 years ago

Requiring the Coq-Equations plugin substantially complicates the build process by introducing a dependency on the version of OCaml and camlp4. It is also only used in a single file, the patched Values.v from compcert, and it's unclear why it's really necessary. It shouldn't be too difficult to remove.

jeehoonkang commented 10 years ago

I agree with you in removing dependency to Coq-Equations, but in a slightly different reason. I would like to use ssreflect library developed by George Gonthier. However, ssreflect can be compiled only if Coq is compiled with camlp5. Thus I would like to remove dependency to camlp4, that also means removing dependency to Coq-Equations.

catalin-hritcu commented 8 years ago

Has there been any progress on removing this dependency? Wanted to have a quick look, but I've already wasted hours making the original SoftBound to compile ... out of time to kill for now.

Zdancewic commented 8 years ago

Sorry, we haven't found the time to do that yet!