/usr/share/hol88-2.02.19940316/help/ENTRIES/compilet.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 compilet
\TYPE {compilet : (string -> void)}
\SYNOPSIS
Compiles the named ML source file with verbose messages.
\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 verbose.
\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 {compilet `foo`} is the same as {compile (`foo`,true)}.
\SEEALSO
compile, compilet, load, loadf, loadt
\ENDDOC
|