Acces environment from command macro

Stream: lean4

[Patrick Massot]

If I want to write a user command using macro, is it possible to access the current environment (at macro execution time, not macro writing time)?

[Sebastian Ullrich]

No, that's the point where you should switch to elab

[Patrick Massot]

Is there a nice example of doing that?

[Sebastian Ullrich]

#find perhaps? https://github.com/leanprover-community/mathlib4/blob/876d9cc42ccbfea023752e40e6edb7279d9c6b5a/Mathlib/Tactic/Find.lean#L67
There's a lot of other stuff about matching types happening there of course

[Sebastian Ullrich]

Depending on what information you need, you probably don't need the liftTermElabM

[Patrick Massot]

Thanks!

[Patrick Massot]

I'm still stuck because I don't know how to mix macro style and elab style. Say I want my custom namespace command where part of the created name comes from the environment. I can do the easy case where that part is actually hard-coded.

import Lean

open Lean Meta

macro "foo" n:num : command =>
  `(namespace $(mkIdent $ Name.str `hard_coded ("bar" ++ toString n.getNat)))

foo 1
def x := 3

end hard_coded.bar1

Now I would like to replace hard_coded in the above macro by the value of head` taken from the environment at command running time. The naive version is

macro "foo" n:num : command =>
  `(namespace $(mkIdent $ Name.str $head ("bar" ++ toString n.getNat)))

which doesn't work at all. Then I tried something like

open Lean Elab in
elab "foo'" n:num : command => do
  let env : Environment ← liftMacroM $ pure (← getEnv)
  match env.find? `head with
  | some decl => `(namespace $(mkIdent $ Name.str $(decl.name) ("bar" ++ toString n.getNat)))
  | none => throwError "Failed"

which doesn't make any sense.

[Mario Carneiro]

@Patrick Massot What is "head" in this example? Is it a global definition? What does the user side code look like?

[Mario Carneiro]

it sounds like you might want to resolve head at elab time, in which case you would call resolveName or one of its friends

[Patrick Massot]

The user code would be

def head := "no_hard_coded"
foo' 2
end not_hard_coded.bar2

[Mario Carneiro]

import Lean
import Mathlib.Util.TermUnsafe

open Lean Meta Elab Command

elab "foo" n:num : command => do
  let [(head, _)] ← resolveGlobalName `head | throwError "head not found or overloaded"
  let head ← unsafe evalConstCheck Name ``Name head
  elabCommand (← `(namespace $(mkIdent $ Name.str head ("bar" ++ toString n.getNat))))

