Add a tutorial about Require and Import

[Villetaneuse]

We can add exercises later but it's not easy with this technical subject. I wrote it thinking I wish I had this tutorial when learning Coq the hard way. TODO:

• [x] Add links suggested by Pierre Roux
• [ ] Add links to refman
• [x] Fill the new "guidelines about Require order" subsection with Pierre Roux's suggestions and more
• [x] remove the canonical structure while still mentioning the comma-separated list of features
• [x] rework the export section
• [x] test with 8.16
• [x] test with 8.17
• [x] test with 8.18
• [x] test with 8.19
• [x] test with dev

[Villetaneuse]

I still need to answer @SkySkimmer's correction about partially qualified names and the Require order (without losing the users' attention). I think that otherwise it's mostly complete. Thank you very much @SkySkimmer.

[Villetaneuse]

Globally, the content of the tutorial is good and clear.

However, the global structure of the tutorial is to flat, making it hard to reach the end and for casual users to locate the information they need. The issue is that the tutorial is long ~850 lines and there are 6 sections but no subsections, so there is nothing to isolate options and technical sections like section 6 from the core knowledge. By looking at the table of content, new users should be able to distinguish basic knowledge to know from options, and more advanced users to easily find the option they would like to learn

I recommend a structure of the following form, possibly adding some subsubsections (numbered or not) to some sections, like the 6. (or merged 4. and 5. + subsubsec ?)

1. Basic stuffs to know (1. 2. 3. possibly 4.)

2. Options (5. 6. possibly 4.)

Otherwise, an issue to me is that there is a point in the tutorial (I guess section 5) where I have the feeling it stops talking about files and only talks about modules. For instance, the discussion on exporting modules in section 5 (~70l). Talking about modules to talk about files sure, but I don't the think the discussion should be side tracked too much.

Hope it helps, best

Thank you very much.

Unfortunately, I think everything here is "core knowledge" (or should be): Export is widely used with files-modules, see for instance Arith_base in the stdlib, selective imports should be used more, locality attributes are widely used and often misunderstood. Everything I write about modules in this tutorial is also about library files.

A problem I have is that I can't really write other files to serve as files-modules examples in this tutorial.

[thomas-lamiaux]

@Villetaneuse I misunderstood it slightly, but my point still holds. Having sections do not have to mean one is options. It depends on what your titles are and what you say in the summary. Maybe there could be a first section about modules and names, and a second one about how to import modules ?

[Villetaneuse]

@Zimmi48 @thomas-lamiaux I have taken most (if not all) reviews into account, and they have been many (thank you very much, everyone!) I suggest we merge this if you agree. There can be more modifications later (for instance links to the reference manual, but I'm afraid it will scare the users) by anyone making a PR. But I'm satisfied with this as an initial version of this (hard to write) tutorial, and need to move on.