opaque Lean.PremiseSelection.Cloud.premiseSelection.apiBaseUrl : Lean.Option String

opaque Lean.PremiseSelection.Cloud.premiseSelection.maxUnindexedPremises : Lean.Option Nat

def Lean.PremiseSelection.Cloud.getApiBaseUrl (opts : Options) : String

Equations

• Lean.PremiseSelection.Cloud.getApiBaseUrl opts = Lean.Option.get opts Lean.PremiseSelection.Cloud.premiseSelection.apiBaseUrl

def Lean.PremiseSelection.Cloud.makeRequest {α : Type} [FromJson α] (method urlPath : String) (data? : Option Json) : CoreM α

Equations

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

Retrieving indexed premises and modules stored on the server, and collecting new premises either imported or defined locally.

The reason we make the distinction between imported and local premises is only because we can cache the results (set of premises and their signatures if unindexed) for imported premises in IO.Ref, because they won't change unless imports are changed.

Indexed premises are represented by a Nat (index in getIndexedPremisesFromServer). Unindexed premises are represented as a Premise (name and signature).

def Lean.PremiseSelection.Cloud.getMaxUnindexedPremises : CoreM Nat

The maximum number of new premises to send to the server.

Equations

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

opaque Lean.PremiseSelection.Cloud.indexedPremisesFromServerRef : IO.Ref (Option (NameMap Nat))

A cache holding indexed premises by the server.

def Lean.PremiseSelection.Cloud.getIndexedPremisesFromServer : CoreM (NameMap Nat)

Unfiltered list of all premises known by the server, as a mapping from name to index. The result is cached in an IO.Ref, because (assuming the server is static) the result will not change.

Equations

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

def Lean.PremiseSelection.Cloud.getIndexedPremisesFromServer.core : CoreM (NameMap Nat)

Equations

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

def Lean.PremiseSelection.Cloud.getIndexedModules : CoreM NameSet

All modules known by the server. NOTE This is not used.

Equations

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

opaque Lean.PremiseSelection.Cloud.indexedImportedPremisesRef : IO.Ref (Option (Array Nat))

A cache holding the premises imported from other modules that are indexed by the server.

opaque Lean.PremiseSelection.Cloud.unindexedImportedPremisesRef : IO.Ref (Option (Array Premise × Nat))

A cache holding the premises imported from other modules that are not indexed by the server.

def Lean.PremiseSelection.Cloud.getImportedPremisesCore (chunkSize : Nat := 256) : CoreM (Array Nat × Array Premise × Nat)

Get imported premises, separated by whether they are indexed by the server, and a number indicating the true number of unindexed imported premises.

Equations

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

def Lean.PremiseSelection.Cloud.getIndexedImportedPremises (chunkSize : Nat := 256) : CoreM (Array Nat)

Get the imported premises that are indexed by the server. The result is cached in an IO.Ref, because (assuming the server is static) the result will not change unless the file is restarted.

Equations

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

def Lean.PremiseSelection.Cloud.getUnindexedImportedPremises (chunkSize : Nat := 256) : CoreM (Array Premise)

Get the imported premises not indexed by the server. The result is cached in an IO.Ref, because (assuming the server is static) the result will not change unless the file is restarted.

Equations

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

def Lean.PremiseSelection.Cloud.getNumUnindexedImportedPremises (chunkSize : Nat := 256) : CoreM Nat

Get the number of imported premises not indexed by the server. The result is cached in an IO.Ref, because (assuming the server is static) the result will not change unless the file is restarted. This number is used only for printing a warning message.

Equations

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

def Lean.PremiseSelection.Cloud.getIndexedLocalPremises : CoreM (Array Nat)

Get the local premises defined in the current file that are indexed by the server. Modifications to these premises will not be reflected in the retrieval results, with the assumption being even if modifications are made, they should be small enough to significantly change the semantic meaning (the name is kept after all).

Equations

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

def Lean.PremiseSelection.Cloud.getUnindexedLocalPremises (chunkSize : Nat := 256) : CoreM (Array Premise)

Returns the local premises defined in the current file that are not indexed by the server. The set of premises is not cached, to allow for adding/deleting local premises (unless indexed by the server). Currently, the printed signature itself is cached by the Premise.fromName function, meaning that it does not support modifying local premises, but (TODO) this behavior might (or should) change in the future by disabling this cache.

Equations

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

def Lean.PremiseSelection.Cloud.getUnindexedPremises (chunkSize : Nat := 256) : CoreM (Array Premise)

Returns new unindexed premises defined in the environment, from both imported and local premises, truncated to the maximum number of unindexed premises allowed by the server.

Equations

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

def Lean.PremiseSelection.Cloud.getIndexedPremises (chunkSize : Nat := 256) : CoreM (Array Nat)

Returns indexed premises defined in the environment, from both imported and local premises.

Equations

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

def Lean.PremiseSelection.Cloud.commandSet_premise_selection_cloud_cache : ParserDescr

Equations

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

def Lean.PremiseSelection.Cloud.commandClear_premise_selection_cloud_cache : ParserDescr

Equations

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

def Lean.PremiseSelection.Cloud.instFromJsonSuggestion_premiseSelection : FromJson Suggestion

Equations

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

def Lean.PremiseSelection.Cloud.instToStringSuggestion_premiseSelection : ToString Suggestion

Equations

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

def Lean.PremiseSelection.Cloud.instToMessageDataSuggestion_premiseSelection : ToMessageData Suggestion

Equations

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

def Lean.PremiseSelection.Cloud.selectPremisesCore (state : String) (indexedPremises : Array Nat) (unindexedPremises : Array Premise) (k : Nat) : CoreM (Array Suggestion)

Equations

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

def Lean.PremiseSelection.Cloud.selectPremises (goal : MVarId) (k : Nat) : MetaM (Array Suggestion)

Equations

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

def Lean.PremiseSelection.Cloud.premiseSelector : Selector

Equations

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