learn about macros

Stream: general

[Paul-Nicolas Madelaine]

Hi everyone,

I've heard about macros in Lean, but I don't exactly know what they are or how they work, except that you can assimilate them with various trust levels. They are not mentioned in the lean tutorial, so what would be a good place to read about them?

[Simon Hudon]

To build macros, you really have to work inside Lean itself. It's not really exposed to meta programming

[Simon Hudon]

What application do you have in mind?

[Paul-Nicolas Madelaine]

I wrote a tactic working by reflexivity, inspired from the ring tactic in Coq.
but it's using rationals as constants and can be quite slow.
@Rob Lewis mentioned that macros could be used to do the computation more efficiently, running the tactic in the kernel only if that's required, depending on the level of trust.

[Paul-Nicolas Madelaine]

of course a more direct solution would be to first write a more efficient definition of rat, but he mentioned the macros and I wanted to learn more about them

[Keeley Hoek]

I've had some limited rational programming experience, and there were huge speedups by locally inlining the rat computation functions if I recall

[Paul-Nicolas Madelaine]

@Keeley Hoek how can I do this? I've never used inlining

[Keeley Hoek]

local attribute [inline] <idents> is all there is too it, that has to appear before the functions using the functions you are inlining are defined. It is useful to look at the generated bytecode to see if more should be inlined after. To do that, use set_option trace.compiler.code_gen true

[Paul-Nicolas Madelaine]

thanks!

[Rob Lewis]

Rob Lewis mentioned that macros could be used to do the computation more efficiently, running the tactic in the kernel only if that's required, depending on the level of trust.

Could possibly be used. I don't actually know if there's any way to do this in practice.

[Rob Lewis]

I've had some limited rational programming experience, and there were huge speedups by locally inlining the rat computation functions if I recall

Inlining will only affect computation in the VM though, right? This is good to know for future reference, but unfortunately we're dealing with kernel computation here.

[Paul-Nicolas Madelaine]

Rob Lewis mentioned that macros could be used to do the computation more efficiently, running the tactic in the kernel only if that's required, depending on the level of trust.

Could possibly be used. I don't actually know if there's any way to do this in practice.

yes, sorry that's what I meant.
I meant to use the past as conditional, but in this case I guess it doesn't work