Here we define mechanisms that send new user-defined premises to the server.

The entire architecture is very WIP: it depends on several unreal assumptions

• If a user imports a module that is indexed by the server, the contents of the module is not changed
• After a user calculates the pretty-printed form of a premise, it will not be changed any more (because of caching)

structure Lean.PremiseSelection.Premise : Type

The data of a new premise sent to the server, including name and a signature consisting of docstring and type.

• name : Name
• decl : String

instance Lean.PremiseSelection.instInhabitedPremise : Inhabited Premise

Equations

• Lean.PremiseSelection.instInhabitedPremise = { default := { name := default, decl := default } }

instance Lean.PremiseSelection.instReprPremise : Repr Premise

Equations

• Lean.PremiseSelection.instReprPremise = { reprPrec := Lean.PremiseSelection.reprPremise✝ }

instance Lean.PremiseSelection.instToJsonPremise : ToJson Premise

Equations

• Lean.PremiseSelection.instToJsonPremise = { toJson := Lean.PremiseSelection.toJsonPremise✝ }

def Lean.PremiseSelection.Premise.getKind (cinfo : ConstantInfo) : MetaM String

Returns kind (string) given constant (from declarations.lean)

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.PremiseSelection.Premise.fromNameCacheRef : IO.Ref (NameMap Premise)

A reference holding a mapping from a user-defined premise name to Premise.fromName name (see Premise.fromName).

def Lean.PremiseSelection.Premise.fromNameCore (name : Name) : CoreM Premise

Equations

• One or more equations did not get rendered due to their size.

def Lean.PremiseSelection.Premise.fromName (name : Name) (useCache : Bool) : CoreM Premise

Serialize a declaration into a Premise by pretty-printing the declaration docstring and signature.

If useCache := true, this function is cached by fromNameCacheRef, so on the second time it is called on the same declaration, it reads the previously stored result instead of calculates the signature again. (TODO) This is just a temporary solution so that it is reasonable to call e.g. aesop (add unsafe (by hammer)) where hammer is called many times.

Equations

• One or more equations did not get rendered due to their size.

def Lean.PremiseSelection.Premise.fromNames (names : Array Name) (chunkSize : Nat) (useCache : Bool) : CoreM (Array Premise)

This is equivalent to names.mapM Premise.fromName, but it processes chunks in parallel.

Equations

• One or more equations did not get rendered due to their size.

TODO: use the implementation of deny-list in https://github.com/leanprover/lean4/tree/mepo instead (once the branch is merged)