TELES START Prompt Template#

Copy and adapt the template below to begin a TELES session. Fill in the bracketed fields. The session is active from the moment START is declared until STOP is declared (see TELES STOP Prompt Template).

TELES START

Session:     [descriptive name, e.g., "b15 compound naming migration"]
Date:        [YYYYmMMdDD]
Authorized:  [who authorized this, e.g., "LLoL"]
Scope:       [what files/directories are in scope]
Operation:   [what TELES will do, e.g., "fix title underlines",
              "rename identifiers A# to ax#_A#"]

Safety contract:
- TELES may fix RST formatting errors (indentation, heading underlines,
  blank lines) that do NOT alter formal content (axioms, theorems,
  symbol definitions, equations, formal proofs).
- Within this session (before STOP), TELES may also rename labels and
  cross-references that this session itself introduced, if the rename
  serves transparency (see DD b14).
- Every repair must be documented: either a dated TELES error admonition
  in each affected file, or a summary in the session llog.
- If in doubt whether a change touches formal content: DO NOT MAKE IT.
  Flag it for human review instead.

Begin.

Usage Notes#

  • One START per session. Do not nest TELES sessions.

  • The scope field bounds what TELES may touch. Files outside scope require explicit authorization.

  • The session llog should be created immediately after START, recording the full prompt and initial state.

  • If the session discovers issues outside its scope, log them as AA tasks for a future session rather than expanding scope silently.