Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq/CoqIde can't find my first hello world file. Please help!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq/CoqIde can't find my first hello world file. Please help!


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Coq/CoqIde can't find my first hello world file. Please help!
  • Date: Mon, 28 Sep 2015 01:38:19 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wi0-f169.google.com
  • Ironport-phdr: 9a23:bgt8sxBBm/q/k+tgXo+MUyQJP3N1i/DPJgcQr6AfoPdwSP78rsbcNUDSrc9gkEXOFd2CrakU16yL7+u5ATRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6bvp9aKO10ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5lH/Sl6k4WJUeWELmFIcCA/cqRr+Q53Zsy3gt+M71jPMbuPsSrVhYTWv9b1mADTvlT0bNjMkuDXPi8Fqlq8dqxW8vQB+zpP8b4ScNf44daTYK4BJDVFdV9pcAnQSSri3aJECWq9YZb5V

Hello, please explain what you typed and where (terminal? inside coqide?) exactly to obtain this error.

Best regards,
Pierre

2015-09-27 2:42 GMT+02:00 Enjoys Math <enjoysmath AT gmail.com>:
Hi :)

I saved as MyTutorial1.v.  The file is only one line:

Check 0.

Compilation output:
Error: Can't find file C:\MyProjects\Coq\MyTutorial.v

I tried it as well from the Coq folder.

How can I fix this?  Thanks.

Regards,
-EM




Archive powered by MHonArc 2.6.18.

Top of Page