feat(refactor): leanlink interface

CHANGELOG.md

@@ -1,5 +1,12 @@
 # Changelog
 
+## 0.1.1
+
+- Use LeanLink's environment evaluator and proof checks when available, while preserving compatibility with released LeanLink.
+- Prepare evaluation during module imports and share expression and proof cleanup.
+- Show expandable notebook summaries for sessions, declarations, values and expressions.
+- Read available installation output without unnecessary waits.
+
 ## 0.1.0
 
 - Add pinned mathlib installation and explicit Lean sessions.

MathlibLink/Kernel/Evaluate.wl

@@ -10,6 +10,24 @@ Options[MathlibEvaluate] = {TimeConstraint -> 120, "ReturnType" -> Automatic}
 Options[MathlibCall] = Options[MathlibEvaluate]
 Options[ProveMathlib] = {TimeConstraint -> 120}
 
+MathlibExpression /: MakeBoxes[expression : MathlibExpression[_String], form : StandardForm | TraditionalForm] := mathlibExpressionBoxes[expression, form]
+
+(* Keep the released LeanLink usable while the environment interface is developed. *)
+importSource[state_Association, source_String] := If[mathlibDirectLeanQ[],
+	mathlibInvoke["LeanImportString", state["Environment"], source],
+	mathlibInvoke["LeanImportString", mathlibSessionSource[state] <> source, "ProjectDir" -> state["Directory"]]
+]
+
+verifyTheorem[term_, time_] := If[mathlibDirectLeanQ[],
+	mathlibInvoke["LeanVerify", term, "TimeLimit" -> time],
+	With[{axioms = term["Axioms"]},
+		If[! MatchQ[axioms, {___String}] || Complement[axioms, {"propext", "Quot.sound", "Classical.choice"}] =!= {},
+			mathlibFailure["UntrustedProof", "The theorem depends on an admitted proof or an additional axiom.", <|"Axioms" -> axioms|>],
+			TimeConstrained[term["KernelCheck"], time, $TimedOut]
+		]
+	]
+]
+
 mathlibQuoteName[name_String] := If[StringContainsQ[name, "\:00ab" | "\:00bb" | "\n" | "\r"],
 	mathlibFailure["MathlibUnsupportedName", "Use MathlibExpression for this Lean identifier."],
 	StringRiffle[("\:00ab" <> # <> "\:00bb" &) /@ StringSplit[name, ".", All], "."]
@@ -39,26 +57,32 @@ mathlibEncode[MathlibSession[sessionID_String], object_MathlibObject] := With[{d
 ]
 mathlibEncode[_, _] := mathlibFailure["MathlibUnsupportedValue", "Use an exact integer, rational, boolean, string, list, MathlibObject or MathlibExpression."]
 
-retainExpression[session_MathlibSession, state_Association, expression_String, time_] := Module[{name, source, environment, result},
-	name = "mathliblink_value_" <> StringDelete[CreateUUID[], "-"];
-	source = mathlibSessionSource[state] <> "noncomputable def " <> name <> " := (" <> expression <> ")\n";
-	environment = None;
+releaseEnvironment[environment_] := If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]],
+	mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]
+]
+
+elaborateSource[session_MathlibSession, state_Association, source_String, time_, failure_Failure] := Module[{environment = None, result},
 	result = CheckAbort[
-		TimeConstrained[environment = Quiet[Check[mathlibInvoke["LeanImportString", source, "ProjectDir" -> state["Directory"]], $Failed]], time, $TimedOut],
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
+		TimeConstrained[environment = Quiet[Check[importSource[state, source], $Failed]], time, $TimedOut],
+		releaseEnvironment[environment];
 		mathlibCloseSession[session]; Abort[]
 	];
 	If[result === $TimedOut,
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
+		releaseEnvironment[environment];
 		mathlibCloseSession[session];
 		Return[mathlibFailure["MathlibTimedOut", "Lean elaboration exceeded the time limit. The session was closed."]]
 	];
-	environment = result;
-	If[! MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]],
-		Return[mathlibFailure[If[environment === $TimedOut, "MathlibTimedOut", "MathlibElaborationFailed"], "Lean could not elaborate the expression.", <|"Expression" -> expression|>]]
-	];
+	If[MatchQ[result, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], result, failure]
+]
+
+retainExpression[session_MathlibSession, state_Association, expression_String, time_] := Module[{name, source, environment, result},
+	name = "mathliblink_value_" <> StringDelete[CreateUUID[], "-"];
+	source = "noncomputable def " <> name <> " := (" <> expression <> ")\n";
+	environment = elaborateSource[session, state, source, time,
+		mathlibFailure["MathlibElaborationFailed", "Lean could not elaborate the expression.", <|"Expression" -> expression|>]];
+	If[FailureQ[environment], Return[environment]];
 	result = mathlibKeepObject[session, environment[name], expression, environment];
-	If[FailureQ[result], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
+	If[FailureQ[result], releaseEnvironment[environment]];
 	result
 ]
 
@@ -70,7 +94,10 @@ MathlibEvaluate[session_MathlibSession, expression_String, opts : OptionsPattern
 	If[FailureQ[state], Return[state]];
 	If[mode === "Object", Return[retainExpression[session, state, expression, time]]];
 	result = CheckAbort[
-		mathlibInvoke["LeanEvaluate", expression, "ProjectDir" -> state["Directory"], "Imports" -> state["Imports"], "TimeLimit" -> time],
+		If[mathlibDirectLeanQ[],
+			mathlibInvoke["LeanEvaluate", state["Environment"], expression, "TimeLimit" -> time],
+			mathlibInvoke["LeanEvaluate", expression, "ProjectDir" -> state["Directory"], "Imports" -> state["Imports"], "TimeLimit" -> time]
+		],
 		mathlibCloseSession[session]; Abort[]
 	];
 	If[MatchQ[result, Failure["TimedOut", _]], mathlibCloseSession[session]];
@@ -91,45 +118,30 @@ MathlibCall[session_MathlibSession, name_String, arguments : Longest[Except[_Rul
 	]
 
 ProveMathlib[session_MathlibSession, statement_String, proof_String, opts : OptionsPattern[]] := Module[{
-	state, time, name, source, environment, term, axioms, checked, result, retained = False, started = AbsoluteTime[]
+	state, time, name, source, environment, term, checked, result, retained = False, started = AbsoluteTime[]
 },
 	If[! mathlibOptionsQ[ProveMathlib, {opts}], Return[mathlibFailure["MathlibInvalidOption", "Unknown proof option."]]];
 	time = OptionValue[TimeConstraint];
 	If[! mathlibTimeQ[time], Return[mathlibFailure["MathlibInvalidOption", "TimeConstraint must be positive or Infinity."]]];
 	state = mathlibSessionData[session];
 	If[FailureQ[state], Return[state]];
 	name = "mathliblink_theorem_" <> StringDelete[CreateUUID[], "-"];
-	source = mathlibSessionSource[state] <> "theorem " <> name <> " : " <> statement <> " := " <> proof <> "\n";
-	environment = None;
-	result = CheckAbort[
-		TimeConstrained[environment = Quiet[Check[mathlibInvoke["LeanImportString", source, "ProjectDir" -> state["Directory"]], $Failed]], time, $TimedOut],
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
-		mathlibCloseSession[session]; Abort[]
-	];
-	If[result === $TimedOut,
-		If[MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]], mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]];
-		mathlibCloseSession[session];
-		Return[mathlibFailure["MathlibTimedOut", "Lean elaboration exceeded the time limit. The session was closed."]]
-	];
-	environment = result;
-	If[! MatchQ[environment, Symbol["Wolfram`LeanLink`LeanEnvironment"][_Association]],
-		Return[mathlibFailure[If[environment === $TimedOut, "MathlibTimedOut", "MathlibProofFailed"], "Lean did not produce the requested theorem.", <|"Statement" -> statement|>]]
-	];
+	source = "theorem " <> name <> " : " <> statement <> " := " <> proof <> "\n";
+	environment = elaborateSource[session, state, source, time,
+		mathlibFailure["MathlibProofFailed", "Lean did not produce the requested theorem.", <|"Statement" -> statement|>]];
+	If[FailureQ[environment], Return[environment]];
 	WithCleanup[
 		term = environment[name];
-		axioms = term["Axioms"];
-		If[! MatchQ[axioms, {___String}] || Complement[axioms, {"propext", "Quot.sound", "Classical.choice"}] =!= {},
-			Return[mathlibFailure["MathlibUntrustedProof", "The theorem depends on an admitted proof or an additional axiom.", <|"Axioms" -> axioms|>]]
-		];
 		checked = CheckAbort[
-			TimeConstrained[term["KernelCheck"], If[time === Infinity, Infinity, Max[0.001, time - (AbsoluteTime[] - started)]], $TimedOut],
+			verifyTheorem[term, If[time === Infinity, Infinity, Max[0.001, time - (AbsoluteTime[] - started)]]],
 			mathlibCloseSession[session]; Abort[]
 		];
-		If[checked === $TimedOut, mathlibCloseSession[session]; Return[mathlibFailure["MathlibTimedOut", "Kernel checking exceeded the time limit. The session was closed."]]];
+		If[checked === $TimedOut || MatchQ[checked, Failure["TimedOut", _]], mathlibCloseSession[session]; Return[mathlibFailure["MathlibTimedOut", "Kernel checking exceeded the time limit. The session was closed."]]];
+		If[MatchQ[checked, Failure["UntrustedProof", _]], Return[mathlibFailure["MathlibUntrustedProof", "The theorem depends on an admitted proof or an additional axiom.", <|"Axioms" -> checked["Axioms"]|>]]];
 		If[! MatchQ[checked, _Success], Return[mathlibFailure["MathlibKernelRejected", "Lean's kernel did not accept the theorem's module.", <|"Result" -> checked|>]]];
-		result = mathlibKeepObject[session, term, "((" <> proof <> ") : " <> statement <> ")", environment, True];
+		result = mathlibKeepObject[session, term, "((" <> proof <> ") : " <> statement <> ")", environment, True, statement];
 		retained = ! FailureQ[result];
 		result,
-		If[! retained, mathlibInvoke["LeanFreeEnvironment", Information[environment, "Handle"]]]
+		If[! retained, releaseEnvironment[environment]]
 	]
 ]

MathlibLink/Kernel/Formatting.wl

@@ -0,0 +1,58 @@
+PackageScoped[{mathlibSessionBoxes, mathlibObjectBoxes, mathlibExpressionBoxes}]
+
+(* Summaries use stored data only. Displaying an object must not evaluate Lean
+   code, query its native environment or repeat a proof check. *)
+
+summaryText[text_String] := Pane[Style[text, "Input", ShowStringCharacters -> False, TextAlignment -> Left],
+	ImageSize -> {{0, 480}, Automatic}, Alignment -> Left]
+
+summaryPreview[text_String] := With[{line = StringReplace[text, {"\r\n" -> " ", "\n" -> " ", "\r" -> " ", "\t" -> " "}]},
+	summaryText[If[StringLength[line] > 90, StringTake[line, 87] <> "...", line]]
+]
+
+summaryBox[head_, object_, items_List, details_List, form_] :=
+	BoxForm`ArrangeSummaryBox[head, object, None, items, details, form, "Interpretable" -> Automatic]
+
+mathlibSessionBoxes[session : MathlibSession[id_String], form_] :=
+	With[{state = Lookup[$mathlibSessions, id, <||>]},
+		summaryBox[MathlibSession, session,
+			{
+				BoxForm`SummaryItem[{"Status: ", Lookup[state, "Status", "Unavailable"]}],
+				If[KeyExistsQ[state, "DeclarationCount"], BoxForm`SummaryItem[{"Declarations: ", state["DeclarationCount"]}], Nothing]
+			},
+			{
+				If[KeyExistsQ[state, "Imports"], BoxForm`SummaryItem[{"Imports: ", Column[summaryText /@ state["Imports"]]}], Nothing],
+				If[KeyExistsQ[state, "Directory"], BoxForm`SummaryItem[{"Directory: ", summaryText[state["Directory"]]}], Nothing]
+			}, form]
+	]
+
+mathlibObjectBoxes[object : MathlibObject[id_String], form_] :=
+	Module[{data, state, term, kind, label, content},
+		data = Lookup[$mathlibObjects, id, <||>];
+		state = Lookup[$mathlibSessions, Lookup[data, "Session", ""], <||>];
+		If[Lookup[state, "Status", None] =!= "Ready",
+			Return[summaryBox[MathlibObject, object, {BoxForm`SummaryItem[{"Status: ", "Unavailable"}]}, {}, form]]
+		];
+		term = Replace[Lookup[data, "Term", None], {_[values_Association] :> values, _ -> <||>}];
+		kind = Which[
+			TrueQ[Lookup[data, "Verified", False]], "Checked theorem",
+			Lookup[data, "Environment", None] =!= None, "Typed expression",
+			True, Lookup[term, "Kind", "Declaration"]
+		];
+		{label, content} = Which[
+			StringQ[Lookup[data, "Statement", None]], {"Statement: ", data["Statement"]},
+			Lookup[data, "Environment", None] =!= None, {"Expression: ", Lookup[data, "Expression", ""]},
+			True, {"Name: ", Lookup[term, "Name", ""]}
+		];
+		summaryBox[MathlibObject, object,
+			{BoxForm`SummaryItem[{"Kind: ", kind}], BoxForm`SummaryItem[{label, summaryPreview[content]}]},
+			{
+				If[StringLength[content] > 90, BoxForm`SummaryItem[{label, summaryText[content]}], Nothing],
+				If[label =!= "Name: ", BoxForm`SummaryItem[{"Declaration: ", summaryText[Lookup[term, "Name", ""]]}], Nothing],
+				BoxForm`SummaryItem[{"Session: ", Lookup[state, "Status", "Unavailable"]}]
+			}, form]
+	]
+
+mathlibExpressionBoxes[expression : MathlibExpression[source_String], form_] :=
+	summaryBox[MathlibExpression, expression, {BoxForm`SummaryItem[{"Source: ", summaryPreview[source]}]},
+		{BoxForm`SummaryItem[{"Source: ", summaryText[source]}]}, form]

MathlibLink/Kernel/Installation.wl

@@ -29,21 +29,27 @@ mathlibInstallStage[stage_String, fraction_ : None] := (
 
 (* Drain both pipes while polling, so a long cache download remains responsive.
    WithCleanup also stops the owned process on Throw, Abort or a callback error. *)
-mathlibInstallRun[arguments_List, directory_String, extraEnvironment_Association : <||>] := Module[{process, out = "", err = "", read},
+mathlibInstallRun[arguments_List, directory_String, extraEnvironment_Association : <||>] := Module[{process, out = "", err = "", read, stdout, stderr, newOut, newErr},
 	mathlibCheckCancellation[];
 	read[stream_] := Replace[ReadString[stream, EndOfBuffer], Except[_String] -> ""];
 	process = Quiet[Check[StartProcess[arguments, ProcessDirectory -> directory,
 		ProcessEnvironment -> mathlibEnvironment[extraEnvironment]], $Failed]];
 	If[! MatchQ[process, _ProcessObject], Return[$Failed]];
+	stdout = ProcessConnection[process, "StandardOutput"];
+	stderr = ProcessConnection[process, "StandardError"];
 	WithCleanup[
-		While[ProcessStatus[process] === "Running",
+		While[True,
 			mathlibCheckCancellation[];
-			out = out <> read[ProcessConnection[process, "StandardOutput"]];
-			err = err <> read[ProcessConnection[process, "StandardError"]];
-			Pause[0.1]
+			newOut = read[stdout];
+			newErr = read[stderr];
+			out = out <> newOut;
+			err = err <> newErr;
+			If[newOut === "" && newErr === "",
+				(* Output may remain buffered after the process exits. *)
+				If[ProcessStatus[process] =!= "Running", Break[]];
+				Pause[0.1]
+			]
 		];
-		out = out <> read[ProcessConnection[process, "StandardOutput"]];
-		err = err <> read[ProcessConnection[process, "StandardError"]];
 		mathlibCheckCancellation[];
 		<|"ExitCode" -> ProcessInformation[process, "ExitCode"], "StandardOutput" -> out, "StandardError" -> err|>,
 		If[ProcessStatus[process] === "Running", KillProcess[process]]

MathlibLink/Kernel/Internal/Common.wl

@@ -1,5 +1,9 @@
 PackageScoped[{mathlibFailure, mathlibLoadLean, mathlibInvoke, mathlibOptionsQ, mathlibTimeQ, mathlibModuleQ, mathlibDirectory, mathlibRuntime, mathlibExecutable, mathlibRun, mathlibVersionQ, mathlibLeanDirectory, mathlibBridgeReadyQ, mathlibElanHome, mathlibToolsDirectory, mathlibExecutables, mathlibPathDirectories, mathlibEnvironment}]
 
+PackageScoped[mathlibDirectLeanQ]
+
+mathlibDirectLeanQ[] := Names["Wolfram`LeanLink`LeanVerify"] =!= {} && With[{verify = Symbol["Wolfram`LeanLink`LeanVerify"]}, DownValues[verify] =!= {}]
+
 mathlibFailure[tag_String, message_String, data_Association : <||>] := Failure[tag, Join[<|"MessageTemplate" -> message|>, data]]
 
 mathlibRuntime[] := mathlibRuntime[] = Import[FileNameJoin[{PacletObject["WolframInstitute/MathlibLink"]["Location"], "Resources", "Runtime.json"}], "RawJSON"]

MathlibLink/Kernel/Object.wl

@@ -6,11 +6,11 @@ MathlibDeclaration::usage = "MathlibDeclaration[session, name] gives a typed obj
 
 $mathlibObjects = <||>
 
-mathlibKeepObject[session : MathlibSession[sessionID_String], term_, expression_String, environment_ : None, verified_ : False] := Module[{id = CreateUUID[], state},
+mathlibKeepObject[session : MathlibSession[sessionID_String], term_, expression_String, environment_ : None, verified_ : False, statement_ : None] := Module[{id = CreateUUID[], state},
 	state = mathlibSessionData[session];
 	If[FailureQ[state], Return[state]];
 	AssociateTo[$mathlibObjects, id -> <|"Session" -> sessionID, "Term" -> term, "Expression" -> expression,
-		"Environment" -> environment, "Verified" -> verified|>];
+		"Environment" -> environment, "Verified" -> verified, "Statement" -> statement|>];
 	AssociateTo[$mathlibSessions, sessionID -> Append[state, "Objects" -> Append[state["Objects"], id]]];
 	MathlibObject[id]
 ]
@@ -67,13 +67,4 @@ MathlibDeclaration[session_MathlibSession, name_String] := With[{state = mathlib
 
 MathlibObject /: Normal[object_MathlibObject] := With[{data = mathlibObjectData[object]}, If[FailureQ[data], data, data["Term"]]]
 MathlibObject /: DeleteObject[MathlibObject[id_String]] := mathlibForgetObject[id]
-MathlibObject /: MakeBoxes[object : MathlibObject[id_String], form_] := With[{
-	data = Lookup[$mathlibObjects, id, None]
-}, With[{label = Which[
-	! AssociationQ[data], "Released",
-	TrueQ[data["Verified"]], "Checked theorem",
-	data["Environment"] =!= None, "Typed expression",
-	True, data["Term"]["Name"]
-]}, With[{boxes = ToBoxes[label, form]},
-	InterpretationBox[RowBox[{"MathlibObject", "[", boxes, "]"}], object]
-]]]
+MathlibObject /: MakeBoxes[object : MathlibObject[_String], form : StandardForm | TraditionalForm] := mathlibObjectBoxes[object, form]