search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Error building base. #123

Open DavidFHCh opened 5 years ago

DavidFHCh commented 5 years ago

When building the base library I get this error, I've followed the instructions of the README.md, any idea on how to make this work? I paste the output of the make command... Thanks.

$ make -C base make: Entering directory '/home/davidf/Documents/hstocoq/hs-to-coq/base' COQC GHC/List.v File "./GHC/List.v", line 191, characters 0-322: Warning: Implicit arguments declaration relies on type. The term declares more implicits than the type here. [implicits-in-term,implicits] File "./GHC/List.v", line 200, characters 0-317: Warning: Implicit arguments declaration relies on type. The term declares more implicits than the type here. [implicits-in-term,implicits] File "./GHC/List.v", line 229, characters 23-33: Error: No interpretation for string "Prelude.".

make[1]: [Makefile:663: GHC/List.vo] Error 1 make: [Makefile:327: all] Error 2 make: Leaving directory '/home/davidf/Documents/hstocoq/hs-to-coq/base'

sweirich commented 5 years ago

Which version of Coq are you using? Did you install ssreflect? (You can ignore the warnings, the issue that is interfering with compilation is the string "Prelude." in the file.)

DavidFHCh commented 5 years ago

My Coq version is 8.9.0, yes, I did all the steps using opam.

<><> coq-mathcomp-ssreflect: information on all versions ><><><><><><><><><><><> name coq-mathcomp-ssreflect all-installed-versions 1.8.0 [default] all-versions 1.6 1.6.1 1.6.2 1.6.4 1.7.0 1.8.0