The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Thanks Adam, but I still can´t make it. I´ll try to be more specific then:

I have a file name "Automata.v" which is located at "C:\Users\Marcus Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current\Sources". This file starts with the following lines:

(*--------------------*)

Require Import Ascii.

Require Import String.

Require Import NPeano.

Add LoadPath "C:\Users\Marcus Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current" as Current.

Require Import Strings.

Require Import Symbols.

(*--------------------*)

When I execute "coqdep *.v" at Sources, I get the messages (besides others):

*** Warning: in file Automata.v, library Strings.v is required and has not been found in loadpath!

*** Warning: in file Automata.v, library Symbols.v is required and has not been found in loadpath!

Automata.vo Automata.glob Automata.v.beautified: Automata.v

Shouldn´t the files "Strings" and "Symbols" appear as dependencies for "Automata"? Also, why these warnings? When I execute interactively in coqide the files are found and loaded without any problem.

Last but not least, if I change "Require Import Strings." by "Require Import Current.Source.Strings." then it just doesn´t work at all and I get the message:

Error: The file C:\Users\Marcus Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current/Sources/Strings.vo contains library Strings and not library Current.Sources.Strings

But this is in accordance with section 6.6.3 of the Reference Manual, isn´t it?

Any help welcome.

Thanks,

Marcus.

2013/11/8 Adam Chlipala <adamc AT csail.mit.edu>

Have you read the whole chapter I pointed to?  It may be necessary to know a bit of ML module system terminology to understand it all, but I could also believe that it would just answer all your questions.

On 11/07/2013 09:11 PM, Marcus Ramos wrote:

Thanks for the pointer, Adam and Rodrigo. However, I guess my problem is even more basic, sorry to bother you with that.

I don´t know ML neither OCaml, and perhaps this is why I have trouble trying to understand what are the differences between libraries, sublibraries, modules, submodules, files, sets of files, logical and physical paths, and how I use these to organize my development. 

After all, I have to deal with concrete things such as files, folders and commands such as Add LoadPath, Require Import etc. Is there a tutorial on how to do this? After 5k lines of Coq code, I really have to get a better setup in order to move ahead.

Once again, sorry for bringing such basic questions to this forum. Was it ever considered to start a second and separate forum only for very beginners like me?

Thanks,

Marcus.

2013/11/7 Adam Chlipala <adamc AT csail.mit.edu>

On 11/07/2013 05:55 PM, Marcus Ramos wrote:

I am not making my way through with coqdep and coq_makefile.

...

Is there any tutorial with examples on how to use these tools correctly?

Yes.  See the "Build Processes" section of the "Proving in the Large" chapter of CPDT <http://adam.chlipala.net/cpdt/>.