Review #1

doc/sphinx/practical-tools/utilities.rst

@@ -12,8 +12,6 @@ running and compiling Coq scripts.  It recommends preferred ways to
 install Coq, manage installed packages and structure your project
 directories for the greatest ease of use.
 
-Feedback on errors and omissions will be appreciated.
-
 Installing Coq and Coq packages with opam
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -71,6 +69,9 @@ future the package name to logical name mapping will be more readily available.
 Once you know the logical name of the package, use it to load compiled
 files from the package with the :cmd:`Require` command.
 
+A :gdef:`package` is a group of files in a top directory and its subdirectories
+that's installed as a unit.  Packages are compiled from *projects*.  These terms
+are virtually interchangeable.
 
 Setup for working on your own projects
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -83,13 +84,11 @@ be copied or moved.
 We encourage you to use a source code control system for any non-trivial
 project because it makes it easy to track the history of your changes.
 `git <https://git-scm.com/>`_ is the system most used by Coq projects.
-Typically, each package has its own git repository.
-
-A :gdef:`package` is a group of files in a top directory and its subdirectories
-that's built and installed as a unit, just like the opam packages mentioned above.
+Typically, each project has its own git repository.
 
 For a project that has only a single file, you can create the file wherever you like
-and then step through it one of the Coq IDEs.
+and then step through it in one of the IDEs for Coq, such as CoqIDE, ProofGeneral, vsCoq
+and Coqtail.
 
 If your project has multiple files in a single directory that depend on each
 other through :cmd:`Require` commands, they must be compiled in an order that
@@ -102,34 +101,34 @@ with :n:`coqc A.v` followed by :n:`coqc B.v`, but you may find it tedious to
 manage the dependencies, particularly as the number of files increases.
 
 If your project files are in multiple directories, you would also need to pass
-additional command-line -Q and -R parameters to your IDE.  Too much detail.
+additional command-line -Q and -R parameters to your IDE.  More details to manage.
 
 Instead, by creating a `_CoqProject` file, you can automatically generate
 a makefile that applies the correct dependencies when it compiles your project.
-In addition, Coq IDEs find and interpret `_CoqProject` files, so project files
-over multiple directories will work seamlessly.  If you're editing `dir/foo.v`,
+In addition, the IDEs find and interpret `_CoqProject` files, so project files
+spread over multiple directories will work seamlessly.  If you're editing `dir/foo.v`,
 the IDEs apply settings from the `_CoqProject` file in `dir` or the closest
 ancestor directory.
 
 The `_CoqProject` file identifies the :term:`logical path` to associate with the
 directories containing your compiled files.  The `_CoqProject` file is normally
-in the top directory of the package.  Occasionally it may be useful to have
+in the top directory of the project.  Occasionally it may be useful to have
 additional `_CoqProject` files in subdirectories, for example in order to pass
 different startup parameters to Coq for particular scripts.
 
 .. _building_with_coqproject:
 
-Building a package with _CoqProject (overview)
+Building a project with _CoqProject (overview)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note: building with `dune` is experimental.  See :ref:`building_dune`.
 
 The `_CoqProject` file contains the information needed to generate a makefile
 for building your project.  Your `_CoqProject` file should be in
-the top directory of your package's source tree.  We recommend using the
-:term:`logical name` of the package as the name of the top directory.
+the top directory of your project's source tree.  We recommend using the
+:term:`logical name` of the project as the name of the top directory.
 
-For example, here's a minimal `_CoqProject` file for the `MyPackage` package
+For example, here is a minimal `_CoqProject` file for the `MyPackage` project
 (the logical name of the package), which includes all the ``.v`` files (and
 other file types) in the `theories` directory and its subdirectories::
 
@@ -138,7 +137,7 @@ other file types) in the `theories` directory and its subdirectories::
 
 :n:`-R theories MyPackage` (see :ref:`here <-Q-option>`) declares that `theories` is a top
 directory of `MyPackage`.  :n:`theories` on the second line declares that all `.v` files
-in `theories` and its subdirectories are indeed included in the package.
+in `theories` and its subdirectories are indeed included in the project.
 
 In addition, you can list individual files, for example the two script files
 `theories/File1.v` and `theories/SubDir/File2.v` whose logical paths are `MyPackage.File1` and
@@ -149,7 +148,6 @@ In addition, you can list individual files, for example the two script files
   theories/SubDir/File2.v
 
 The generated makefile only processes the specified files.
-
 You can list multiple directories if you wish.
 
 .. I think dotted names are not useful.  For example, this doesn't produce usable
@@ -274,7 +272,8 @@ a `From` clause provided that the logical path is unambiguous (as if they are
 available through `-R`).  In contrast, :cmd:`Require` commands that load files from other
 locations such as `user-contrib` must either use an exact logical path
 or include a `From` clause (as if they are available through `-Q`).  This is done
