lean4-htt/src/Lean/Compiler/IR
Sebastian Ullrich 719765ec5c
feat: overhaul meta system (#10362)
This PR refines and clarifies the `meta` phase distinction in the module
system.

* `meta import A` without `public` now has the clarified meaning of
"enable compile-time evaluation of declarations in or above `A` in the
current module, but not downstream". This is now checked statically by
enforcing that public meta defs, which therefore may be referenced from
outside, can only use public meta imports, and that global evaluating
attributes such as `@[term_parser]` can only be applied to public meta
defs.
* `meta def`s may no longer reference non-meta defs even when in the
same module. This clarifies the meta distinction as well as improves
locality of (new) error messages.
* parser references in `syntax` are now also properly tracked as meta
references.
* A `meta import` of an `import` now properly loads only the `.ir` of
the nested module for the purposes of execution instead of also making
its declarations available for general elaboration.
* `initialize` is now no longer being run on import under the module
system, which is now covered by `meta initialize`.
2025-09-17 21:04:29 +00:00
..
AddExtern.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Basic.lean chore: remove unused FnBody.mdata constructor (#9564) 2025-07-26 15:20:13 +00:00
Borrow.lean chore: fix indentation (#9936) 2025-08-16 05:30:36 +00:00
Boxing.lean chore: use dotted constructor names (#10074) 2025-08-23 04:52:19 +00:00
Checker.lean chore: use ofConstName in error messages (#10121) 2025-08-25 23:20:36 +00:00
CompilerM.lean feat: overhaul meta system (#10362) 2025-09-17 21:04:29 +00:00
ElimDeadBranches.lean perf: do not export LCNF/IR function summaries under the module system (#9645) 2025-07-31 15:23:04 +00:00
ElimDeadVars.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
EmitC.lean perf: do not export opaque bodies (#10119) 2025-08-27 20:59:59 +00:00
EmitLLVM.lean chore: remove unused FnBody.mdata constructor (#9564) 2025-07-26 15:20:13 +00:00
EmitUtil.lean chore: clean up IR.Arg usage (#9557) 2025-07-26 00:22:38 +00:00
ExpandResetReuse.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Format.lean fix: do not allow access to private primitives in public scope (#9890) 2025-08-14 15:34:54 +00:00
FreeVars.lean refactor: use a state monad rather than combinators for computing free indices (#9711) 2025-08-04 13:55:41 +00:00
LiveVars.lean chore: rewrite LiveVars in a monadic style (#9745) 2025-08-05 21:49:43 +00:00
LLVMBindings.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Meta.lean feat: overhaul meta system (#10362) 2025-09-17 21:04:29 +00:00
NormIds.lean chore: remove unused FnBody.mdata constructor (#9564) 2025-07-26 15:20:13 +00:00
PushProj.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
RC.lean perf: avoid ref count increments for borrowed array accesses (#9866) 2025-08-12 05:27:35 +00:00
ResetReuse.lean perf: disable reuse when a value's last use is an owned argument (#10017) 2025-08-21 00:41:56 +00:00
SimpCase.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Sorry.lean chore: replace partially redundant calls to FnBody.split with .body (#9568) 2025-07-26 20:18:37 +00:00
ToIR.lean chore: remove special case for extern constructors (#10257) 2025-09-05 06:08:45 +00:00
ToIRType.lean fix: make IO.RealWorld opaque (#9631) 2025-09-08 18:12:19 +00:00
UnboxResult.lean refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00