I'm following the logic foundation preface and just began learning. I tried to use the docker with vscoq like the suggested in the book but it didn't work for me and kept asking me to install coq again, so I installed it using opam but then I had this error:

Cannot find a physical path bound to logical path ImpCEvalFun with prefix LF

If anybody could help I tried to fix it all night yesterday.

  • $\begingroup$ Is the error message the title of your question, by any chance? $\endgroup$ Oct 29, 2023 at 8:33
  • $\begingroup$ yes it is if you could help me I still didn't find a solution $\endgroup$ Oct 29, 2023 at 20:20
  • $\begingroup$ That error means that the file ImpCEvalFun.vo can't be found. That's the compiled version of the ImpCEvalFun.v file. That is one of the last chapters of Logic Foundations though. Can you interact with Basics.v as expected? What about with Induction.v? That is where the book explains how to compile files. If my comment is not helpful, please update your question with information about what exactly you did before obtaining the error message. $\endgroup$
    – Ana Borges
    Oct 31, 2023 at 14:55


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.