pirapira/dry-analyzer

Error: The implementation CoqNat.ml does not match the interface CoqNat.cmi: Values do not match: val zero : int is not included in val zero : Decimal.int File "CoqNat.mli", line 6, characters 0-14: Expected declaration File "CoqNat.ml", line 8, characters 4-8: Actual declaration Command exited with code 2. Compilation unsuccessful after building 38 targets (0 cached) in 00:00:01.

Ywmet opened this issue · 1 comments

Ywmet commented

when I make ,errors blow.Can you help me?

Error: The implementation CoqNat.ml does not match the interface CoqNat.cmi:
Values do not match:
val zero : int
is not included in
val zero : Decimal.int
File "CoqNat.mli", line 6, characters 0-14: Expected declaration
File "CoqNat.ml", line 8, characters 4-8: Actual declaration
Command exited with code 2.
Compilation unsuccessful after building 38 targets (0 cached) in 00:00:01.

I faced the same problems.
The issue here is that

opam install lwt cohttp coq getopt batteries ocamlnet

gets the most recent version of the packages and installs an second compiler for ocaml to compile that versions.
This leads to your described issue.

My solution was to install specific verison of the upper packages like

opam install lwt.2.7.1 cohttp.0.19.3 coq.8.5.2~camlp4 getopt batteries.3.5.1 ocamlnet.4.1.9-2

Finally get the analyzer to work following the next steps on the project description.