namespace, alias and open_locale

Stream: metaprogramming / tactics

[Huajian Xin]

I'm working with building interface between LEAN and Python for automated theorem proving and trying to extract information and setting the proving environment, but many difficulties emerge.

1. Is there any metaprogramming method to declare that "the current proof is within a specific namespace" like we declare "namespace" and "end" in lean file? To my knowledge there is only tactic.set_env (env.execute_open some_namespaces) in init/meta/tactic.lean with seems behave like open.
2. Is there any metaprogramming method to make declaration open_locale?
3. Is there any metaprogramming method to collect declared alias information?
   Any reply or explaination would be appreciated! And if anyone want to build this project with me please contact me xinhj@mail2.sysu.edu.cn, thanks!

[Jannis Limperg]

You might want to do your interface for Lean 4 instead of Lean 3. Both because Lean 3 will be obsolete soon-ish and because the metaprogramming API of Lean 4 is a lot more expressive than that of Lean 3.

[Huajian Xin]

Jannis Limperg said:

You might want to do your interface for Lean 4 instead of Lean 3. Both because Lean 3 will be obsolete soon-ish and because the metaprogramming API of Lean 4 is a lot more expressive than that of Lean 3.

Thanks! Good suggestions

[Patrick Massot]

My recommended path is:

• Read https://leanprover.github.io/functional_programming_in_lean/
• Read https://github.com/arthurpaulino/lean4-metaprogramming-book
• Have a look at https://github.com/PatrickMassot/lean4-game-server for inspiration about how to interact with Lean 4 in a non-editor way

Of course this includes asking tons of questions in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4 when needed