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 difficulty.

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 version.

The plain text format

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

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" menu.

Open

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.

ReOpen

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.

Save

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 format.

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:

1. Use a text editor to produce a <mysyntax.v> file containing the grammar rules, that you store in a directory <mydirectory>
2. Compile the file mysyntax.v using the command coqc provided in the Coq distribution.
3. Choose the option Add Syntax Path from the file menu and give <mydirectory> at the prompt.
4. 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:

1. 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 second one.
2. 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.
3. This window has a "File menu" and you can save the goal in polish format.
4. 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.