How likely will there be numerical analysis / visualization

Stream: lean4

[Fengyang Wang]

How active, or ever interested, is the development in numerical analysis and makeing good looking plots in lean.

I googled plotting in lean and the first result was graph theory in lean. If this is the most correlated result, I don't have too much faith in plotting in lean.

[Kevin Buzzard]

You might be interested in scilean

[Alok Singh]

https://github.com/alok/limestone at least one person besides me has plotted with this (ai port of a haskell terminal plotting lib)

https://github.com/alok/leanplot has working commits but the head is broken

[Pablo Donato]

What's the latest commit which is still working @Alok Singh ? I am currently trying to run the Quickstart example, and after trying a few revisions I always get the following error when running lake build:

error: Lean exited with code 1
✖ [13/25] Building ProofWidgets.Component.Basic
trace: .> LEAN_PATH=[...]/.lake/packages/Cli/.lake/build/lib/lean:[...]/.lake/packages/Qq/.lake/build/lib/lean:[...]/.lake/packages/aesop/.lake/build/lib/lean:[...]/.lake/packages/importGraph/.lake/build/lib/lean:[...]/.lake/packages/LeanSearchClient/.lake/build/lib/lean:[...]/.lake/packages/plausible/.lake/build/lib/lean:[...]/.lake/packages/batteries/.lake/build/lib/lean:[...]/.lake/packages/subverso/.lake/build/lib/lean:[...]/.lake/packages/MD4Lean/.lake/build/lib/lean:[...]/.lake/packages/proofwidgets/.lake/build/lib/lean:[...]/.lake/packages/verso/.lake/build/lib/lean:[...]/.lake/packages/mathlib/.lake/build/lib/lean:[...]/.lake/packages/LeanPlot/.lake/build/lib/lean:[...]/.lake/build/lib/lean /Users/pablo/.elan/toolchains/leanprover--lean4---v4.26.0-rc2/bin/lean [...]/.lake/packages/proofwidgets/ProofWidgets/Component/Basic.lean -o [...]/.lake/packages/proofwidgets/.lake/build/lib/lean/ProofWidgets/Component/Basic.olean -i [...]/.lake/packages/proofwidgets/.lake/build/lib/lean/ProofWidgets/Component/Basic.ilean -c [...]/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c --setup [...]/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.setup.json --json
error: ProofWidgets/Component/Basic.lean:62:5: Invalid `⟨...⟩` notation: Constructor for `Lean.Server.WithRpcRef` is marked as private
error: Lean exited with code 1
Some required targets logged failures:
- LeanPlot.ToFloat
- ProofWidgets.Component.Basic
error: build failed

[Pablo Donato]

seems to be a problem with ProofWidgets

[Alok Singh]

try latest?