Skip to content

v0.1.1

Choose a tag to compare

View all tags
@github-actions github-actions released this 03 Nov 19:46
· 8 commits to main since this release
v0.1.1
c45a369

MathlibLink 0.1.1

  • Reuse LeanLink's imported environments for evaluation and proof checking when supported.
  • Use LeanLink's in-process evaluator by default when available. Set "Isolated" -> True in MathlibEvaluate or MathlibCall to evaluate in a separate process.
  • Prepare evaluation during imports, improve cleanup and remove unnecessary waits when reading installation output.
  • Display sessions, declarations, values and expressions as expandable notebook summaries.

Existing MathlibLink session functions remain supported with LeanLink 1.2.5 or
later. The new environment interface, evaluator preparation and in-process evaluation require
LeanLink PR #4 until those
changes are released. Loading MathlibLink does not start Lean or install software.

Requires Wolfram Language 15.0 or later, Lean 4.35.0 and mathlib v4.35.0.

Assets 6
Loading