From 530b776697af07850b91553c73355ee8c3ce0d31 Mon Sep 17 00:00:00 2001 From: Healfdene Goguen Date: Thu, 14 May 1998 11:49:29 +0000 Subject: Updated install script after finding problems with Savi's setup. --- INSTALL | 36 ++++++++++++++++++++++++++++-------- 1 file changed, 28 insertions(+), 8 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 10881ad8..d3ad3e70 100644 --- a/INSTALL +++ b/INSTALL @@ -1,15 +1,29 @@ -Put the compiled emacs files and the file script-management.info in a -suitable directory for local emacs files, as suggested by your system -administrator. Otherwise, alter the coq-info-dir in coq.el to a -hard-coded path where you put the file script-management.info. +This file describes what to do to be able to run our script management +mode for xemacs. Please let us know if you have any problems in +trying to install it. Check the values of coq-tags and coq-prog-name in coq.el to see that they correspond to the paths for coqtop and the library on your system. -To install, put the .el files in an appropriate directory and compile -them using `byte-compile-file' in xemacs: +To install, begin by making sure that your load-path has the current +directory in it by typing: + load-path C-j +in the *scratch* buffer. If it does not, type: + (setq load-path (cons "." load-path)) C-j +again in the *scratch* buffer (or add it to your .emacs file). + +Then put the .el files in an appropriate directory and compile them +using `byte-recompile-file' in xemacs: M-0 M-x byte-recompile-directory +Put the compiled emacs files and the file script-management.info in a +suitable directory for local emacs files, as suggested by your system +administrator. Otherwise, if you prefer to keep your own private +copy, alter the variable coq-info-dir in coq.el to that directory and +add the line: + (setq load-path (cons load-path)) +to your .emacs file, where is your local directory. + If you want to use this mode for Coq, you need to make sure you have an appropriate version, which is from later than 1 March 1998. @@ -17,9 +31,10 @@ Install coqtags or legotags in a standard place. If you are running Coq, generate a TAGS file for the library by running coqtags `find . -name \*.v -print` -in the root directory of the library, $COQTOP/theories. +in the root directory of the library, $COQTOP/theories. If you are +running LEGO, do the same using legotags in the appropriate directory. -Finally, you may want to add the following lines to your .emacs file: +Finally, you should add the following lines to your .emacs file. ;;; LEGO and Coq (setq auto-mode-alist @@ -34,3 +49,8 @@ Finally, you may want to add the following lines to your .emacs file: ; Tags is unusable with Coq library otherwise: (setq tag-always-exact t) + +After this, simply load a LEGO or Coq file and the appropriate mode +will be run automatically. + +Healfdene GOGUEN -- cgit v1.2.3