1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
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 <dvi file>'.
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
|
