Another day, another prover:

added support for the Casl Consistency Checker (file name extension: .ccc).

2 files changed, 101 insertions, 0 deletions

diff --git a/ccc/README b/ccc/README
new file mode 100644
index 00000000..c4b36d55
--- /dev/null
+++ b/ccc/README
@@ -0,0 +1,55 @@
+Example Proof General instance for Isabelle
+
+Written by David Aspinall.
+
+Status:	supported as a demonstration only
+
+========================================
+
+
+		"Isabelle Proof General in 30 setqs"
+
+This is a whittled down version of Isabelle Proof General, supplied as
+an (almost) minimal demonstration of how to instantiate Proof General
+to a particular proof assistant.  You can use this as a template to
+get support for a new assistant going. (I did for HOL Proof General).
+
+This mode uses the unadulterated terminal interface of Isabelle, to
+demonstrate that hacking the proof assistant is not necessary to get
+basic features working.
+
+And it really works!  You you get a toolbar, menus, short-cut keys,
+script management for multiple files, a function menu, ability to
+run proof assistant remotely, etc, etc.
+
+To try it out, set in the shell PROOFGENERAL_ASSISTANTS=demoisa
+before invoking Emacs.  (Of course, you need Isabelle installed).
+
+What's missing? 
+
+ 1. A few handy commands (e.g. proof-find-theorems-command)
+ 2. Syntax settings and highlighting for proof scripts
+ 3. Indentation for proof scripts
+ 4. Special markup characters in output for robustness 
+ 5. True script management for multiple files (automatic mode is used)
+ 6. Proof by pointing
+
+How easy is it to add all that?
+
+ 1. Trivial.  2. A table specifying syntax codes for characters
+ (strings, brackets, etc) and some regexps; depends on complexity
+ of syntax.  3. A bit of elisp to scan script; depends on
+ complexity of syntax.  4. Needs hacking in the proof assistant:
+ how hard is to hack your assistant to do this?  5. Depends on file
+ management mechanism in the prover, may need hacking there to send
+ messages. But automatic multiple files may be all you need anyway.
+ 6. Non trivial (but worth a go).
+
+See demoisa.el and demoisa-easy.el for more details.
+
+
+
+========================================
+
+README,v 7.0 2002/08/29 09:12:10 da Exp
+
diff --git a/ccc/ccc.el b/ccc/ccc.el
new file mode 100644
index 00000000..e1398adb
--- /dev/null
+++ b/ccc/ccc.el
@@ -0,0 +1,46 @@
+;; ccc.el - Proof General for the Casl Consistency Checker
+;; 
+;; Author: Christoph Lüth <cxl@informatik.uni-bremen.de>
+;;        
+;; This is a fairly straightforward instantiation of Proof General for
+;; the Casl Consistency Checker, CCC. 
+;;
+;; CASL is the standard algebraic specification language, and CCC is a
+;; tool to check consistency of CASL specifications.
+;; 
+;; For more information, hasten thee browser yonder:
+;;   http://www.informatik.uni-bremen.de/cofi/ccc
+
+(require 'proof-easy-config)            ; nice and easy does it
+
+(proof-easy-config  'ccc "CASL Consistency Checker" 
+ proof-prog-name		 "ccc" ;; must be in your path.
+ proof-terminal-char             ?\;
+ proof-script-comment-start      "(*"
+ proof-script-comment-end        "*)"
+ proof-goal-command-regexp       "^"
+ proof-save-command-regexp       "^qeccc"
+ proof-goal-with-hole-regexp     "ccc \"\\(\\(.*\\)\\)\"" 
+ proof-save-with-hole-regexp     "qeccc \"\\(\\(.*\\)\\)\""
+ proof-non-undoables-regexp      "undo\\|back"
+ proof-goal-command              "ccc \"%s\";"
+ proof-save-command              "qeccc \"%s\";"
+ proof-kill-goal-command         "abort ();"
+ proof-showproof-command         "prt()"
+ proof-undo-n-times-cmd          "undo_steps %s;"
+ proof-auto-multiple-files       t
+ proof-shell-cd-cmd              "cd \"%s\""
+ proof-shell-prompt-pattern      "^\\(CCC\\|^HOL-CASL\\) > "
+ proof-shell-interrupt-regexp    "Interrupt"
+ proof-shell-start-goals-regexp  "^No subgoals\\|^[0-9]* subgoals\\|^Wts:"
+ proof-shell-end-goals-regexp    "val it"
+ proof-shell-quit-cmd            "quit();"
+ proof-assistant-home-page       "http://www.informatik.uni-bremen.de/cofi/tools/ccc"
+ proof-shell-annotated-prompt-regexp  "^\\(val it = () : unit\n\\)?\\(CCC\\|^HOL-CASL\\)> " ;; "^\\(val it = () : unit\n\\)?ML>? "
+ proof-shell-error-regexp        "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
+ proof-shell-init-cmd            ""
+ proof-shell-proof-completed-regexp "^Consistency proof successfully finished."
+ proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" ;;; ???
+)
+
+(provide 'ccc)