The meaning of `@&` in source code of Lean?

Stream: general

[White Chen]

In ./src/Lean/Environment.lean, we have:

/--
  Evaluate the given declaration under the given environment to a value of the given type.
  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. -/
@[extern "lean_eval_const"]
unsafe opaque evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α

What's the meaning of @& in the code given above?

[Derek Rhodes]

Hi White, from the FFI docs, in the borrowing section, it says:

To reduce reference counting overhead, parameters can be marked as borrowed by prefixing their type with @&.

[Kyle Miller]

If you hover over it, the docstring has an explanation.

[Kyle Miller]

Indicates that an argument to a function marked @[extern] is borrowed.

Being borrowed only affects the ABI and runtime behavior of the function when compiled or interpreted. From the perspective of Lean's type system, this annotation has no effect. It similarly has no effect on functions not marked @[extern].

When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.

Please see https://lean-lang.org/lean4/doc/dev/ffi.html#borrowing for a complete description.

[White Chen]

@Kyle Miller
I'm currently reading the lean source code directly after git clone, and there's no such support since the Lean server hasn't even started. Previously, I was using #check foo in a lean project and then using F12 to jump to the corresponding source code section in Lean to read it, which allowed me to get docstrings through mouse hover. However, I feel this method is both stupid and cumbersome. Is there a better way?

[Kyle Miller]

The experience is nice once you've built it (be sure to set up the lean4 and lean4-dev toolchains in elan like the dev docs say to do, and to open the workspace file in VS Code)

[Kyle Miller]

There's also using the mathlib docs, which contain all the Lean docs too https://leanprover-community.github.io/mathlib4_docs/

[Kyle Miller]

I use #check too, but the mathlib docs are convenient

[White Chen]

Thank you very much, I'll try it.