# AgentPMT - Frequently Asked Questions

Total: 7 questions

## General

### Can I upload `lakefile.lean`, `lean-toolchain`, or my own build configuration?
No. The platform pins the Lean toolchain and exporter runtime for you. Do not include `lakefile.lean`, `lean-toolchain`, `lake-manifest.json`, or `.lake/` in the uploaded archive.

### Does this compile any Lean program?
No. The selected definition must elaborate to `HeytingLean.LeanCP.CProgramDecl`, which is the exportable LeanCP program form supported by the current compiler path.

### What do I upload to Proof Code Compiler?
Upload a `.zip` whose top-level folder is `UserProofs/` and whose contents are Lean source files only. A single-file project can be as small as `UserProofs/Main.lean`.

### What do `entry_module` and `entry_symbol` mean?
`entry_module` is the Lean module imported from your uploaded source tree, such as `UserProofs.Main`. `entry_symbol` is the definition exported from that module, such as `exportProgram`.

### What is the difference between `fast` and `full` verification?
`fast` checks certificate details and hashes without rebuilding. `full` rebuilds and re-exports under the pinned runtime, then compares the regenerated output with the stored artifact for stronger assurance.

### What should I save after a successful generation?
Save the generated output file, the certificate, the generation log, and especially `artifacts.bundle.file_id`. The bundle is what you need for later verification.

### Which target should I choose?
Use `c` when you want the broadest and lowest-risk support. Use `rust` when you want the same export path with Rust output. Use `wasm` only when you are comfortable with the current target being more constrained than `c`.