-to reduce the number of ambiguous logical paths.
+to reduce the number of ambiguous logical paths.  We encourage using `From`
+clauses.
 
 Note that if you use a `_CoqProject` file, the `COQPATH` environment variable is not helpful.
 If you use `COQPATH` without a `_CoqProject`, a file in `MyPackage/theories/SubDir/File.v` will be
@@ -284,31 +283,27 @@ If you associate the same logical name with more than one directory, Coq
 looks for the `.vo` file in the most recently added path first (i.e., the one
 that appears earlier in the :cmd:`Print LoadPath` output).
 
-Multi-package projects
-~~~~~~~~~~~~~~~~~~~~~~
+Modifying multiple interdependent projects at the same time
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-If you're modifying a multi-package project, you may want to be able to modify
-more than one packages as you work, in which case good practice recommends that
-none of its packages should be installed.  Since Coq IDEs only apply a single
-`_CoqProject` file for each script, the best way to handle this case is to
-temporarily edit the `_CoqProject` for each package so it includes the other
-uninstalled packages it depends on (then regenerate the makefile).  This may
+If you want to modify multiple interdependent projects simultaneously,
+good practice recommends that
+all of them should be uninstalled.  Since the IDEs only apply a single
+`_CoqProject` file for each script, the best way to make them work properly is to
+temporarily edit the `_CoqProject` for each project so it includes the other
+uninstalled projects it depends on, then regenerate the makefile.  This may
 make your `_CoqProject` system dependent.  Such dependencies shouldn't be
 present in published packages.
 
 For example, if
-package `A` requires package `B`, add `-Q <directory path of B> B` to the
+project `A` requires project `B`, add `-Q <directory path of B> B` to the
 `_CoqProject` in `A`.  This will override any installed version of `B` only
 when you're working on scripts in `A`.
 
-If you want to build an entire multi-package project at once, you're
+If you want to build all the related projects at once, you're
 on your own.  There's currently no tooling to identify the internal dependencies
-between the packages (and thus the order in which to build the packages).
+between the projects (and thus the order in which to build them).
 
-Alternatively, if you have a single-package project that depends on external
-packages that were not installed with the Coq binaries or accessible through
-`COQPATH`, you could add `-Q` options to the `_CoqProject` that point to the
-dependencies.
 
 .. todo I thought @herbelin added code to complain about ambiguous short names
    I made up some stuff below, need to check it:
@@ -317,7 +312,7 @@ Installed and uninstalled packages
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The directory structure of installed packages (i.e., in the `user-contrib` directory
-of the Coq installation) differs from that generally used for the package source tree.
+of the Coq installation) differs from that generally used for the project source tree.
 The installed directory structure omits the pathname given in the `-R` and `-Q`
 parameters that aren't part of the logical name of a script.  For example, the `theories`
 pathname used in this `_CoqProject` file is omitted from the installed pathname::
@@ -329,26 +324,26 @@ pathname used in this `_CoqProject` file is omitted from the installed pathname:
 `theories/File1.v` appears in the directory `user-contrib/MyPackage`and `theories/SubDir/File2.v`
  is in `user-contrib/MyPackage/SubDir`
 
-Use :n:`make -f CoqMakefile install` to install a package from a directory.
+Use :n:`make -f CoqMakefile install` to install a project from a directory.
 
 If you try to step through scripts in installed packages (e.g. to understand
 the proofs therein), you may get unexpected failures for two reasons (which
 don't apply to scripts in the standard library, which have logical paths
 beginning with `Coq`):
 
-* `_CoqProject` files commonly have at least one `-R` parameter, while
+* `_CoqProject` files often have at least one `-R` parameter, while
   installed packages are loaded with the less-permissive `-Q` option described in
   the :cmd:`Require` command, which may cause a :cmd:`Require` to fail.  One workaround is
-  to create a `_CoqProject` file containing the line `-R . <package directory>` in
-  `user-contrib/<package directory>`.  In this case, the `_CoqProject` doesn't
+  to create a `_CoqProject` file containing the line `-R . <project directory>` in
+  `user-contrib/<project directory>`.  In this case, the `_CoqProject` doesn't
   need to list all the source files.
 
 * Sometimes, the `_CoqProject` file specifies options that affect the
   behavior of Coq, such as `-impredicative-set`.  These can similarly be
   added in `_CoqProject` files in `user-contrib`.
 
 Another way to get around these problems is to download the source tree for the
-package in a new directory and compile it before stepping through its scripts.
+project in a new directory and compile it before stepping through its scripts.
 
 Upgrading to a new version of Coq
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -361,7 +356,6 @@ new version, most users no longer have a need to run on the old version.
 
 If, however, you want to overlap working on your project on both the old and new
 versions, you'll need to create separate source directories for your project
-versions, you'll need to create separate source directories for your project
 for the different Coq versions.  Currently the compiled `.vo` files are kept
 in the same directory as their corresponding `.v` file.