The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

We are happy to announce the release of a new version of CtCoq, now
adapted for CoqV6.2.1

CtCoq is a graphical user interface that helps you produce and maintain
proof scripts for the Coq proof system.  It works by managing the
communication with the Coq system, displaying goals and computation
results in various windows, and recording all successful commands in
scripts that are kept clean and uncorrupted by the system.

The main advantages of using CtCoq are :

-- Proof-By-Pointing: generate proof commands using only the
   mouse to point at the relevant data on the screen.

-- Script Management: see at first glance the commands that have
   been successfully executed, replay old scripts coming from all
   versions of Coq or old axiomatizations, and let the interface point
   you to the commands that no longer work.

-- Elaborate Undoing: undo proof commands with unlimited depth within
   the same proof.  Use logical undo, where you can undo an older command
   without undoing commands that have been executed later, but which are
   unrelated.  Visualize dependencies between various proof commands.  
   Visualize previous goals without having to undo the commands.

-- Domain specific notations: Using the PPML language, you can also
   adapt your notation to the mathematical domain you work on.

-- Structured editing: select large expressions in just one click,
   forget the pains of looking for missing parentheses.  Use menu
   directed editing to perform intricate modifications of your
   expressions with only the mouse.  Add you own entries in these
   menus for your most frequent commands.

The CtCoq system is available on a variety of Unix varieties, mainly

   linux (Intel architecture), solaris (Sun), and decosf1 (alpha 
machines).

Other architecture may be available, please contact us!

It typically requires between 15 and 30 MBytes (when the Coq system
reaches 80 MBytes to do the proofs on a decosf machine).

CtCoq is not free software, but it is available free of charge from
the following addresses:

http://www.inria.fr/croap/ctcoq/ctcoq-eng.html
http://www.inria.fr/croap/ctcoq/ctcoq-fra.html ;(in french)

The CtCoq team: 
ctcoq-request AT sophia.inria.fr