/usr/share/hol88-2.02.19940316/help/ENTRIES/compilef.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | \DOC compilef
\TYPE {compilef : (string -> void)}
\SYNOPSIS
Compiles an ML source file `silently'.
\DESCRIBE
Given a string {`name`}, {compile} loads the named file, and then compiles it
into LISP generating a file {name_ml.l}. It then calls the LISP compiler to
create an object file {name_ml.o}. The intermediate LISP file is automatically
deleted once the {name_ml.o} file has been generated. Loading and compilation
are silent.
\FAILURE
Fails if the named ML source file does not exist, or if the load is
unsuccessful. In the latter case, the intermediate {name_ml.l} file is
left undeleted.
\COMMENTS
The function call {compilef `foo`} is the same as {compile (`foo`,false)}.
\SEEALSO
compile, compilet, load, loadf, loadt
\ENDDOC
|