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

examples/successors make error #47

Closed aogrcs closed 6 years ago

aogrcs commented 6 years ago

*** No rule to make target '../../base/GHC/Base.vo', needed by 'Control/Applicative/Successors.vo'.

lastland commented 6 years ago

Hi, you will need to run make in base first. Can you try, for example, make -C ../../base (or just cd to base, and then make)?

aogrcs commented 6 years ago

I cd to base then I make, but I said that could not find ssreflect

sweirich commented 6 years ago

Sorry about that. I just updated the toplevel README.md file with instructions to install ssreflect.

aogrcs commented 6 years ago

Just "opam install coq-mathcomp-ssreflect.1.6.1" worked, "opam install coq.8.6 coq-mathcomp-ssreflect.1.6.1" did not work, maybe caused by the opam source or the network. I also found the link https://stackoverflow.com/questions/43955082/how-to-install-ssreflect-and-mathcomp-in-linux# It did not set the coq version and installed coq 8.7, neither did it. Thanks for your patient!

sweirich commented 6 years ago

Were you able to get it work?

aogrcs commented 6 years ago

Yes, it did work, thanks

sweirich commented 6 years ago

Ok, closing issue. Let us know if you have other questions!