def head : Name := `not_hard_coded

foo 1
def x := 3
end not_hard_coded.bar1

[Mario Carneiro]

resolveGlobalName is not the most convenient function to call, there should be a better one somewhere

[Patrick Massot]

Thanks! What needs mathlib here?

[Sebastian Ullrich]

The unsafe term macro

[Mario Carneiro]

I just fixed it

[Mario Carneiro]

I want to PR that to core, it comes up all the time

[Patrick Massot]

I was also missing elabCommand. I searched for it but couldn't find it.

[Mario Carneiro]

as you can see, using elabCommand makes it easy to turn a macro into an elab

[Mario Carneiro]

same thing for elabTactic or elabTerm

[Mac]

Mario Carneiro You should probably be using withMacroExpansion in your example to make sure the macro stack is setup properly:

elab "foo" n:num : command => do
  let [(head, _)] ← resolveGlobalName `head | throwError "head not found or overloaded"
  let head ← unsafe evalConstCheck Name ``Name head
  let cmd ← `(namespace $(mkIdent $ Name.str head ("bar" ++ toString n.getNat)))
  withMacroExpansion (← getRef) cmd <| elabCommand cmd

[Mac]

Mario Carneiro said:

I want to PR that to core, it comes up all the time

I think the major problem is that evalConst does not do the usual unsafe/implementedBy split done by most other unsafe code. It unsafety being hidden behind an opaque is always the behavior I want in any of my use cases.

[Mario Carneiro]

I'm not sure what you mean. evalConst should definitely be an unsafe function, it directly causes unsafety if you call it wrong

[Mario Carneiro]

A safe interface for evalConst would be great; I think it could be an elab that checks the expected type and synthesizes the expr version to ensure no discrepancy

[Mario Carneiro]

In any case, the thing that I want to PR is term-mode unsafe - evalConst is not specifically the motivator here, but rather the unsafe/implementedBy trick that comes up many dozens of times in the lean 4 codebase

[Mac]

Mario Carneiro said:

I'm not sure what you mean. evalConst should definitely be an unsafe function, it directly causes unsafety if you call it wrong

Yes, but it should be an the unsafe version should be unsafeEvalConst with the user evalConst being an standard implementedBy wrapper. At least, that is always what I want when I use it.

[Mac]

Mario Carneiro said:

In any case, the thing that I want to PR is term-mode unsafe - evalConst is not specifically the motivator here, but rather the unsafe/implementedBy trick that comes up many dozens of times in the lean 4 codebase

I know, and I agree. However, I think evalConst is unique in that it is one of the few places the unsafety bleeds into user code in burdensome manner. Most other usages in the Lean core utilize the unsafe/implementedBy trick to make this more convenient for the end-user (and not require them write dozens of such tricks themselves).

[Mario Carneiro]

Mac said:

Mario Carneiro said:

I'm not sure what you mean. evalConst should definitely be an unsafe function, it directly causes unsafety if you call it wrong

Yes, but it should be an the unsafe version should be unsafeEvalConst with the user evalConst being an standard implementedBy wrapper. At least, that is always what I want when I use it.

What I'm saying is that there can't be a safe version of evalConst, that would just be unsound

[Mario Carneiro]

at least, not with the signature it has

[Mario Carneiro]

the safe version, as I said, would have to be part-macro in order to ensure that the expected type actually matches the provided Expr

[Mario Carneiro]

even evalConstCheck is only "slightly less unsafe", because it fundamentally can't check this as a regular function

[Mac]

Mario Carneiro said:

that would just be unsound

It would not be unsound, the implementedBy prohibits that already, it would be memory unsafe, though. But that's fine, one naturally is assuming the value is of the expected type to do the evaluation in most use cases.

[Mac]

As your example demonstrate, we generally discard this potentially unsafety in use cases.

[Mario Carneiro]

Mac said:

It would not be unsound, the implementedBy prohibits that already, it would be memory unsafe, though.

Yes, that's what I mean by unsound. unsafe isn't just line noise, it has meaning and you shouldn't just be wrapping it with a safe wrapper unless you are preventing the memory safety issue from leaking

[Mario Carneiro]

Mac said:

As your example demonstrate, we generally discard this potentially unsafety in use cases.

In use cases, we can confirm that the unsafety is encapsulated. In my example we can see that it is safe because I used Name and ``Name as parameters

[Mario Carneiro]

so the unsafe is exactly where it should be in this example

[Mac]

Mario Carneiro said:

In use cases, we can confirm that the unsafety is encapsulated. In my example we can see that it is safe because I used Name and ``Name as parameters

Note that this is not true, (as mentioned in the documentation for evalConst):

This function is only safe to use if the type matches the declaration's type in the environment
and if `enableInitializersExecution` has been used before importing any modules

The key here is "if the type matches the declaration's type in the [provided] environment" . In your example, there is no fool-proof guarantee that the type Name in the environment (which is arbitrary environment accepted at the run time of the command) matches that of the type Name mentioned at the use site (which is fixed to the Name of compile time elaboration environment). For example, if this elab command was used as a pluign in a prelude module with a different definition for Lean.Name, it could cause memory unsafety. Or, if the olean was used with a different Lean version where the name definition changed (as it recently did), it could also cause memory unsafety.

In summary, the safety guarantee for evalConst is essentially unmeetable. Every practical use of its still introduces the possibility of memory unsafety.

[Mario Carneiro]

In your example, there is no fool-proof guarantee that the type Name in the environment (which is arbitrary environment accepted at the run time of the command) matches that of the type Name mentioned at the use site (which is fixed to the Name of compile time elaboration environment).

The environment has to be an extension of the current compile time environment in order to call this function.

[Mario Carneiro]

If the oleans don't match, then you are already in UB territory. Lean provides no guarantees in this case

[Mac]

Mario Carneiro said:

The environment has to be an extension of the current compile time environment in order to call this function.

No it does not (at least with the use of plugins). Just like one can use (and does use) builtin Lean elaborates without importing all of Lean. Furthermore, even an extension of the environment could modify the meaning of Name (that would be extremely hacky and probably break other things, but it is still possible).

[Mario Carneiro]

Furthermore, even an extension of the environment could modify the meaning of Name (that would be extremely hacky and probably break other things, but it is still possible).

You can't remove or change definitions in the environment, that is something the kernel itself prevents

[Mario Carneiro]

As for plugins, I would call that an unsafe feature. You have to abide by certain rules when using plugins to avoid memory unsafety

[Mario Carneiro]

you can get all sorts of link errors that way

[Mac]

@Mario Carneiro The environment's constants are just stored in an SMap, they are perfectly modifiable (though I don't doubt that would cause major problems elsewhere).

[Mac]

Actually, based on this comment in SMap, supporting deletions would not be that hard. So maybe it wouldn't break tons of things elsewhere.

[Mario Carneiro]

the comment says that it would require changing the definition of the map to have Option keys

[Mario Carneiro]

in other words, they aren't really being deleted, only hidden from the frontend

[Mac]

@Mario Carneiro yes, to properly efficiently support them in the core. You could still overwrite the whole map to do so if you wanted.

[Mario Carneiro]

I still wouldn't put the blame for this on evalConst, those are some unsafe operations you are doing

[Mac]

Mario Carneiro said:

in other words, they aren't really being deleted, only hidden from the frontend

That second map is for local declarations, it is then compacted into the first map on a import. So, after an import, I think it would be deleted?

[Mario Carneiro]

it's not implemented so it's difficult to speculate on what exactly it would do

[Mario Carneiro]

like, you can also just add things to the environment without calling the kernel too

[Mario Carneiro]

or you could override the toplevel to play tetris instead

[Mario Carneiro]

at some point you aren't really using lean anymore

[Mario Carneiro]

and if you get into trouble it's on you

[Mac]

Mario Carneiro said:

I still wouldn't put the blame for this on evalConst, those are some unsafe operations you are doing

Since you didn't like my reasonable (imo) example of plugins and my hacky example of an environment modifications, here is another one: running the elaborator on a external environment. For instance, if we are in the process of elaborating an external file (ala runFrontend) and wish to execute this elaborator (or a set of elaborators in general including this one) on some synthetic syntax related to the file (and thus in its environment) the eval would also break.

[Mario Carneiro]

This command and many others like it do not support that use case

[Mario Carneiro]

if you try to use it anyway that's on you

[Mario Carneiro]

unsafe is a way of saying "don't come to me if your hacks don't work"

[Mac]

UB in certain use cases is generally what "unsafe" means.

[Mario Carneiro]

importModules is unsafe for this reason

[Mac]

importModules is not unsafe?

[Mario Carneiro]

withImportModules

[Mac]

which is not generally used directly when augmenting the frontend?

[Mario Carneiro]

lean isn't very bulletproof esp. if you try writing your own prelude

[Mario Carneiro]

time being finite and all that

[Mario Carneiro]

but the notion of what is unsafe or not for the purpose of "blame assignment" is fairly well trodden in e.g. rust, and lean is trying to follow the same patterns

[Mac]

Regardless, my general point, is that by bypassing the unsafe in your example, what the user is stating that they don't care about the edge cases where the behavior may still be unsafe, not that they have reasonably verified that any such case is now impossible. Which is fine, but is an important distinction in guarentees.

[Mac]

In that vein, I am not sure what the unsafe adds in that code, it is essentially silently introducing an equivalent to the common unsafe/implementedBy trick for every use case of the evalConst* without preforming additional verification to ensure it is less unsafe. I don't understand how that would be more useful than just do that trick at the definition of evalConst (or evalConstCheck) since that is generally always the way it will be used.

That isn't to say I think the term level unsafe is useless in general (it is a great idea that removes a lot of burdensome boilerplate). I just think the evalConst is one place where the unsafe should be hidden away and mentioned in the docstring, as it will be just be hidden away at all its use sites otherwise.

[Mac]

Though, I guess that last comment is more relevant now without the term-level unsafe in the Lean core, than once it is there. Because currently hiding it away takes a lot of boilerplate. With the unsafe macro, it just takes one keyword (which admittedly does nicely documented to the read of the code that the function being used is introducing unsafety).

[Mario Carneiro]

Mac said:

In that vein, I am not sure what the unsafe adds in that code, it is essentially silently introducing an equivalent to the common unsafe/implementedBy trick for every use case of the evalConst* without preforming additional verification to ensure it is less unsafe.

This is rust-style verification: you read the code carefully and convince yourself that it is correct. The unsafe alerts you to the possibility that something that requires additional scrutiny is going on. Lean-style verification would have proof side conditions and for most memory safety issues in lean that's not an option because the side conditions cannot be expressed in the lean logic.

I don't understand how that would be more useful than just do that trick at the definition of evalConst (or evalConstCheck) since that is generally always the way it will be used.

Of course, if the trick could be done in the definition of evalConst it should be placed there, but the point is that it can't be because the type is generic in evalConst and it is not generic in the user code.

[Mario Carneiro]

Like I said, I think it can be done in general but you would need to use a macro to automate the matching of type to expr, or possibly a typeclass like the reflect typeclass that did it in lean 3

[Mac]

Mario Carneiro said:

Like I said, I think it can be done in general

Assuming that you are okay disregarding cases like plugins, elaborators, and environment changes that I mentioned above. One reason I point this out is that this is the case for Lake which uses evalConst extensively in such a scenario (on a separately elaborated environment -- that of the configuration file).

[Mac]

Mario Carneiro said:

or possibly a typeclass like the reflect typeclass that did it in lean 3

You could use the toTypeExpr of the ToExpr class for this (I have done this is some places).

[Mac]

Though, for cases like this, it might be best to separate toTypeExpr from ToExpr, since there are many cases where a type of a value is reflectable even if the value is not.

[Mac]

Mario Carneiro said:

Of course, if the trick could be done in the definition of evalConst it should be placed there, but the point is that it can't be because the type is generic in evalConst and it is not generic in the user code.

Huh, yes it can? The following definitions compile just fine:

@[implementedBy Lean.Environment.evalConst] opaque evalConst'
(α) (env : @& Environment) (opts : @& Options) (type : @& Name) : Except String α

@[implementedBy Lean.Environment.evalConstCheck] opaque evalConstCheck'
(α) (env : Environment) (opts : Options) (type : Name) (const : Name) : ExceptT String Id α

[Mario Carneiro]

That's not made it any safer though, so taking the unsafe off is not correct

[Mario Carneiro]

if you can make it safer then you can take the unsafe off

[Gabriel Ebner]

Mac said:

Mario Carneiro said:

or possibly a typeclass like the reflect typeclass that did it in lean 3

You could use the toTypeExpr of the ToExpr class for this (I have done this is some places).

This is just as unsafe as calling evalConst directly, since you can safely construct any (unlawful) ToExpr instance.

[Sebastian Ullrich]

Mac said:

One reason I point this out is that this is the case for Lake which uses evalConst extensively in such a scenario (on a separately elaborated environment -- that of the configuration file).

This is a interesting case though since you're probably not concerned about alternative implementations of those imports in Lake. So you could check whether the imports are resolved to the olean files you expect them to.

[Sebastian Ullrich]

For the general case I don't see a better safe solution than comparing deep hashes of the type's structure. It's the same problem as how to detect .olean structure incompatibilities.