5.4 Compiled files
This feature allows to build files for a quick loading. When loaded, the commands contained in a compiled file will not be replayed. In particular, proofs will not be replayed. This avoids a useless waste of time.Remark: A module containing an open section cannot be compiled.
5.4.1 Compile Module ident.
This command loads the file ident.v and plays the script it contains. Declarations, definitions and proofs it contains are "packaged" in a compiled form: the module named ident. A file ident.vo is then created. The file ident.v is searched according to the current loadpath. The ident.vo is then written in the directory where ident.v was found.Variants:
-
Compile Module ident string.
Uses the file string.v or string if the previous one does not exist to build the module ident. In this case, string is any string giving a filename in the UNIX sense (see section 1).
- Compile Module Specification ident.
Builds a specification module: only the types of terms are stored in the module. The bodies (the proofs) are not written in the module. In that case, the file created is ident.vi. This is only useful when proof terms take too much place in memory and are not necessary. - Compile Verbose Module ident.
Verbose version of Compile: shows the contents of the file being compiled.
These different variants can be combined.
Error messages:
-
You cannot open a module when there are things other than
Modules and Imports in the context.
The only commands allowed before a Compile Module command are Require,
Read Module and Import. Actually, The normal way to compile modules is by the coqc command (see chapter 11).
See also: sections 5.2.4, 5.5, chapter 11
5.4.2 Read Module ident.
Loads the module stored in the file ident, but does not open it: its contents is invisible to the user. The implementation file (ident.vo) is searched first, then the specification file (ident.vi) in case of failure.5.4.3 Import ident.
Opens the module ident. The module ident must have been previously loaded (through the Read Module command or embedded Require commands. See the description of the Require command below).5.4.4 Require ident.
This command loads and opens (imports) the module stored in the file ident. The implementation file (ident.vo) is searched first, then the specification file (ident.vi) in case of failure. If the module required has already been loaded, Coq simply opens it (as Import ident would do it). If the module required is already loaded and open, Coq displays the following warning: ident already imported.If a module A contains a command Require B then the command Require A loads the module B but does not open it (See the Require Export variant below).
Variants:
-
Require Export ident.
This command acts as Require ident. But if a module A contains a command Require Export B, then the command Require A opens the module B as if the user would have typed RequireB. - Require [ Implementation | Specification ] ident.
Is the same as Require, but specifying explicitly the implementation (.vo file) or the specification (.vi file). - Require ident string.
Specifies the file to load as being string, instead of ident. The opened module is still ident and therefore must have been loaded. - Require ident string.
Specifies the file to load as being string, instead of ident. The opened module is still ident.
These different variants can be combined.
Error messages:
-
Can't find module toto on loadpath
The command did not find the file toto.vo. Either toto.v exists but is not compiled or toto.vo is in a directory which is not in your LoadPath (see section 5.5). - Bad magic number
The file ident.vo was found but either it is not a Coq compiled module, or it was compiled with an older and incompatible version of Coq.
See also: chapter 11
5.4.5 Print Modules.
This command shows the currently loaded and currently opened (imported) modules.5.4.6 Declare ML Module string1 .. stringn.
This commands loads the Objective Caml compiled files string1 ...stringn (dynamic link). It is mainly used to load tactics dynamically (see chapter 10). The files are searched into the current Objective Caml loadpath (see the command Add ML Path in the section 5.5). Loading of Objective Caml files is only possible under the bytecode version of coqtop (i.e. not using options -opt or -full -- see chapter 11).5.4.7 Print ML Modules.
This print the name of all Objective Camlmodules loaded with Declare ML Module. To know from where these module were loaded, the user should use the command Locate File (X)