Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Fri, 18 Dec 1992 13:33:16 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA29921; Fri, 18 Dec 92 05:14:07 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA29916; Fri, 18 Dec 92 05:13:59 -0800 Received: from razorbill.cl.cam.ac.uk (user jg) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Fri, 18 Dec 1992 13:03:11 +0000 To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs, Tom.Melham@uk.ac.cam.cl Subject: Updates to window and pair libraries. Date: Fri, 18 Dec 92 13:03:02 +0000 From: Jim Grundy Message-Id: <"swan.cl.ca.488:18.11.92.13.03.14"@cl.cam.ac.uk> Its been brought to my attention that my pair library is not being compiled as part of the build process of HOL21. (Thanks Ching Tsun for pointing that out). This is because I forgot to put it on the build list in the Library makefile. While fixing this I noticed another problem. It seems a person who shall remain unnamed but who knows who they are and doesn't think RCS is a very good idea and I made a simultaneous update to the Makefiles for documentation to the pair and window libraries :-) . Their change got lost. As a result the documentation for these libraries doesn't build under HOL21. The following shell script will fix all of these propblems. To use it just cut it out, edit it so that it sets the variable HOLDIR to be the top of your HOL directory tree and run it. It changes the following files: ${HOLDIR}/Manual/Libraries/Makefile ${HOLDIR}/Library/Makefile ${HOLDIR}/Library/pair/Manual/Makefile ${HOLDIR}/Library/window/Manual/Makefile ${HOLDIR}/Library/window/Manual/description.tex {fixes a typo too} An unchanged copy of each of these files will be made and given the suffix ".orig". Sorry for this Jim --------------------------8< CUT HERE 8<------------------------------ #!/bin/sh # HOLDIR should be the base of the HOL directory tree. HOLDIR=/usr/groups/hol/HOL21/src patch -d ${HOLDIR}/Library << LIB_MAKE_PATCH Index: Makefile 41c41 < latex-hol abs_theory reals window UNITY --- > latex-hol abs_theory reals window UNITY pair LIB_MAKE_PATCH patch -d ${HOLDIR}/Manual/Libraries << MAN_MAKE_PATCH Index: Makefile 9c9 < string taut trs unwind window --- > string taut trs unwind window pair MAN_MAKE_PATCH patch -d ${HOLDIR}/Library/pair/Manual << PAIR_MAN_MAKE_PATCH Index: Makefile 19c19 < MAKEINDEX=../../../Manual/Reference/bin/makeindex --- > MAKEINDEX=../../../Manual/LaTeX/makeindex ../../../ 32a33,35 > tex: ids theorems > @echo "TeX files made" > 45c48 < \${MAKEINDEX} -o index.tex pair --- > \${MAKEINDEX} pair.idx index.tex 52,53c55 < make ids; \\ < make theorems; \\ --- > make tex; \\ PAIR_MAN_MAKE_PATCH patch -d ${HOLDIR}/Library/window/Manual << WIN_MAN_MAKE_PATCH Index: Makefile 19c19 < MAKEINDEX=../../../Manual/Reference/bin/makeindex --- > MAKEINDEX=../../../Manual/LaTeX/makeindex ../../../ 32a33,35 > tex: ids theorems > @echo "TeX files makde" > 47c50 < \${MAKEINDEX} -o index.tex window --- > \${MAKEINDEX} window.idx index.tex 54,55c57 < make ids; \\ < make theorems; \\ --- > make tex; \\ WIN_MAN_MAKE_PATCH patch -d ${HOLDIR}/Library/window/Manual << WIN_MAN_DES_PATCH Index: description.tex 898c898 < \\end{verbatim}\\end{boxed} --- > \\end{verbatim}\\end{boxed}\\index{store\\_rule@{\\ptt store\\_rule}|)} WIN_MAN_DES_PATCH