Compile error in SerializeImplement

[kmbnw]

I'm unable to compile mspack-ocaml on a 64 bit Linux Mint 13. This is the error I get:

omake: Symbol `FamErrlist' has different size in shared object, consider re-linking * omake: reading OMakefiles * omake: finished reading OMakefiles (0.04 sec)

• build proof SerializeImplement.glob
• coqc SerializeImplement.v File "./SerializeImplement.v", line 243, characters 0-26: Error: Found no subterm matching "ascii8_of_nat 0" in the current goal. * omake: 53/133 targets are up to date
  * omake: failed (10.88 sec, 0/12 scans, 9/16 rules, 17/160 digests) *\ omake: targets were not rebuilt because of errors:
  proof/SerializeImplement.glob depends on: proof/SerializeImplement.v proof/SerializeImplement.vo depends on: proof/SerializeImplement.v

I have libfindlib-ocaml 1.2.7, libfindlib-ocaml-dev 1.2.7, libextlib-ocaml 1.5.2, libextlib-ocaml-dev 1.5.2, and omake-0.9.8.5-3-8 from the Debian repositories installed.

I cloned the msgpack-ocaml github repo and ran

omake

I also tried 'omake clean' first, but that produced the same error. I'm not real familiar with OMake; any suggestions?

[jlouis]

What is your Coq version? 8.3 or 8.4? The msgpack system uses a Proof Assistant to prove that the implementation is correct and this error is from that system.

[mzp]

Coq 8.4 (September 2012) only.