In this page, you will learn how the user-interface interacts with
the operating system and files on disk, about the options of the "File"
menu, how to parse a file and how to use parser
extensions, about the plain text format , the
Centaur polish format, and the Postscript
format, about the auto saving (backup) mechanism and
indications to turn around the system memory limitations. Also we explain how
to save on disk data that is normally displayed in windows without a File menu.
The File menu
The File menu is the first pull-down menu of the menubar,
on top of the Command window (you can have a screen shot
of all these windows in another page). It has the following aspect:
The options of this menu make it possible to read and write files in various
formats. Before touring all these options, we can explain the various formats.
The Centaur polish format
The Centaur polish format is a format that makes it possible to save a
document while respecting its tree structure and its annotations. This format
is useful in the following circumstances:
- For saving incomplete documents.
- Documents that contain holes (meta-variables) cannot be parsed again, so
that it is not possible to save an incomplete document in text format and
re-read it directly in Coq or in CtCoq. The polish format overcomes this
- For saving files in a format that can be quickly re-read.
- The parser used in CtCoq is very powerful because it enables dynamic
modification of the parsing rules. This power has a price in terms of parsing
efficiency. The loading of a polish file does not use the parser and this may
be much quicker.
- For saving proof texts in a re-loadable form.
- A proof text is an annotated tree, saving it in text format makes that only
the tree (and not the annotations) will be saved. Saving the proof text in
postscript format give a form that can be printed and displayed on screen using
a postscript previewer but which cannot be re-loaded in the CtCoq interface.
The polish format is the only format that will make it possible to re-load the
proof without replaying it in the Coq proof assistant.
Documents in polish format are distinguished by the special suffix ".po".
Files whose name terminates with this suffix can only be re-read if they are in
polish format. The CtCoq interface will save automatically in polish format if
it is writing in a file whose name has the suffix ".po".
The polish format is very version-dependent: it is most unlikely that a file
saved in polish format in one version of CtCoq will be re-loadable in another
The plain text format is a format that is compatible with the Coq parser.
When a document is saved in this format, both the Coq proof assistant
(independently from the CtCoq interface) and the CtCoq user-interface can
re-load it. This should be the preferred format for permanent storage and
communication with the Coq community.
Files saved in plain text format can be edited using a text editor, but they
will be re-loadable in the CtCoq user-interface only if they respect the Coq
syntax. Actually, there is not one Coq syntax, since the Coq parser
is extensible. If you want to use a syntax extension you need to tell the CtCoq
interface how to load this syntax extension.
The postscript format is used only to get hard copy prints of the Commands
and formulas as they appear on the screen. This format cannot be re-read.
The options of the "File" menu
Now that we know enough about the various formats that can be produced by
CtCoq, we can explain the use of the options provided by the "File"
- This option makes it possible to replace the contents of the window by the
document find in a file. When this option is triggered, the user is prompted
with an interactor that lets him choose a file name. If the file name has no
suffix or the ".v" suffix, then the file is parsed and the result of
parsing is displayed in the window. If the file name ends with ".po",
the file is read in polish format.
- This option makes it possible to re-read the file associated to the
window, thus re-synchronizing the window's content and the data on disk,
and possibly discard possible changes in this window.
- This option makes it possible to save the content of the window in the file
associated with the last "Read" or "Save as ..." operation.
If the file name ends with ".po" the contents will be saved in polish
format, otherwise it will be in plain text format.
- Save as ...
- This option makes it possible to save the contents of the window in a file
whose name is requested from the user. If the new file name ends with ".po"
the contents will be saved in polish format, otherwise it will be in plain text
- Save as is
- This option makes it possible to write the contents of the window in a file
whose name is requested from the user. The format is intermediary between a
text and a postscript format: all the characters present on screen are written,
but the font and color information is not. For example, the universal
quantification symbol is replaced by a '"'. This format, useful in other
applications of Centaur may not be very interesting in CtCoq.
- Write PS
- This option prompts the user for a file name and saves the postcript
commands necessary to reproduce on paper the characters on the screen. The
fonts are respected as much as possible, but not exactly since there may be
slight differences between the fonts available in X and the fonts available in
Postscript. The colors are mapped to black and white. Also the generated code
is not encapsulated.
- Add Syntax Path
- This option is present only in the File menu for the Command
window. It makes it possible to tell the CtCoq interface that syntax extensions
may be loaded from a specific directory.
The CtCoq interface accomodates
partially the possibility provided by the Coq proof assistant to add new grammar
rules to extend the parser. Only compiled parser extensions are accepted in
CtCoq (this contrasts with the more dynamic behavior of the Coq proof
assistant). Whenever you read a file that contains a "Require <package>."
command, such that the <package> file contains parser extensions and can
be found in the current syntax path, these extensions are taken into account in
the parser. However, if you attempt to load a file that contains a few grammar
rules and a few commands whose parsing is valid only in the context of these
grammar rules, the parsing will fail.
If you want to add new grammar
rules to the parser used in CtCoq, you should proceed as follows:
- Use a text editor to produce a <mysyntax.v> file containing the
grammar rules, that you store in a directory <mydirectory>
- Compile the file mysyntax.v using the command coqc provided in
the Coq distribution.
- Choose the option Add Syntax Path from the file menu and give <mydirectory>
at the prompt.
- Make sure the parser parses the string "Require mysyntax.". You
can either select a Command hole in you Command window, enter
text editing mode, type "Require mynsyntax." then <Escape>,
or make sure this string is in a file that you read using the "Read"
option of the "File" menu.
The backup mechanism
For the Command window and all Definitions
windows, the CtCoq user-interface provides a backup that saves regularly (every
ten minutes) the contents of these windows on disk. This mechanism can be used
to recover data that could be lost when a crash occurs. The backup files are in
polish format , they have a ".ckp.po" suffix, and they are saved in
four possible place:
- If a file name "file.v" is associated to the window and it
is possible to write a file ".file.ckp.po" in the same directory, then
this is where the backup is saved. For instance, if you are editing the
contents of the file found in "/net/home/bertot/tmp/drinking_problem.v"
the backup file will be called "/net/home/bertot/tmp/.dringin_problem.v".
At every backuping cycle, the backup files associated to documents that have
not been modified since the last save are destroyed.
- If no file name is associate to the document or if it is not possible to
save the backup file next to the original file following the naming convention
given above, and if the user set the resource "ctcoqv10.checkpoint.directory"
(resource class "Centaur.Checkpoint.Directory") to <directory>
then the backup file has the name "<directory>/tmp/ctcoq<nn>.ckp.po",
where <nn> is the decimal representation of a number chose to avoid
conflicts with existing files.
- If no resource has been set, the backup file name is "<current-directory>/.ctcoq<nn>.ckp.po".
Note that the base name starts with a dot, so that this backup file name does
not appear in a plain listing of the directory.
- If it is not possible to create a file in the current directory, then the
backup file name is"/tmp/ctcoq<nn>.ckp.po". Note that this
situation should be avoided since the directory "/tmp" is cleaned at
every reboot of the system (and a reboot usually follows a crash).
If you need to recover data from an auto-save file, you can simply read
this data in a CtCoq window using the "Read" button and then save it
in a more conventional file. The CtCoq interface does not recognize an
auto-save file as a special file when it reads it.
Saving non-conventional data on disk
The CtCoq user-interface provides a "File" menu for the Command
and Definitions windows, but not for the State
or Theorems windows. For personal needs, you may want to
keep on disk the contents of these windows. In this section we will indicate
how to do this.
Permanent storage for goals
The State window is not fitted with a File menu.
Sometimes it may be interesting to have a paper print of a goal, to study
independently of the workstation. It is possible to have goals displayed in a
window that has such a menu. The trick is to follow these instructions:
- Note the current rank of the goal, for instance by clicking on it, and
observing the indication in the toolbar. Let us say the goal you want is the
- In the command window, Edit and execute the command "2:Idtac.".
When this command is executed and stored in the script area, click on it and
type "<Shift>-H. This command normally opens a window with
the goal on which the selected command was apply in it.
- This window has a "File menu" and you can save the goal in polish
- If you want a postscript print of the goal, you must re-read this file in a
window fitted with a "Definitions" window that you obtain by typing "<Shift>-D
when the mouse is in the Command window.This is dirty, we should provide
a nicer way to do this!
Permanent storage for theorem statements
The Theorems window is not fitted with a File menu.
Sometimes it may be interesting to store collections of theorems related to
specific topics, re-using these collections as theorem menus in Library
windows. When you type <Shift>-D in the Theorems
window, the CtCoq user-interface opens a new Library window
fitted with a "File" menu. This file menu may be used to saved the
theorems on disk, in polish format. Here again, if you want a postscript
output, you need to use the same trick as above.
Permanent storage for proof texts
If you store a proof text in polish format, it will be possible to re-read
this proof text in the CtCoq interface in a later session. However, it is not
exact text that is saved in the polish format, but the formatting indications,
so that this proof text will still be displayable in several languages.