What an author writes next to a def #

A package is a namespace of ordinary Lean defs, each marked @[ship], and one ship_package under them. Marking a def reads the declaration out of it; ship_package gathers those into the program, writes the certificate saying each one denotes the def it came from, and puts up the wall emit puts up. None of it is a shortcut — the declarations and the certificates come out of the same walk, so a declaration cannot reach the program without one.

The certificates are written after the program because a certificate names it: a declaration that calls another goes through p.find?.