coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Add Load Path however still can not find library

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Add Load Path however still can not find library
Date: Sun, 20 Dec 2015 11:42:12 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f182.google.com
Ironport-phdr: 9a23:xVIs4hTsJsBkfNl6O/xzfG9Ql9psv+yvbD5Q0YIujvd0So/mwa64YRaN2/xhgRfzUJnB7Loc0qyN4/6mATRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niabqo9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULYQWD8hKiU+4NDhnRjFVwqGoHUGBDY4iB1NViHP7BDhXpry+gL8v+xxkH2TN833VrA5WnKr6a5tRFnpiTsIHzE8+WDTzMd3ifQI81qauxVjztuMM8muP/1kc/aFcA==

The answer is clearly described in the description of the commands "Add Loadpath" and "Require Import" in the manual at

https://coq.inria.fr/refman/command-index.html

To summarize, you must ensure that the file

/home/martin/hilbertreborn/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.vo

exists. Perhaps you haven't compiled the library GeoCoq.

Also, I would highly recommend first reading some basic Coq tutorial.

Perhaps read the first few chapters of

https://www.cis.upenn.edu/~bcpierce/sf/current/toc.html ?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Dec 20, 2015 at 1:55 AM, Mandy Martino <tesleft AT hotmail.com> wrote:

Hi,

martin@ubuntu:~/hilbertreborn/GeoCoq/Highschool$ coqtop
Welcome to Coq 8.4pl6 (December 2015)

Coq < Add LoadPath "/home/martin/hilbertreborn/GeoCoq/".
Require Import GeoCoq.Tarski_dev.Annexes.midpoint_theorems.
Coq <
Error: Cannot find library GeoCoq.Tarski_dev.Annexes.midpoint_theorems in loadpath

Regards,

Martin

[Coq-Club] make error for geocoq, Mandy Martino, 12/11/2015
- Re: [Coq-Club] make error for geocoq, Julien Narboux, 12/12/2015
  - [Coq-Club] Add Load Path however still can not find library, Mandy Martino, 12/20/2015
    - Re: [Coq-Club] Add Load Path however still can not find library, Abhishek Anand, 12/20/2015