From 7767b6b59850f3eb8372bff7f432980e8a0bd8c7 Mon Sep 17 00:00:00 2001
From: James Yoo <24359440+jyoo980@users.noreply.github.com>
Date: Fri, 29 Sep 2023 12:29:09 -0700
Subject: [PATCH] Update manual with subsection for WPI results (#6209)

---
 docs/manual/inference.tex | 37 +++++++++++++++++++++++++++++++++----
 1 file changed, 33 insertions(+), 4 deletions(-)

diff --git a/docs/manual/inference.tex b/docs/manual/inference.tex
index 0347926af72..2d55d90da57 100644
--- a/docs/manual/inference.tex
+++ b/docs/manual/inference.tex
@@ -139,10 +139,9 @@
 \end{Verbatim}
 
 The result is a set of log files placed in the \<dljc-out/> folder of the
-target project. The results of type-checking with each candidate set of
-annotations will be concatenated into the file \<dljc-out/wpi-stdout.log>; the final
-results (i.e., those obtained using the most precise, consistent set of annotations)
-will appear at the end of this file.
+target project.
+See Section~\ref{wpi-results} for an explanation of the log files generated by
+an invocation of \<wpi.sh>.
 The inferred annotations appear in \<.ajava> files in a
 temporary directory whose name appears in the \<dlcj-out/wpi-stdout.log> file;
 you can find their location by examining the \<-Aajava> argument
@@ -229,6 +228,36 @@
 
 You may need to wait a few minutes for the command to complete.
 
+\subsectionAndLabel{Whole-program inference results}{wpi-results}
+
+The result of invoking \<wpi.sh> are log files stored in the \<dljc-out/> folder
+of the target project.
+The \<dljc-out/> folder contains:
+
+\begin{itemize}
+\item \<typecheck.out>: The final error messages produced by \<javac>,
+  comprising the results of type-checking obtained with the
+  latest iteration of WPI (i.e., using the most precise, consistent set of
+  annotations).
+\item \<build\_output.txt>: Logs collected from compiling the target project
+  without the Checker Framework, using the build file found at the
+  top-level directory.
+\item \<wpi-stdout.log>: The results of type-checking with each candidate set of
+  annotations, concatenated together in the order in which the annotations
+  were inferred.
+  The final results (i.e., those obtained using the most precise, consistent
+  set of annotations) will appear at the end of this file.
+\item \<wpi-stdout-*>: These files are separate from the logs in \<wpi-stdout.log>.
+  They may be useful in the case where \<dljc> is not working as expected.
+\item \<toplevel.log>: The log of the command executed at the top-level of the
+  target directory to invoke whole-program inference.
+\item \<javac.json>: The list of all \<.java> files for which inference was
+  attempted by \<wpi.sh>, and the options passed to \<javac>.
+\item \<stats.json>: Statistics from the invocation of \<wpi.sh> on the target
+  project, including build time, the number of built \<.jar> files, the number of
+  executable \<.jar> files, the number of \<javac> invocations, and the number of
+  source files.
+\end{itemize}
 
 \subsectionAndLabel{Requirements for whole-program inference scripts}{wpi-shared-requirements}