Documentation on Using Z with EMTEX LaTex ----------------------------------------- Version 1.1 28 May 1993 Introduction ------------ There are numerous macros available for extending LaTex to set Z and other predicate calculus documents. The file 'oz.tex' by Paul King is very good and demonstrates what can be done. It also incorporates the Object-Z extensions by the University of Queenland. I had a problem with fonts when I tried to run 'oz.tex'. Speaking to others, it seems this is common with would-be users. I am running emtex on a PC, either in a DOS session with extended environment space within OS/2 2.0, or in an OS/2 text screen. I discovered that some fonts are available on Internet (if you know what you need) for immediate use; others have to be massaged before use. I now have a set which works. There are two sets of fonts needed. The former is used to translate from a '.tex' file to a '.dvi' file. A different set is needed to generate a printer file from the '.dvi' file. I have constructed a font library for the hp laser jet printer. You will need another version of the second set if you are not using a laser jet printer. To save others from spending lots of hours on setting up their systems, here is a description of what to do. Differences from Version 1.0 ---------------------------- Version 1.0 was written for emTeX version of late 1990. Since then, another version has been released, in late 1992. The files for my version 1.0 were not all useable with the 1992 release. Specifically, the problem was with the fli file. This has been rectified by changing the name 'amsz.fli' to lj_amsz.fli'. A change to the calling of libraries in config files has required the addition of another config file. To distinguish between the two versions, I have added the year to the file name. Now there is an 'lj1990.cnf' file and an 'lj1992.cnf' file. Associated Files ---------------- You should have the following associated files: texinput.zip This contains style additions to the texinput directory. The files are oz.sty and 3column.sty. The latter is the normal 'threecolumn.sty' with a name change as mentioned below. tfm.zip This contains additional fonts in tfm format. These are used to produce the '.dvi' files. lj_amsz.fli This is a font library for producing laser jet output from the '.dvi' files. (In my version 1.0, this was known as 'amsz.fli'). lj1990.cnf lj1992.cnf These are two versions of the (modified) configuration file used by 'dvihplj'. The file 'lj1990.cnf' is for the 1990 version of emTeX; the file 'lj1992.cnf' is for the 1992 version of emTeX. Select the appropriate one for your system and either use it as a template for modifications to your own, or use it in place of your existing. To use either unchanged, do a "copy a:lj1990.cnf c:\emtex\lj.cnf /v" or "copy a:lj1992.cnf c:\emtex\lj.cnf /v" Of course, you adjust the source and destination drives and destination directory to suit your own preferences. The examples are guides. oz.tex This is a tutorial on using LaTex for Z and test document. This version has 'threecolumn' changed to '3column'. Setting Up ---------- 1. To produce a dvi file: ------------------------- a) Load the style files. Unzip 'oz.sty' and '3column.sty' from 'texinput.zip'. Use 'pkunzip a:texinput' or 'unzip a:texinput'. Copy 'oz.sty' and '3column.sty' into the directory used for 'texinput' styles etc. On emtex, this defaults on installation to '\emtex\texinput'. It should contain files like 'article.sty' and 'book.sty'. Note that on the Internet, '3column.sty' is 'threecolumn.sty'. I changed the name for PC FAT file system use. For the same reason, in 'oz.tex', I changed the reference to 'threecolumn' to '3column'. You can do this process in one step. If the zip file is on drive A:, cd \emtex\texinput pkunzip a:texinput will extract the files into the correct directory. b) Load the dvi fonts. To set up the fonts for the dvi genertion phase, copy the contents of the 'tfm.zip' file into the directory for '.tfm' files. With emtex, this defaults on installation to 'emtex\tfm'. Again, in one step, if the zip file is on drive A:, cd \emtex\tfm a:pkunzip a:tfm will extract the files into the working directory. Now you can run 'latex oz' to generate from 'oz.tex' a file 'oz.dvi'. 2. To produce laser jet output: ------------------------------- a) Copy the font library. The font library is stored with other '.fli' files in a directory set by the environment variable 'DVIDRVFONTS'. This value is set when an initialization batch file is run. The default file is 'set-tex.bat' for DOS or 'set-tex.cmd' for OS/2, and the default value of 'DVIDRVFONTS' is 'c:\texfonts'. To check your current setting, enter 'set' after normal initialization. Find the directory and copy the library 'lj_amsz.fli' into it. (NB: In version 1.0 of this file, the file name was 'amsz.fli'. I have changed the name, but not the contents. If you have already installed the earlier file, you need only to change the name.) I created this library using fontlib and fonts from the AMS ftp server. The name means AMS symbols for Z. b) Modify the configuration file 'lj.cnf'. This file is used by the program 'dvihplj'. The change is on the line where the value '/pl' is set. If you are using the 1990 version of emTeX, append ';lj_amsz' to the line so this library will be searched too. Refer to the sample file 'lj1990.cnf'. If you are running the 1992 version of emTeX, add the name by changing the line '/pl=$DVIDRVFONTS:lj_{0,h,1,2,3,4,5a,5b,sli}' to the line '/pl=$DVIDRVFONTS:lj_{0,h,1,2,3,4,5a,5b,sli,amsz}' Refer to the sample file 'lj1992.cnf'. Alternatively, copy the modified version from my distribution package. If you are using the 1990 version of emTeX, do a 'copy a:lj1990.cnf c:\emtex\lj.cnf /v' or, if you are using the 1992 version, do a 'copy a:lj1992.cnf c:\emtex\lj.cnf /v' (See also the note above in 'Associated Files'.) Now you can run 'dvihplj @lj.cnf '. When dvihplj is loading fonts, there are some warning messages about wrong magnification. The output seems to be ok so these probably need not trouble you. ------------------------------------------------------ Selwyn Russell Information Security Research Centre Faculty of Information Technology Queensland University of Technology 2 George Street Brisbane 4000 Australia Telephone: +61 7 864 1619 Fax: +61 7 221 2384 Internet: selwyn@fitmail.qut.edu.au