The Coq mailing list

[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/>.