The Coq mailing list

[karsar <karen.sarkisyan AT gmail.com>]

You just go to the relevant directory in your terminal, type 'make' and hit enter. Then wait.

If your version of Coq is suitable for cpdt, then all will finish successfully. 

make will prepare .vo files from .v files. Files with .vo extension are required for

loading libraries in you case. They are not there by default. More on this at https://coq.inria.fr/tutorial/3-modules.

I feel it would be easier for you to start with web version though.

Best,

Karen

On Sun, Aug 20, 2017 at 3:06 PM, Manny Romero <mannyromero AT mail.com> wrote:

Thank you for your help.

 

I had read the section you describe. It looked--and it still looks--like it is mostly about people using Coq in Emacs. I do not have Emacs; I have been using CoqIde. There may be a part of the section you cite that is relevant for my purposes; but again, I am much too unfamiliar with computers to know what that would be and how to use it. For example, I don't know what "make" is yet, so I can't currently make sense of an abstract instruction to use it (if indeed that part is applicable to CoqIde). More specific advice, beyond what I had already seen e.g. in the textbook, was exactly what I was hoping to get help on.

 

Sent: Sunday, August 20, 2017 at 2:35 AM
From: karsar <karen.sarkisyan AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to add file locations for Require Import? (CoqIde)

You'll need to read "1.6.3 Installation and Emacs Set-Up" from Chapter 1 (Introduction) in Cpdt book and do all the steps beyond unzipping.

There is an easy way to experiment with code in your browser as well.

At https://x80.org/collacoq/ you need to click on Packages (right and down at the page) 

to load required packages, like cpdt, cor-arith, coq-base...

Then, to import all you need, just do:

 

From Coq Require Import Bool.Bool Arith.Arith Lists.List. 

From Cpdt Require Import CpdtTactics.

 

Set Implicit Arguments.
Set Asymmetric Patterns.

 

Hope this is useful. 

Best,

Karen Sargsyan

 

On Sun, Aug 20, 2017 at 1:43 PM, Manny Romero <mannyromero AT mail.com> wrote:

Hello! Apologies if this isn't the appropriate mailing list; I couldn't find a Coq beginners' list anywhere.

 

I am someone who is ignorant of the most basic aspects of computers who is getting started with Coq. I have installed the CoqIde 8.4pl4 on Linux Mint 18 and used it successfully with some simple tutorials.

 

Now, however, I am trying to use the textbook **Adam Chlipala** ( http://adam.chlipala.net/cpdt/ ); and, as explained at the beginning of Chapter 2, it requires me to "Require Import" various files to follow along with the texts and do the exercises. Specifically, I must:

 

Require Import Bool Arith List Cpdt.CpdtTactics.
Set Implicit Arguments.
Set Asymmetric Patterns.

 

Cpdt.CpdtTactics is among the files available for download on the Chlipala website. I downloaded all the files and "unzipped" them into a subfolder I made within my folder /home/mannyromero/Downloads; but that is not among the locations I see when I enter "Print LoadPath" into the CoqIde, which I assume is why I get a message "Error: Cannot find library Cpdt.CpdtTactics in loadpath" when I try to Require Import as above.

 

What do I do to add the location of the Cpdt.CpdtTactics file to the CoqIde's list somehow so that I can Require Import it and proceed with the textbook exercises?

 

Or, if this is off topic or inappropriate, apologies and can someone direct me to a better community to ask this question?