If the file starts with two or more comment lines (that is, lines with semicolon as the first non-blank character), or a mixture of blank lines two more comment lines, Proof Pad makes a separate segment in the proof bar for the initial comments. The segment stays white until you click in the proof bar segment first definition (not the comment segment). Then, the comment segment shortens to end with the first comment line and that shortened segment turns dark green with a check mark, as if ACL2 had done a proof.
The ACL2 report for the phantom segment usually says something about the first definition (whose proof bar segment is still gray) being redundant.
The second segment (first "real" segment) doesn't go to ACL2 until you click it again, and the ACL2 report for the segment says the definition is redundant.
There are some other, similar, odd things about the initial segment of the proof bar, which you can see by putting various combinations of comment-lines and blank lines at the beginning of the file.
If the file starts with two or more comment lines (that is, lines with semicolon as the first non-blank character), or a mixture of blank lines two more comment lines, Proof Pad makes a separate segment in the proof bar for the initial comments. The segment stays white until you click in the proof bar segment first definition (not the comment segment). Then, the comment segment shortens to end with the first comment line and that shortened segment turns dark green with a check mark, as if ACL2 had done a proof.
The ACL2 report for the phantom segment usually says something about the first definition (whose proof bar segment is still gray) being redundant.
The second segment (first "real" segment) doesn't go to ACL2 until you click it again, and the ACL2 report for the segment says the definition is redundant.
There are some other, similar, odd things about the initial segment of the proof bar, which you can see by putting various combinations of comment-lines and blank lines at the beginning of the file.