Feature request: emit #line directives in generated C code for source-level debugging

Summary

The Lean 4 C code generator (EmitC.lean) produces C code without #line preprocessor directives. This means DWARF debug info in compiled binaries references the generated .c files rather than the original .lean source files, making source-level debugging impossible.

Current behavior

When compiling a Lean program with debug flags (moreLeancArgs := #["-g"]), the resulting binary's DWARF .debug_line section maps to the intermediate Main.c file (e.g., .lake/build/ir/Main.c), not the .lean source.

The generated C files contain no #line directives:

// Lean compiler output
// Module: Main
// Imports: public import Init
#include <lean/lean.h>
// ... pure C code with no source location markers ...

Requested behavior

Add #line directives to the generated C code that map back to the corresponding .lean source positions:

#line 6 "Main.lean"
LEAN_EXPORT lean_object* l_calculateSum(lean_object* x_1, lean_object* x_2) {
    // ...
}

This is a standard C preprocessor feature (C11 §6.10.4) supported by all C compilers. Many language implementations that compile through C use this technique (e.g., Cython, GHC's -via-C backend).

Motivation

We're building CodeTracer, a time-travel debugger that supports multiple languages through RR + LLDB. Lean programs can be recorded and replayed, but without source mapping in the DWARF info, we cannot:

• Set breakpoints on .lean source lines
• Show the current position in .lean source during stepping
• Extract flow/omniscience data mapped to Lean source locations

This single change would unblock source-level debugging for Lean in any debugger (LLDB, GDB, CodeTracer, etc.).

Implementation notes

The change would be in src/Lean/Compiler/IR/EmitC.lean. The compiler IR already tracks declaration names — the missing piece is threading source position (Syntax.Pos or Position) information through the IR pipeline and emitting #line directives at function boundaries (and ideally at statement granularity).

A minimal version could emit #line only at function definition boundaries, which would at least enable function-level breakpoints.

Start with src/Lean/Compiler/IR/EmitC.lean and inspect how declaration names are emitted and where source positions are available in the IR pipeline. Trace the path from source positions to generated function definitions, then verify that compiled debug output maps function boundaries back to the corresponding .lean files and lines.