Commit graph

8 commits

Author SHA1 Message Date
Sebastian Ullrich
3770808b58
feat: split Lean.Kernel.Environment from Lean.Environment (#5145)
This PR splits the environment used by the kernel from that used by the
elaborator, providing the foundation for tracking of asynchronously
elaborated declarations, which will exist as a concept only in the
latter.

Minor changes:
* kernel diagnostics are moved from an environment extension to a direct
environment as they are the only extension used directly by the kernel
* `initQuot` is moved from an environment header field to a direct
environment as it is the only header field used by the kernel; this also
makes the remaining header immutable after import
2025-01-18 18:42:57 +00:00
Leonardo de Moura
66304d83a0 chore(library/init/lean/compiler): export as C functions 2019-08-17 06:58:36 -07:00
Leonardo de Moura
34ca44cca1 chore(frontends/lean,library): remove unnecessary #includes and dead code 2019-06-26 11:36:23 -07:00
Leonardo de Moura
45dc2cd49a feat(library/init/lean/compiler): [export] attribute in Lean 2019-06-24 15:48:12 -07:00
Leonardo de Moura
f852cd774f feat(library/init/lean/compiler/ir): expose C++ primitives for accessing export and extern attributes 2019-05-20 15:49:03 -07:00
Sebastian Ullrich
a6ac98966a refactor(library/attribute_manager): parse attribute data from pexpr instead of abstract_parser 2019-02-15 12:13:45 -08:00
Leonardo de Moura
e8758a1707 chore(library/compiler/export_attribute): exporting constructors is messy
It is much simpler and only slightly more verbose to export an
auxiliary function that just invokes the constructor.
2019-02-09 18:00:27 -08:00
Leonardo de Moura
bf15ee48fd refactor(library/compiler): export_name ==> export_attribute 2019-02-09 17:59:46 -08:00