I-AM-HERE

Major Section:  MISCELLANEOUS

Example Input File for Rebuild:
(defun fn1 (x y) ...)
(defthm lemma1 ...)
(defthm lemma2 ...)
(i-am-here)
The following lemma won't go through.  I started
typing the hint but realized I need to prove a
lemma first.  See the failed proof attempt in foo.bar.
I'm going to quit for the night now and resume tomorrow
from home.


(defthm lemma3 ...
  :hints (("Goal" :use (:instance ???
...

By putting an (i-am-here) form at the ``frontier'' of an evolving file of commands, you can use rebuild to load the file up to the (i-am-here). I-am-here simply returns an ld error triple and any form that ``causes an error'' will do the same job. Note that the text of the file after the (i-am-here) need not be machine readable.