		Search-engine friendly clone of the ACL2 documentation.

Atj-tutorial

Atj-tutorial-screen-output

ATJ tutorial: Control of the Screen Output.

This tutorial page describes the :verbose option of ATJ, which has no effect on the generated Java code but affects the screen output produced by ATJ. This applies to both deep and shallow embedding approaches.

Terse Screen Output

When :verbose is nil, which is the default, ATJ just prints a short completion message about the generated Java files. This is mentioned in the factorial function example in atj-tutorial-deep.

Verbose Screen Output

When :verbose if t, which must be supplied explicitly, ATJ prints, before the short completion messages mentioned above, also additional information about its internal progress. This may be useful to understand better what ATJ is doing, and also for debugging.

As discussed in the factorial example in atj-tutorial-deep, and more generally and systematically in atj-tutorial-translated later, ATJ translates to Java not only the explicitly supplied target function(s), but also the functions that they call directly or indirectly. With the verbose screen output, ATJ displays the list of all such functions.

As discussed in the factorial example in atj-tutorial-deep, ATJ generates Java code to build Java representations of all the ACL2 packages that are known when ATJ is called. The list of these packages is displayed by ATJ when the screen output is verbose.

These two lists, of ACL2 functions and packages, are actually printed twice: once when they are collected, and once when they are translated to Java code. The purpose of this duplication is mainly debugging, and to give an idea of ATJ's progress in case the process takes time. (However, ATJ often runs, and prints the lists, very quickly.) For debugging and for progress indication, ATJ also displays (with verbose screen output), messages as it is generating Java classes, compilation units, and files.

In the factorial example in atj-tutorial-deep, verbose screen output can be displayed via

(java::atj fact :deep t :guards nil :verbose t)

Previous: Customization Options for Generated Code

Next: ACL2 Functions Translated To Java