diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 256 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 307 |
2 files changed, 563 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst new file mode 100644 index 0000000000..1ff808894a --- /dev/null +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -0,0 +1,256 @@ +.. include:: ../replaces.rst + +.. _thecoqcommands: + +The |Coq| commands +==================== + +There are three |Coq| commands: + ++ ``coqtop``: the |Coq| toplevel (interactive mode); ++ ``coqc``: the |Coq| compiler (batch compilation); ++ ``coqchk``: the |Coq| checker (validation of compiled libraries). + + +The options are (basically) the same for the first two commands, and +roughly described below. You can also look at the ``man`` pages of +``coqtop`` and ``coqc`` for more details. + +Interactive use (coqtop) +------------------------ + +In the interactive mode, also known as the |Coq| toplevel, the user can +develop his theories and proofs step by step. The |Coq| toplevel is run +by the command ``coqtop``. + +They are two different binary images of |Coq|: the byte-code one and the +native-code one (if OCaml provides a native-code compiler for +your platform, which is supposed in the following). By default, +``coqtop`` executes the native-code version; run ``coqtop.byte`` to get +the byte-code version. + +The byte-code toplevel is based on an OCaml toplevel (to +allow dynamic linking of tactics). You can switch to the OCaml toplevel +with the command ``Drop.``, and come back to the |Coq| +toplevel with the command ``Coqloop.loop();;``. + +Batch compilation (coqc) +------------------------ + +The ``coqc`` command takes a name *file* as argument. Then it looks for a +vernacular file named *file*.v, and tries to compile it into a +*file*.vo file (See :ref:`TODO-6.5`). Warning: The name *file* should be a +regular |Coq| identifier, as defined in Section :ref:'TODO-1.1'. It should contain +only letters, digits or underscores (_). For instance, ``/bar/foo/toto.v`` is valid, but +``/bar/foo/to-to.v`` is invalid. + + +Customization at launch time +--------------------------------- + +By resource file +~~~~~~~~~~~~~~~~~~~~~~~ + +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file +``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +is the configuration directory of the user (by default its home +directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is +searched. You can also specify an arbitrary name for the resource file +(see option ``-init-file`` below). + +This file may contain, for instance, ``Add LoadPath`` commands to add +directories to the load path of |Coq|. It is possible to skip the +loading of the resource file with the option ``-q``. + + +By environment variables +~~~~~~~~~~~~~~~~~~~~~~~~~ + +Load path can be specified to the |Coq| system by setting up ``$COQPATH`` +environment variable. It is a list of directories separated by +``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and +``$XDG_DATA_DIRS`` (see Section :ref:`TODO-2.6.3`). + +Some |Coq| commands call other |Coq| commands. In this case, they look for +the commands in directory specified by ``$COQBIN``. If this variable is +not set, they look for the commands in the executable path. + +The ``$COQ_COLORS`` environment variable can be used to specify the set +of colors used by ``coqtop`` to highlight its output. It uses the same +syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated +list of assignments of the form ``name=``:n:``{*; attr}`` where +``name`` is the name of the corresponding highlight tag and each ``attrᵢ`` is an +ANSI escape code. The list of highlight tags can be retrieved with the +``-list-tags`` command-line option of ``coqtop``. + +By command line options +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following command-line options are recognized by the commands ``coqc`` +and ``coqtop``, unless stated otherwise: + +:-I *directory*, -include *directory*: Add physical path *directory* + to the OCaml loadpath. See also: :ref:`TODO-2.6.1` and the + command Declare ML Module Section :ref:`TODO-6.5`. +:-Q *directory* dirpath: Add physical path *directory* to the list of + directories where |Coq| looks for a file and bind it to the the logical + directory *dirpath*. The subdirectory structure of *directory* is + recursively available from |Coq| using absolute names (extending the + dirpath prefix) (see Section :ref:`TODO-2.6.2`).Note that only those + subdirectories and files which obey the lexical conventions of what is + an ident (see Section :ref:`TODO-1.1`) are taken into account. Conversely, the + underlying file systems or operating systems may be more restrictive + than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive + layout (within the limit of 255 bytes per file name), the default on + NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to + disallow two files differing only in the case in the same directory. + See also: Section :ref:`TODO-2.6.1`. +:-R *directory* dirpath: Do as -Q *directory* dirpath but make the + subdirectory structure of *directory* recursively visible so that the + recursive contents of physical *directory* is available from |Coq| using + short or partially qualified names. See also: Section :ref:`TODO-2.6.1`. +:-top dirpath: Set the toplevel module name to dirpath instead of Top. + Not valid for `coqc` as the toplevel module name is inferred from the + name of the output file. +:-exclude-dir *directory*: Exclude any subdirectory named *directory* + while processing options such as -R and -Q. By default, only the + conventional version control management directories named CVS + and_darcs are excluded. +:-nois: Start from an empty state instead of loading the Init.Prelude + module. +:-init-file *file*: Load *file* as the resource file instead of + loading the default resource file from the standard configuration + directories. +:-q: Do not to load the default resource file. +:-load-ml-source *file*: Load the OCaml source file *file*. +:-load-ml-object *file*: Load the OCaml object file *file*. +:-l *file*, -load-vernac-source *file*: Load and execute the |Coq| + script from *file.v*. +:-lv *file*, -load-vernac-source-verbose *file*: Load and execute the + |Coq| script from *file.v*. Output its content on the standard input as + it is executed. +:-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This + is equivalent to runningRequire dirpath. +:-require dirpath: Load |Coq| compiled library dirpath and import it. + This is equivalent to running Require Import dirpath. +:-batch: Exit just after argument parsing. Available for `coqtop` only. +:-compile *file.v*: Compile file *file.v* into *file.vo*. This options + imply -batch (exit just after argument parsing). It is available only + for `coqtop`, as this behavior is the purpose of `coqc`. +:-compile-verbose *file.v*: Same as -compile but also output the + content of *file.v* as it is compiled. +:-verbose: Output the content of the input file as it is compiled. + This option is available for `coqc` only; it is the counterpart of + -compile-verbose. +:-w (all|none|w₁,…,wₙ): Configure the display of warnings. This + option expects all, none or a comma-separated list of warning names or + categories (see Section :ref:`TODO-6.9.3`). +:-color (on|off|auto): Enable or not the coloring of output of `coqtop`. + Default is auto, meaning that `coqtop` dynamically decides, depending on + whether the output channel supports ANSI escape sequences. +:-beautify: Pretty-print each command to *file.beautified* when + compiling *file.v*, in order to get old-fashioned + syntax/definitions/notations. +:-emacs, -ide-slave: Start a special toplevel to communicate with a + specific IDE. +:-impredicative-set: Change the logical theory of |Coq| by declaring the + sort Set impredicative. Warning: This is known to be inconsistent with some + standard axioms of classical mathematics such as the functional + axiom of choice or the principle of description. +:-type-in-type: Collapse the universe hierarchy of |Coq|. Warning: This makes the logic + inconsistent. +:-mangle-names *ident*: Experimental: Do not depend on this option. Replace + Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, + etc. The command ``Set Mangle Names`` turns the behavior on in a document, + and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature + s intended to be used as a linter for developments that want to be robust to + changes in the auto-generated name scheme. The options are provided to + facilitate tracking down problems. +:-compat *version*: Attempt to maintain some backward-compatibility + with a previous version. +:-dump-glob *file*: Dump references for global names in file *file* + (to be used by coqdoc, see :ref:`TODO-15.4`). By default, if *file.v* is being + compiled, *file.glob* is used. +:-no-glob: Disable the dumping of references for global names. +:-image *file*: Set the binary image to be used by `coqc` to be *file* + instead of the standard one. Not of general use. +:-bindir *directory*: Set the directory containing |Coq| binaries to be + used by `coqc`. It is equivalent to doing export COQBIN= *directory* + before launching `coqc`. +:-where: Print the location of |Coq|’s standard library and exit. +:-config: Print the locations of |Coq|’s binaries, dependencies, and + libraries, then exit. +:-filteropts: Print the list of command line arguments that `coqtop` has + recognized as options and exit. +:-v: Print |Coq|’s version and exit. +:-list-tags: Print the highlight tags known by |Coq| as well as their + currently associated color and exit. +:-h, --help: Print a short usage and exit. + +Compiled libraries checker (coqchk) +---------------------------------------- + +The ``coqchk`` command takes a list of library paths as argument, described either +by their logical name or by their physical filename, hich must end in ``.vo``. The +corresponding compiled libraries (``.vo`` files) are searched in the path, +recursively processing the libraries they depend on. The content of all these +libraries is then type-checked. The effect of ``coqchk`` is only to return with +normal exit code in case of success, and with positive exit code if an error has +been found. Error messages are not deemed to help the user understand what is +wrong. In the current version, it does not modify the compiled libraries to mark +them as successfully checked. + +Note that non-logical information is not checked. By logical +information, we mean the type and optional body associated to names. +It excludes for instance anything related to the concrete syntax of +objects (customized syntax rules, association between short and long +names), implicit arguments, etc. + +This tool can be used for several purposes. One is to check that a +compiled library provided by a third-party has not been forged and +that loading it cannot introduce inconsistencies [#]_. Another point is +to get an even higher level of security. Since ``coqtop`` can be extended +with custom tactics, possibly ill-typed code, it cannot be guaranteed +that the produced compiled libraries are correct. ``coqchk`` is a +standalone verifier, and thus it cannot be tainted by such malicious +code. + +Command-line options ``-Q``, ``-R``, ``-where`` and ``-impredicative-set`` are supported +by ``coqchk`` and have the same meaning as for ``coqtop``. As there is no notion of +relative paths in object files ``-Q`` and ``-R`` have exactly the same meaning. + +:-norec *module*: Check *module* but do not check its dependencies. +:-admit *module*: Do not check *module* and any of its dependencies, + unless explicitly required. +:-o: At exit, print a summary about the context. List the names of all + assumptions and variables (constants without body). +:-silent: Do not write progress information in standard output. + +Environment variable ``$COQLIB`` can be set to override the location of +the standard library. + +The algorithm for deciding which modules are checked or admitted is +the following: assuming that ``coqchk`` is called with argument ``M``, option +``-norec N``, and ``-admit A``. Let us write :math:`\overline{S}` for the +set of reflexive transitive dependencies of set :math:`S`. Then: + ++ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type-checked before being added + to the context. ++ And :math:`M \cup N \backslash C` is the set of modules that are loaded and added to the + context without type-checking. Basic integrity checks (checksums) are + nonetheless performed. + +As a rule of thumb, the -admit can be used to tell that some libraries +have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` && +``coqchk B -admit A`` without type-checking any definition twice. Of +course, the latter is slightly slower since it makes more disk access. +It is also less secure since an attacker might have replaced the +compiled library ``A`` after it has been read by the first command, but +before it has been read by the second command. + +.. [#] Ill-formed non-logical information might for instance bind + Coq.Init.Logic.True to short name False, so apparently False is + inhabited, but using fully qualified names, Coq.Init.Logic.False will + always refer to the absurd proposition, what we guarantee is that + there is no proof of this latter constant. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst new file mode 100644 index 0000000000..1fcfc665be --- /dev/null +++ b/doc/sphinx/practical-tools/coqide.rst @@ -0,0 +1,307 @@ +.. include:: ../replaces.rst + +.. _coqintegrateddevelopmentenvironment: + +|Coq| Integrated Development Environment +======================================== + +The Coq Integrated Development Environment is a graphical tool, to be +used as a user-friendly replacement to `coqtop`. Its main purpose is to +allow the user to navigate forward and backward into a Coq vernacular +file, executing corresponding commands or undoing them respectively. + +CoqIDE is run by typing the command `coqide` on the command line. +Without argument, the main screen is displayed with an “unnamed +buffer”, and with a file name as argument, another buffer displaying +the contents of that file. Additionally, `coqide` accepts the same +options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously +no meaning for |CoqIDE| being ignored. + +.. _coqide_mainscreen: + + .. image:: ../_static/coqide.png + :alt: |CoqIDE| main screen + +A sample |CoqIDE| main screen, while navigating into a file `Fermat.v`, +is shown in the figure :ref:`CoqIDE main screen <coqide_mainscreen>`. +At the top is a menu bar, and a tool bar +below it. The large window on the left is displaying the various +*script buffers*. The upper right window is the *goal window*, where +goals to prove are displayed. The lower right window is the *message +window*, where various messages resulting from commands are displayed. +At the bottom is the status bar. + +Managing files and buffers, basic editing +---------------------------------------------- + +In the script window, you may open arbitrarily many buffers to edit. +The *File* menu allows you to open files or create some, save them, +print or export them into various formats. Among all these buffers, +there is always one which is the current *running buffer*, whose name +is displayed on a background in the *processed* color (green by default), which +is the one where Coq commands are currently executed. + +Buffers may be edited as in any text editor, and classical basic +editing commands (Copy/Paste, …) are available in the *Edit* menu. +CoqIDE offers only basic editing commands, so if you need more complex +editing commands, you may launch your favorite text editor on the +current buffer, using the *Edit/External Editor* menu. + +Interactive navigation into Coq scripts +-------------------------------------------- + +The running buffer is the one where navigation takes place. The toolbar offers +five basic commands for this. The first one, represented by a down arrow icon, +is for going forward executing one command. If that command is successful, the +part of the script that has been executed is displayed on a background with the +processed color. If that command fails, the error message is displayed in the +message window, and the location of the error is emphasized by an underline in +the error foreground color (red by default). + +In the figure :ref:`CoqIDE main screen <coqide_mainscreen>`, +the running buffer is `Fermat.v`, all commands until +the ``Theorem`` have been already executed, and the user tried to go +forward executing ``Induction n``. That command failed because no such +tactic exists (tactics are now in lowercase…), and the wrong word is +underlined. + +Notice that the processed part of the running buffer is not editable. If +you ever want to modify something you have to go backward using the up +arrow tool, or even better, put the cursor where you want to go back +and use the goto button. Unlike with `coqtop`, you should never use +``Undo`` to go backward. + +There are two additional buttons for navigation within the running buffer. The +"down" button with a line goes directly to the end; the "up" button with a line +goes back to the beginning. The handling of errors when using the go-to-the-end +button depends on whether |Coq| is running in asynchronous mode or not (see +Chapter :ref:`Asyncprocessing`). If it is not running in that mode, execution +stops as soon as an error is found. Otherwise, execution continues, and the +error is marked with an underline in the error foreground color, with a +background in the error background color (pink by default). The same +characterization of error-handling applies when running several commands using +the "goto" button. + +If you ever try to execute a command which happens to run during a +long time, and would like to abort it before its termination, you may +use the interrupt button (the white cross on a red circle). + +There are other buttons on the CoqIDE toolbar: a button to save the running +buffer; a button to close the current buffer (an "X"); buttons to switch among +buffers (left and right arrows); an "information" button; and a "gears" button. + +The "information" button is described in Section :ref:`sec:trytactics`. + +The "gears" button submits proof terms to the |Coq| kernel for type-checking. +When |Coq| uses asynchronous processing (see Chapter :ref:`Asyncprocessing`), +proofs may have been completed without kernel-checking of generated proof terms. +The presence of unchecked proof terms is indicated by ``Qed`` statements that +have a subdued *being-processed* color (light blue by default), rather than the +processed color, though their preceding proofs have the processed color. + +Notice that for all these buttons, except for the "gears" button, their operations +are also available in the menu, where their keyboard shortcuts are given. + +.. _try-tactics-automatically: + +Trying tactics automatically +------------------------------ + +The menu Try Tactics provides some features for automatically trying +to solve the current goal using simple tactics. If such a tactic +succeeds in solving the goal, then its text is automatically inserted +into the script. There is finally a combination of these tactics, +called the *proof wizard* which will try each of them in turn. This +wizard is also available as a tool button (the "information" button). The set of +tactics tried by the wizard is customizable in the preferences. + +These tactics are general ones, in particular they do not refer to +particular hypotheses. You may also try specific tactics related to +the goal or one of the hypotheses, by clicking with the right mouse +button on the goal or the considered hypothesis. This is the +“contextual menu on goals” feature, that may be disabled in the +preferences if undesirable. + + +Proof folding +------------------ + +As your script grows bigger and bigger, it might be useful to hide the +proofs of your theorems and lemmas. + +This feature is toggled via the Hide entry of the Navigation menu. The +proof shall be enclosed between ``Proof.`` and ``Qed.``, both with their final +dots. The proof that shall be hidden or revealed is the first one +whose beginning statement (such as ``Theorem``) precedes the insertion +cursor. + + +Vernacular commands, templates +----------------------------------- + +The Templates menu allows using shortcuts to insert vernacular +commands. This is a nice way to proceed if you are not sure of the +spelling of the command you want. + +Moreover, this menu offers some *templates* which will automatic +insert a complex command like ``Fixpoint`` with a convenient shape for its +arguments. + +Queries +------------ + +.. _coqide_queryselected: + +.. image:: ../_static/coqide-queries.png + :alt: |CoqIDE| queries + +We call *query* any vernacular command that does not change the current state, +such as ``Check``, ``Search``, etc. To run such commands interactively, without +writing them in scripts, CoqIDE offers a *query pane*. The query pane can be +displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. +Queries can also be performed by selecting a particular phrase, then choosing an +item from the ``Queries`` menu. The response then appears in the message window. +Figure :ref:`fig:queryselected` shows the result after selecting of the phrase +``Nat.mul`` in the script window, and choosing ``Print`` from the ``Queries`` +menu. + + +Compilation +---------------- + +The `Compile` menu offers direct commands to: + ++ compile the current buffer ++ run a compilation using `make` ++ go to the last compilation error ++ create a `Makefile` using `coq_makefile`. + +Customizations +------------------- + +You may customize your environment using menu Edit/Preferences. A new +window will be displayed, with several customization sections +presented as a notebook. + +The first section is for selecting the text font used for scripts, +goal and message windows. + +The second section is devoted to file management: you may configure +automatic saving of files, by periodically saving the contents into +files named `#f#` for each opened file `f`. You may also activate the +*revert* feature: in case a opened file is modified on the disk by a +third party, |CoqIDE| may read it again for you. Note that in the case +you edited that same file, you will be prompt to choose to either +discard your changes or not. The File charset encoding choice is +described below in :ref:`character-encoding-saved-files`. + +The `Externals` section allows customizing the external commands for +compilation, printing, web browsing. In the browser command, you may +use `%s` to denote the URL to open, for example: +`firefox -remote "OpenURL(%s)"`. + +The `Tactics Wizard` section allows defining the set of tactics that +should be tried, in sequence, to solve the current goal. + +The last section is for miscellaneous boolean settings, such as the +“contextual menu on goals” feature presented in the section +:ref:`Try tactics automatically <try-tactics-automatically>`. + +Notice that these settings are saved in the file `.coqiderc` of your +home directory. + +A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It +is not recommanded to edit this file manually: to modify a given menu +shortcut, go to the corresponding menu item without releasing the +mouse button, press the key you want for the new shortcut, and release +the mouse button afterwards. If your system does not allow it, you may +still edit this configuration file by hand, but this is more involved. + + +Using Unicode symbols +-------------------------- + +CoqIDE is based on GTK+ and inherits from it support for Unicode in +its text windows. Consequently a large set of symbols is available for +notations. + + +Displaying Unicode symbols +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +You just need to define suitable notations as described in the chapter +:ref:`syntaxextensionsandinterpretationscopes`. For example, to use the +mathematical symbols ∀ and ∃, you may define: + +.. coqtop:: in + + Notation "∀ x : T, P" := + (forall x : T, P) (at level 200, x ident). + Notation "∃ x : T, P" := + (exists x : T, P) (at level 200, x ident). + +There exists a small set of such notations already defined, in the +file `utf8.v` of Coq library, so you may enable them just by +``Require utf8`` inside |CoqIDE|, or equivalently, by starting |CoqIDE| with +``coqide -l utf8``. + +However, there are some issues when using such Unicode symbols: you of +course need to use a character font which supports them. In the Fonts +section of the preferences, the Preview line displays some Unicode +symbols, so you could figure out if the selected font is OK. Related +to this, one thing you may need to do is choose whether GTK+ should +use antialiased fonts or not, by setting the environment variable +`GDK_USE_XFT` to 1 or 0 respectively. + + +Defining an input method for non-ASCII symbols +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +To input a Unicode symbol, a general method provided by GTK+ is to +simultaneously press the Control, Shift and “u” keys, release, then +type the hexadecimal code of the symbol required, for example `2200` +for the ∀ symbol. A list of symbol codes is available at +`http://www.unicode.org`. + +An alternative method which does not require to know the hexadecimal +code of the character is to use an Input Method Editor. On POSIX +systems (Linux distributions, BSD variants and MacOS X), you can +use `uim` version 1.6 or later which provides a :math:`\LaTeX`-style input +method. + +To configure uim, execute uim-pref-gtk as your regular user. In the +"Global Settings" group set the default Input Method to "ELatin" +(don’t forget to tick the checkbox "Specify default IM"). In the +"ELatin" group set the layout to "TeX", and remember the content of +the "[ELatin] on" field (by default Control-\\). You can now execute +|CoqIDE| with the following commands (assuming you use a Bourne-style +shell): + +:: + + $ export GTK_IM_MODULE=uim + $ coqide + + +Activate the ELatin Input Method with Control-\\, then type the +sequence `\\Gamma`. You will see the sequence being replaced by Γ as +soon as you type the second "a". + +.. _character-encoding-saved-files: + +Character encoding for saved files +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In the Files section of the preferences, the encoding option is +related to the way files are saved. + +If you have no need to exchange files with non UTF-8 aware +applications, it is better to choose the UTF-8 encoding, since it +guarantees that your files will be read again without problems. (This +is because when |CoqIDE| reads a file, it tries to automatically detect +its character encoding.) + +If you choose something else than UTF-8, then missing characters will +be written encoded by `\x{....}` or `\x{........}` where each dot is +an hexadecimal digit: the number between braces is the hexadecimal +Unicode index for the missing character. |