Calling Lean Functions As Python Functions
I think Lean is neat.
Maybe especially as a programming language. Got lots of fun doodads, cool compiler to fast code, metaprogramming, and then some day maybe you can prove something if you feel like it as a treat.
I made a python library to make lean-python interop a little less painful https://github.com/philzook58/leancall . Cody has also been sniffing around this area and has been poking me to try and build something like this. https://github.com/codyroux/lean-to-python
Here’s what it looks like to use it.
import leancall as lc
mod = lc.from_string("def foo (x : Nat) (s : String) : String := s ++ toString x")
mod.foo(42, "The answer is ")
'The answer is 42'
This is done by basically 3 things:
- an extensible singledispatch
to_leanto serialize python values to lean. - a lark parser for lean output. I like lark. It also outputs reasonable defaults.
nonebecomesNone,Stringisstr,IntandNatareint, etc. - a grep for
defsin the lean file - a
LeanFunclass that uses these things to take python values to and from lean
You can see an early prototype of this way below.
Here’s some fun examples of using it with interesting libraries
Controlling a Cartpole
It is fast enough to control a gym environment https://gymnasium.farama.org/introduction/basic_usage/ (gym is a library for reinforcement learning)
Cody had a lean pendulum controller that he kept private for some reason.
%%file /tmp/cartpole.lean
def action (obs : List Float) : Nat :=
let pos := obs[0]!
let vel := obs[1]!
let ang := obs[2]!
let ang_vel := obs[3]!
-- I fiddled with this until it seems to work
if pos - 1 * vel + 2.0 * ang + 0.7 * ang_vel < 0.0 then
0
else
1
Overwriting /tmp/cartpole.lean
import leancall as lc
import leancall.numpy
mod = lc.from_file("/tmp/cartpole.lean")
import gymnasium as gym
env = gym.make("CartPole-v1", render_mode="human")
observation, info = env.reset()
episode_over = False
total_reward = 0
try:
while not episode_over:
# Choose an action: 0 = push cart left, 1 = push cart right
action = mod.action(list(observation))
observation, reward, terminated, truncated, info = env.step(action)
total_reward += reward
episode_over = terminated or truncated
finally:
env.close()
print(f"Episode finished! Total reward: {total_reward}")
It balances! Wowee zowee!
Ray Tracing
My friends were also just sort of winging a bad ray tracer. Using python is nice because you already have image showing libraries, which avoids the need to make some new custom Lean vs code thing or serialize to PPM.
Here was a python thing we whipped out to draw a circle. I do not claim it as a paragon of code excellence.
import numpy as np
img = np.zeros((800,800,3))
for i in range(800):
for j in range(800):
if (i-200)**2 + (j-200)**2 < 100**2:
img[i,j] = [0,255,0]
import matplotlib.pyplot as plt
plt.imshow(img)
%%file /tmp/circle.lean
abbrev Image := Array (Array (Array UInt8))
partial def doit (N : Nat) := Id.run do
let mut img : Image := Array.replicate N (Array.replicate N #[0, 0, 0])
for i in [0:N] do
for j in [0:N] do
if ((i : Int)- N/2)^2 + ((j : Int) - N/2)^2 < (N/4)^2 -- This Int conversion sucks. But I'd have a similar problem in many other languages
then
img := img.modify i fun row => row.set! j #[0, 0, 255]
return img
Writing /tmp/circle.lean
import leancall as lc
mod = lc.from_file("/tmp/ray.lean")
plt.imshow(mod.doit(300))
I found the lark parsing to be a bit slow (printing a giant array out is a somewhat ludicrous thing to be doing). Using numpy.loadtxt is quite a bit faster. I wrapped it in leancall.numpy.parse
import leancall.numpy as lcnp
N = 600
plt.imshow(lcnp.parse(mod.doit(N, parse=None)).reshape((N,N,3)).astype(np.uint8))
This is a larger ray tracer. Again, not a paragon of anything. AI produced this largely from our python version. You may also want to check out https://github.com/kmill/lean4-raytracer and https://raytracing.github.io/books/RayTracingInOneWeekend.html
%%file /tmp/ray.lean
abbrev Pixel := UInt8 × UInt8 × UInt8
abbrev Image : Type := Array (Array Pixel)
structure Vec3 where
x : Float
y : Float
z : Float
deriving Repr, Inhabited, BEq
instance : Add Vec3 where
add a b := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
instance : Sub Vec3 where
sub a b := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩
instance : HMul Float Vec3 Vec3 where
hMul s v := ⟨s * v.x, s * v.y, s * v.z⟩
instance : HDiv Vec3 Float Vec3 where
hDiv v s := ⟨v.x / s, v.y / s, v.z / s⟩
def dot (a b : Vec3) : Float :=
a.x * b.x + a.y * b.y + a.z * b.z
def norm (v : Vec3) : Float :=
Float.sqrt (dot v v)
def normalize (v : Vec3) : Vec3 :=
let n := norm v
if n == 0 then v else v / n
def clamp01 (x : Float) : Float :=
if x < 0 then 0 else if x > 1 then 1 else x
def hadamard (a b : Vec3) : Vec3 :=
⟨a.x * b.x, a.y * b.y, a.z * b.z⟩
def floatToByte (x : Float) : UInt8 :=
let y := clamp01 x
UInt8.ofNat (UInt64.toNat (Float.toUInt64 (y * 255.0)))
def colorToPixel (c : Vec3) : Pixel :=
(floatToByte c.x, floatToByte c.y, floatToByte c.z)
structure Sphere where
center : Vec3
radius : Float
color : Vec3
deriving Repr, Inhabited, BEq
structure Ray where
origin : Vec3
direction : Vec3
deriving Repr, Inhabited, BEq
structure Light where
position : Vec3
color : Vec3
deriving Repr, Inhabited, BEq
def Sphere.intersect (s : Sphere) (r : Ray) : Option (Float × Vec3) :=
let oc := r.origin - s.center
let a := dot r.direction r.direction
let b := 2.0 * dot oc r.direction
let c := dot oc oc - s.radius * s.radius
let discriminant := b * b - 4 * a * c
if discriminant < 0 then
none
else
let t1 := (-b - Float.sqrt discriminant) / (2.0 * a)
let t2 := (-b + Float.sqrt discriminant) / (2.0 * a)
if t1 > 0 then
let pos := r.origin + t1 * r.direction
let norm := (pos - s.center) / s.radius
some (t1, norm)
else if t2 > 0 then
let pos := r.origin + t2 * r.direction
let norm := (pos - s.center) / s.radius
some (t2, norm)
else
none
def lights : List Light :=
[ { position := ⟨50, 50, 0⟩, color := ⟨1, 0.1, 0.4⟩ } ]
def objects : List Sphere :=
[ { center := ⟨0, 10, 50⟩, radius := 10, color := ⟨1, 0.1, 0.1⟩ }
, { center := ⟨0, 0, 100⟩, radius := 10, color := ⟨0.1, 1, 0.1⟩ }
, { center := ⟨-20, 0, 100⟩, radius := 10, color := ⟨0.1, 0.1, 1⟩ } ]
def render (N : Nat) : Image := Id.run do
let mut img : Image := Array.replicate N (Array.replicate N (0, 0, 0))
let half := Float.ofNat (N / 2)
let nFloat := Float.ofNat N
for i in [0:N] do
for j in [0:N] do
let dir := ⟨(Float.ofNat i - half) / nFloat, (Float.ofNat j - half) / nFloat, 1⟩
let ray := Ray.mk ⟨0, 0, 0⟩ dir
let mut closestT : Float := 1.0e30
let mut pixelColor : Pixel := (135, 206, 235) -- sky color
for obj in objects do
match obj.intersect ray with
| some (t, norm) =>
if t < closestT then
closestT := t
let mut col : Vec3 := ⟨0, 0, 0⟩
let hitPos := ray.origin + t * ray.direction
for light in lights do
let lightDir := normalize (light.position - hitPos)
let diff := dot norm lightDir
if diff > 0 then
col := col + diff * (hadamard obj.color light.color)
pixelColor := colorToPixel col
| none => ()
img := img.modify i fun row => row.set! j pixelColor
img
Overwriting /tmp/ray.lean
mod = lc.from_file("/tmp/ray.lean")
plt.imshow(mod.render(400))
Bits and Bobbles
https://www.youtube.com/watch?v=c5LOYzZx-0c The Best New Programming Language is a Proof Assistant by Harry Goldstein
https://www.philipzucker.com/dirty_lean/ Doing Lean Dirty: Lean as a Jupyter Notebook Replacement
https://www.philipzucker.com/lean_smt/ Using Lean like an External SMT Solver from Python
Feel no guilt putting unsafe and partial everywhere imo. It’s the analog of just getting clone happy in Rust. Just do it at the first sight of trouble. I absolve you.
You pay quite an overhead to serialize and deserialize. I also added an experimental direct FFI thing. It was pretty vibe coded so I dunno.
Another thing that could actually be useful is to use Lean with cocotb, which is a python verilog test driver thing
Maybe leancall should just be a module in leaninteract.
Also, I like using python. I defend it to my PL nerd friends and shit on it to my python friends. It has a vast number of useful libraries. It’s nice for ripping ideas out.
Once you get past the standard library and mathlib, Lean’s library ecosystem is not great yet. Using python as a shim to get pictures and file formats and stuff is not that crazy. Using Lean as a backend to python libraries is also not that crazy of an idea also I think. It is faster (almost everything is), it exposes a C ABI. Some projects already do it (https://github.com/leanprover/KLR https://github.com/alerad/leancert )
https://github.com/augustepoiroux/LeanInteract Lean interact is a project that gives you a lean repl as a python library. It’s main intent is probably for machine learning proof stuff. This library really supplies the heaviest lifting and what I added was some ergonomics shellac.
I thought it would be fun to use it to build a python lean bridge where you can use lean functions fairly painlessly as python functions.
Because people are interested in
One thing that isn’t great about lean is it’s library ecosystem. It’s a young language still. Mathlib is remarkable, the standard library has made great strides, but there isn’t much else.
I am a dirty dog. I do not like lifting little ideas out into projects of their own. I have a giant folder of files that I tinker on. I want to install garbage willy nilly and puke all over my computer. This is against best software engineering practice.
The one way I have to make this work is to just have my garvage folder have a lakefile at the top level specifying a version of lean and mathlib. I keep it updating to the latest versio nevery couple of months. Libraries get left behind.
Actually Lean stresses me out. Too many smart people working hard. What’s left for little ole me?
import leancall as lc
import leancall.numpy
mod = lc.from_string("def foo x := x + 1")
type(mod.foo(3))
Does leancall change how I would go about pcode?
%%file /tmp/app.lean
import Lean.Data.Json
structure App where
f : String
args : List App
deriving Repr, Inhabited, BEq, Lean.ToJson, Lean.FromJson
def idapp (a : App) : Lean.Json := Lean.toJson a
partial def is_subterm (a b : App) : Bool :=
if a == b then
true
else
match a with
| App.mk _ args => args.any (fun arg => is_subterm arg b)
Writing /tmp/app.lean
import leancall as lc
import leancall.numpy
from dataclasses import dataclass
@dataclass(frozen=True)
class App:
f: str
args: tuple["App", ...] = ()
def of_dict(d):
return App(d['f'], [App.of_dict(a) for a in d['args']])
@lc.register_from_lean("App")
def _(x) -> App:
return x
mod = lc.from_file("/tmp/app.lean")
App.of_dict(mod.idapp(App("foo", [])))
x = App("x")
y = App("y")
f = lambda x: App("f", (x,))
#mod.is_subterm(f(x), x) # true
calllean look at other similar solutions? prologs? ocaml? clr https://pythonnet.github.io/pythonnet/python.html
https://github.com/codyroux/simple-prolog/blob/master/SimpleProlog/Basic.lean
Overwriting /tmp/cartpole.lean
import numpy as np
mod = lc.from_file("/tmp/cartpole.lean")
mod.action([0.01234567, -0.00987654, 0.02345678, 0.01456789])
1
import gymnasium as gym
env = gym.make("CartPole-v1", render_mode="human")
observation, info = env.reset()
print(f"Starting observation: {observation}")
# Example output: [ 0.01234567 -0.00987654 0.02345678 0.01456789]
# [cart_position, cart_velocity, pole_angle, pole_angular_velocity]
print(type(observation))
episode_over = False
total_reward = 0
try:
while not episode_over:
# Choose an action: 0 = push cart left, 1 = push cart right
action = mod.action(list(observation))
observation, reward, terminated, truncated, info = env.step(action)
# reward: +1 for each step the pole stays upright
# terminated: True if pole falls too far (agent failed)
# truncated: True if we hit the time limit (500 steps)
total_reward += reward
episode_over = terminated or truncated
finally:
env.close()
print(f"Episode finished! Total reward: {total_reward}")
Starting observation: [-0.04921084 -0.01602873 0.02273309 -0.01083545]
<class 'numpy.ndarray'>
Episode finished! Total reward: 500.0
Lean interact
def foo1(i):
s = 0
for _ in range(i):
s += i
return s
%%timeit
foo1(100000)
2.18 ms ± 5.57 μs per loop (mean ± std. dev. of 7 runs, 100 loops each)
%%file /tmp/foo.lean
def foo (i : Nat) : Nat := Id.run do
let mut s := 0
for _ in [0:i] do
s := s + i
return s
Overwriting /tmp/foo.lean
mod = cl.from_file("/tmp/foo.lean")
Yea, it’s constant time
mod.foo(100000000)
10000000000000000
%%timeit
mod.foo(100000000)
191 μs ± 65.4 μs per loop (mean ± std. dev. of 7 runs, 1 loop each)
from lean_interact import LeanREPLConfig, LeanServer, Command
config = LeanREPLConfig(verbose=True) # download and build Lean REPL
server = LeanServer(config) # start Lean REPL
server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := id"))
server.run(Command(cmd="def mysucc x := x + 1", env=0))
CommandResponse(env=1)
server.run(Command(cmd="#eval mysucc 41", env=1))
CommandResponse(env=2, messages=[Message(start_pos=Pos(line=1, column=0), severity='info', data='42', end_pos=Pos(line=1, column=5))])
"""
def to_lean(x : object) -> str:
if isinstance(x, int):
return str(x)
elif isinstance(x, bool):
return "true" if x else "false"
elif isinstance(x, str):
return f'"{x}"'
elif isinstance(x, list):
return "[" + ", ".join(map(to_lean, x)) + "]"
elif isinstance(x, tuple):
return "(" + ", ".join(map(to_lean, x)) + ")"
elif isinstance(x, float):
return str(x)
# dict -> json or hashmap?
else:
raise Exception(f"Cannot convert {x} to Lean")
"""
Could have lean reach into python process and directly access memory for numpy / buffers That’d be nasssssty.
from lean_interact import LeanREPLConfig, LeanServer, Command
from functools import singledispatch
config = LeanREPLConfig(verbose=True) # download and build Lean REPL
server = LeanServer(config) # start Lean REPL
@singledispatch
def to_lean(x : object) -> str:
raise Exception(f"Cannot convert {x} to Lean")
@to_lean.register
def _(x : int) -> str:
return str(x)
@to_lean.register
def _(x : bool) -> str:
return "true" if x else "false"
@to_lean.register
def _(x : str) -> str:
return f'"{x}"'
@to_lean.register
def _(x : float) -> str:
return str(x)
@to_lean.register(list)
def _(x : list) -> str:
return "[" + ", ".join(map(to_lean, x)) + "]"
@to_lean.register(tuple)
def _(x : tuple) -> str:
return "(" + ", ".join(map(to_lean, x)) + ")"
def from_lean(x : str, typ : str) -> object:
if typ == "Nat" or typ == "Int":
return int(x)
elif typ == "Bool":
assert x in ["true", "false"]
return x == "true"
elif typ == "String":
return x.strip('"')
elif typ == "Float":
return float(x)
elif typ == "Unit":
assert x == "()"
return ()
elif typ.startswith('Option '):
if x == "none":
return None
elif x.startswith("some "):
inner_typ = typ[len('Option '):]
return from_lean(x[len("some "):], inner_typ)
else:
# hail mary
# may work for lists and tuples of simple elements
return eval(x)
class LeanFun():
def __init__(self, code, env=None):
codesplit = code.split()
assert codesplit[0] == "def"
self.name = codesplit[1]
self.code = code
res = server.run(Command(cmd=code, env=env))
if hasattr(res, "messages") and len(res.messages) > 0:
for message in res.messages:
if message.severity == "error":
raise Exception(message.data)
self.env = res.env
# get return type for deserialization
res = server.run(Command(cmd=f"#check {self.name}", env=self.env))
self.res_type = res.messages[0].data.split(":")[-1].strip()
@classmethod
def from_string(cls, code : str, env=None):
...
def from_file(cls, filename : str, names : list[str], env=None):
# load from file
# return list of LeanFun objects
...
def __call__(self, *args, **kwargs):
res = server.run(Command(cmd=f"#eval {self.name} " + " ".join(map(to_lean, args)), env=self.env))
assert len(res.messages) == 1
message = res.messages[0]
if message.severity == "info":
return from_lean(message.data, self.res_type)
else:
raise Exception(message.data)
f = LeanFun("def mysucc (x y : Int) (s : String) (p : Nat × Nat) (r : List Int) (f : Float) := (f + 1.3, x + y + s.length + p.fst + r[0]!) |> some")
print(f.res_type)
f(1,2, "foo", (4,5), [1,2,3], 7.4)
Lake version 5.0.0-src+d8204c9 (Lean version 4.26.0)
Build completed successfully (26 jobs).
Option (Float × Int)
(8.7, 11)
%%prun -s cumulative
for i in range(1000):
f(1,2, "foo", (4,5))
216676 function calls (202767 primitive calls) in 0.260 seconds
Ordered by: cumulative time
ncalls tottime percall cumtime percall filename:lineno(function)
1000 0.004 0.000 0.263 0.000 2346713141.py:90(__call__)
1 0.001 0.001 0.259 0.259 <string>:1(<module>)
1000 0.004 0.000 0.247 0.000 server.py:327(run)
1000 0.003 0.000 0.211 0.000 server.py:242(run_dict)
1000 0.003 0.000 0.189 0.000 server.py:173(_execute_cmd_in_repl)
1000 0.002 0.000 0.173 0.000 threading.py:1115(join)
1000 0.002 0.000 0.150 0.000 threading.py:1153(_wait_for_tstate_lock)
1000 0.012 0.000 0.129 0.000 threading.py:1016(_bootstrap)
1000 0.001 0.000 0.117 0.000 threading.py:1056(_bootstrap_inner)
1000 0.003 0.000 0.114 0.000 ipkernel.py:744(run_closure)
1000 0.001 0.000 0.086 0.000 threading.py:999(run)
1000 0.003 0.000 0.084 0.000 server.py:198(reader)
7000 0.078 0.000 0.079 0.000 {method 'readline' of '_io.TextIOWrapper' objects}
1000 0.021 0.000 0.021 0.000 {built-in method _thread.start_new_thread}
1000 0.002 0.000 0.014 0.000 server.py:298(_augment_request)
1000 0.002 0.000 0.012 0.000 threading.py:973(start)
2000 0.003 0.000 0.012 0.000 main.py:384(model_copy)
3000/2000 0.010 0.000 0.011 0.000 {method 'validate_python' of 'pydantic_core._pydantic_core.SchemaValidator' objects}
1000 0.001 0.000 0.010 0.000 main.py:677(model_validate)
3000/2000 0.002 0.000 0.009 0.000 {method 'join' of 'str' objects}
2000 0.001 0.000 0.009 0.000 main.py:240(__init__)
2000 0.004 0.000 0.008 0.000 main.py:955(__copy__)
1000 0.001 0.000 0.008 0.000 ipkernel.py:768(init_closure)
1000 0.001 0.000 0.008 0.000 server.py:220(_parse_repl_output)
1000 0.001 0.000 0.008 0.000 interface.py:564(__init__)
6000/4000 0.003 0.000 0.008 0.000 functools.py:904(wrapper)
1000 0.001 0.000 0.007 0.000 __init__.py:299(loads)
1000 0.001 0.000 0.007 0.000 __init__.py:183(dumps)
1000 0.002 0.000 0.007 0.000 threading.py:882(__init__)
1000 0.001 0.000 0.006 0.000 threading.py:616(set)
1000 0.001 0.000 0.006 0.000 decoder.py:332(decode)
1000 0.001 0.000 0.005 0.000 encoder.py:183(encode)
1000 0.002 0.000 0.005 0.000 threading.py:1043(_set_tstate_lock)
1001 0.001 0.000 0.004 0.000 threading.py:424(notify_all)
1000 0.000 0.000 0.004 0.000 main.py:418(model_dump)
6000 0.002 0.000 0.004 0.000 copy.py:61(copy)
1000 0.004 0.000 0.004 0.000 encoder.py:205(iterencode)
1000 0.001 0.000 0.004 0.000 threading.py:1079(_stop)
1000 0.003 0.000 0.003 0.000 {method 'to_python' of 'pydantic_core._pydantic_core.SchemaSerializer' objects}
1000 0.000 0.000 0.003 0.000 server.py:111(is_alive)
1001 0.001 0.000 0.003 0.000 threading.py:394(notify)
2000 0.002 0.000 0.003 0.000 threading.py:855(_maintain_shutdown_locks)
1000 0.001 0.000 0.003 0.000 2346713141.py:22(_)
1000 0.003 0.000 0.003 0.000 {method 'write' of '_io.TextIOWrapper' objects}
1000 0.000 0.000 0.003 0.000 subprocess.py:1233(poll)
1000 0.003 0.000 0.003 0.000 decoder.py:343(raw_decode)
1000 0.001 0.000 0.003 0.000 subprocess.py:1973(_internal_poll)
6000 0.001 0.000 0.002 0.000 functools.py:818(dispatch)
1000 0.001 0.000 0.002 0.000 threading.py:588(__init__)
4001 0.002 0.000 0.002 0.000 {method 'release' of '_thread.lock' objects}
1000 0.001 0.000 0.002 0.000 <frozen codecs>:319(decode)
1 0.000 0.000 0.001 0.001 {method 'execute' of 'sqlite3.Connection' objects}
8003/78 0.022 0.000 0.001 0.000 {method 'acquire' of '_thread.lock' objects}
6000 0.001 0.000 0.001 0.000 weakref.py:414(__getitem__)
1000 0.001 0.000 0.001 0.000 {built-in method posix.waitpid}
2000 0.001 0.000 0.001 0.000 {method 'match' of 're.Pattern' objects}
2001 0.001 0.000 0.001 0.000 threading.py:314(_is_owned)
7000 0.001 0.000 0.001 0.000 {method 'endswith' of 'str' objects}
1000 0.001 0.000 0.001 0.000 threading.py:1106(_delete)
1000 0.001 0.000 0.001 0.000 threading.py:277(__init__)
2003 0.001 0.000 0.001 0.000 threading.py:299(__enter__)
2003 0.001 0.000 0.001 0.000 threading.py:302(__exit__)
7143/7139 0.001 0.000 0.001 0.000 {built-in method builtins.isinstance}
8004 0.001 0.000 0.001 0.000 {method 'get' of 'dict' objects}
3 0.000 0.000 0.001 0.000 base_events.py:1910(_run_once)
4000 0.001 0.000 0.001 0.000 2346713141.py:10(_)
2000 0.001 0.000 0.001 0.000 {method 'difference_update' of 'set' objects}
2000 0.001 0.000 0.001 0.000 threading.py:1483(current_thread)
5007 0.001 0.000 0.001 0.000 {method '__exit__' of '_thread.lock' objects}
1000 0.001 0.000 0.001 0.000 _weakrefset.py:85(add)
1000 0.001 0.000 0.001 0.000 threading.py:837(_newname)
1000 0.000 0.000 0.001 0.000 _weakrefset.py:39(_remove)
3000 0.001 0.000 0.001 0.000 threading.py:1234(daemon)
1000 0.000 0.000 0.001 0.000 threading.py:1036(_set_ident)
5000 0.001 0.000 0.001 0.000 {built-in method _thread.get_ident}
1000 0.000 0.000 0.001 0.000 threading.py:1040(_set_native_id)
5/3 0.000 0.000 0.001 0.000 events.py:86(_run)
5010 0.001 0.000 0.001 0.000 {built-in method builtins.hasattr}
4000 0.001 0.000 0.001 0.000 {method 'copy' of 'dict' objects}
1000 0.001 0.000 0.001 0.000 {built-in method _codecs.utf_8_decode}
1000 0.001 0.000 0.001 0.000 2346713141.py:45(from_lean)
3001 0.000 0.000 0.000 0.000 {method '__exit__' of '_thread.RLock' objects}
2000 0.000 0.000 0.000 0.000 {method 'update' of 'set' objects}
1000 0.000 0.000 0.000 0.000 {built-in method _thread._set_sentinel}
1001 0.000 0.000 0.000 0.000 threading.py:311(_acquire_restore)
4000 0.000 0.000 0.000 0.000 {method 'locked' of '_thread.lock' objects}
2002 0.000 0.000 0.000 0.000 {method '__enter__' of '_thread.lock' objects}
4/2 0.000 0.000 0.000 0.000 {method 'run' of '_contextvars.Context' objects}
1000 0.000 0.000 0.000 0.000 {built-in method _thread.get_native_id}
3020 0.000 0.000 0.000 0.000 {built-in method builtins.len}
2000 0.000 0.000 0.000 0.000 {method 'add' of 'set' objects}
3000 0.000 0.000 0.000 0.000 {method 'keys' of 'dict' objects}
2 0.000 0.000 0.000 0.000 zmqstream.py:573(_handle_events)
2001 0.000 0.000 0.000 0.000 {built-in method _thread.allocate_lock}
1001 0.000 0.000 0.000 0.000 threading.py:308(_release_save)
2000 0.000 0.000 0.000 0.000 {built-in method __new__ of type object at 0xa43b40}
2000 0.000 0.000 0.000 0.000 {method 'copy' of 'set' objects}
1 0.000 0.000 0.000 0.000 asyncio.py:200(_handle_events)
1 0.000 0.000 0.000 0.000 kernelbase.py:302(poll_control_queue)
1 0.000 0.000 0.000 0.000 _base.py:537(set_result)
1 0.000 0.000 0.000 0.000 _base.py:337(_invoke_callbacks)
1000 0.000 0.000 0.000 0.000 threading.py:1354(_make_invoke_excepthook)
1000/13 0.001 0.000 0.000 0.000 threading.py:637(wait)
1000 0.000 0.000 0.000 0.000 {method 'startswith' of 'str' objects}
2 0.000 0.000 0.000 0.000 zmqstream.py:614(_handle_recv)
1000 0.000 0.000 0.000 0.000 {method 'strip' of 'str' objects}
1000/13 0.001 0.000 0.000 0.000 threading.py:323(wait)
2000 0.000 0.000 0.000 0.000 {method 'end' of 're.Match' objects}
2000 0.000 0.000 0.000 0.000 threading.py:1196(ident)
2 0.000 0.000 0.000 0.000 zmqstream.py:546(_run_callback)
2000 0.000 0.000 0.000 0.000 {method 'items' of 'dict' objects}
1000 0.000 0.000 0.000 0.000 {method 'flush' of '_io.TextIOWrapper' objects}
1 0.000 0.000 0.000 0.000 futures.py:394(_call_set_state)
1000 0.000 0.000 0.000 0.000 {method 'remove' of 'collections.deque' objects}
2000 0.000 0.000 0.000 0.000 threading.py:601(is_set)
2 0.000 0.000 0.000 0.000 iostream.py:157(_handle_event)
2 0.000 0.000 0.000 0.000 iostream.py:276(<lambda>)
1000 0.000 0.000 0.000 0.000 {method 'discard' of 'set' objects}
1000 0.000 0.000 0.000 0.000 encoder.py:105(__init__)
1000 0.000 0.000 0.000 0.000 2346713141.py:16(_)
1 0.000 0.000 0.000 0.000 decorator.py:232(fun)
1 0.000 0.000 0.000 0.000 base_events.py:838(call_soon_threadsafe)
1 0.000 0.000 0.000 0.000 history.py:93(only_when_enabled)
1 0.000 0.000 0.000 0.000 selector_events.py:141(_write_to_self)
1 0.000 0.000 0.000 0.000 {method 'send' of '_socket.socket' objects}
1007 0.000 0.000 0.000 0.000 {method 'append' of 'collections.deque' objects}
1005 0.000 0.000 0.000 0.000 {method 'append' of 'list' objects}
1000 0.000 0.000 0.000 0.000 threading.py:1220(is_alive)
1 0.000 0.000 0.000 0.000 history.py:1025(writeout_cache)
3 0.000 0.000 0.000 0.000 zmqstream.py:653(_rebuild_io_state)
2 0.000 0.000 0.000 0.000 iostream.py:278(_really_send)
2 0.000 0.000 0.000 0.000 socket.py:700(send_multipart)
14 0.000 0.000 0.000 0.000 socket.py:623(send)
3 0.000 0.000 0.000 0.000 zmqstream.py:676(_update_handler)
2 0.000 0.000 0.000 0.000 traitlets.py:708(__set__)
1 0.000 0.000 0.000 0.000 {method 'disable' of '_lsprof.Profiler' objects}
2 0.000 0.000 0.000 0.000 traitlets.py:3631(set)
5 0.000 0.000 0.000 0.000 attrsettr.py:43(__getattr__)
1 0.000 0.000 0.000 0.000 ioloop.py:742(_run_callback)
15 0.000 0.000 0.000 0.000 enum.py:1551(__or__)
1 0.000 0.000 0.000 0.000 zmqstream.py:684(<lambda>)
2 0.000 0.000 0.000 0.000 traitlets.py:689(set)
66 0.000 0.000 0.000 0.000 enum.py:1544(_get_value)
1 0.000 0.000 0.000 0.000 decorator.py:200(fix)
7 0.000 0.000 0.000 0.000 enum.py:1562(__and__)
5 0.000 0.000 0.000 0.000 attrsettr.py:66(_get_attr_opt)
2 0.000 0.000 0.000 0.000 traitlets.py:718(_validate)
1 0.000 0.000 0.000 0.000 queues.py:186(put)
2 0.000 0.000 0.000 0.000 socket.py:771(recv_multipart)
1 0.000 0.000 0.000 0.000 queues.py:209(put_nowait)
1 0.000 0.000 0.000 0.000 history.py:1009(_writeout_input_cache)
29 0.000 0.000 0.000 0.000 enum.py:726(__call__)
2 0.000 0.000 0.000 0.000 {method '__exit__' of 'sqlite3.Connection' objects}
1 0.000 0.000 0.000 0.000 inspect.py:3237(bind)
1 0.000 0.000 0.000 0.000 selector_events.py:129(_read_from_self)
2 0.000 0.000 0.000 0.000 typing.py:1194(__instancecheck__)
2 0.000 0.000 0.000 0.000 base_events.py:785(call_soon)
1 0.000 0.000 0.000 0.000 inspect.py:3102(_bind)
3 0.000 0.000 0.000 0.000 base_events.py:814(_call_soon)
1 0.000 0.000 0.000 0.000 asyncio.py:225(add_callback)
2 0.000 0.000 0.000 0.000 {method 'recv' of '_socket.socket' objects}
1 0.000 0.000 0.000 0.000 traitlets.py:1512(_notify_trait)
2 0.000 0.000 0.000 0.000 typing.py:1465(__subclasscheck__)
2 0.000 0.000 0.000 0.000 traitlets.py:3474(validate)
1 0.000 0.000 0.000 0.000 concurrent.py:182(future_set_result_unless_cancelled)
1 0.000 0.000 0.000 0.000 traitlets.py:1523(notify_change)
6 0.000 0.000 0.000 0.000 typing.py:392(inner)
3 0.000 0.000 0.000 0.000 zmqstream.py:532(sending)
3 0.000 0.000 0.000 0.000 events.py:36(__init__)
2 0.000 0.000 0.000 0.000 traitlets.py:727(_cross_validate)
1 0.000 0.000 0.000 0.000 queues.py:225(get)
2 0.000 0.000 0.000 0.000 {built-in method builtins.issubclass}
29 0.000 0.000 0.000 0.000 enum.py:1129(__new__)
3 0.000 0.000 0.000 0.000 selector_events.py:750(_process_events)
3 0.000 0.000 0.000 0.000 queue.py:97(empty)
1 0.000 0.000 0.000 0.000 traitlets.py:1527(_notify_observers)
4 0.000 0.000 0.000 0.000 traitlets.py:676(__get__)
2 0.000 0.000 0.000 0.000 {method 'set_result' of '_asyncio.Future' objects}
2/1 0.000 0.000 0.000 0.000 selectors.py:451(select)
5 0.000 0.000 0.000 0.000 <frozen importlib._bootstrap>:1390(_handle_fromlist)
1 0.000 0.000 0.000 0.000 base_events.py:1895(_add_callback)
1 0.000 0.000 0.000 0.000 contextlib.py:299(helper)
8 0.000 0.000 0.000 0.000 {built-in method builtins.next}
4 0.000 0.000 0.000 0.000 base_events.py:734(time)
1 0.000 0.000 0.000 0.000 history.py:1017(_writeout_output_cache)
2 0.000 0.000 0.000 0.000 <frozen abc>:121(__subclasscheck__)
2 0.000 0.000 0.000 0.000 traitlets.py:3624(validate_elements)
4 0.000 0.000 0.000 0.000 typing.py:1258(__hash__)
1 0.000 0.000 0.000 0.000 inspect.py:2918(apply_defaults)
2 0.000 0.000 0.000 0.000 iostream.py:216(_check_mp_mode)
1 0.000 0.000 0.000 0.000 queues.py:317(__put_internal)
1 0.000 0.000 0.000 0.000 inspect.py:2865(args)
1 0.000 0.000 0.000 0.000 contextlib.py:141(__exit__)
4 0.000 0.000 0.000 0.000 traitlets.py:629(get)
1 0.000 0.000 0.000 0.000 threading.py:627(clear)
1 0.000 0.000 0.000 0.000 contextlib.py:132(__enter__)
1 0.000 0.000 0.000 0.000 contextlib.py:104(__init__)
1 0.000 0.000 0.000 0.000 queues.py:256(get_nowait)
2 0.000 0.000 0.000 0.000 queues.py:322(_consume_expired)
6 0.000 0.000 0.000 0.000 {built-in method builtins.getattr}
2/1 0.000 0.000 0.000 0.000 {method 'poll' of 'select.epoll' objects}
5 0.000 0.000 0.000 0.000 {built-in method builtins.max}
2 0.000 0.000 0.000 0.000 iostream.py:213(_is_master_process)
2 0.000 0.000 0.000 0.000 {built-in method _abc._abc_subclasscheck}
2 0.000 0.000 0.000 0.000 traitlets.py:2304(validate)
1 0.000 0.000 0.000 0.000 inspect.py:2888(kwargs)
1 0.000 0.000 0.000 0.000 queues.py:312(_put)
3 0.000 0.000 0.000 0.000 queue.py:209(_qsize)
8 0.000 0.000 0.000 0.000 {method 'popleft' of 'collections.deque' objects}
5 0.000 0.000 0.000 0.000 {method 'upper' of 'str' objects}
2 0.000 0.000 0.000 0.000 {built-in method posix.getpid}
20 0.000 0.000 0.000 0.000 typing.py:2154(cast)
10 0.000 0.000 0.000 0.000 inspect.py:2777(kind)
1 0.000 0.000 0.000 0.000 queues.py:173(qsize)
2 0.000 0.000 0.000 0.000 {built-in method _contextvars.copy_context}
4 0.000 0.000 0.000 0.000 {built-in method time.monotonic}
3 0.000 0.000 0.000 0.000 {method 'items' of 'mappingproxy' objects}
1 0.000 0.000 0.000 0.000 {built-in method _asyncio.get_running_loop}
2 0.000 0.000 0.000 0.000 history.py:1066(hold)
2 0.000 0.000 0.000 0.000 traitlets.py:3486(validate_elements)
1 0.000 0.000 0.000 0.000 {built-in method math.ceil}
5 0.000 0.000 0.000 0.000 zmqstream.py:528(receiving)
4 0.000 0.000 0.000 0.000 {built-in method builtins.hash}
2 0.000 0.000 0.000 0.000 {built-in method builtins.iter}
1 0.000 0.000 0.000 0.000 {method 'values' of 'mappingproxy' objects}
5 0.000 0.000 0.000 0.000 base_events.py:2005(get_debug)
1 0.000 0.000 0.000 0.000 {method '__enter__' of '_thread.RLock' objects}
1 0.000 0.000 0.000 0.000 selectors.py:275(_key_from_fd)
3 0.000 0.000 0.000 0.000 base_events.py:539(_check_closed)
1 0.000 0.000 0.000 0.000 queues.py:309(_get)
1 0.000 0.000 0.000 0.000 {built-in method builtins.min}
1 0.000 0.000 0.000 0.000 unix_events.py:81(_process_self_data)
1 0.000 0.000 0.000 0.000 queues.py:177(empty)
2 0.000 0.000 0.000 0.000 iostream.py:255(closed)
4 0.000 0.000 0.000 0.000 inspect.py:2765(name)
4 0.000 0.000 0.000 0.000 inspect.py:3058(parameters)
1 0.000 0.000 0.000 0.000 locks.py:224(clear)
2 0.000 0.000 0.000 0.000 {method 'cancelled' of '_asyncio.Future' objects}
1 0.000 0.000 0.000 0.000 {method 'done' of '_asyncio.Future' objects}
1 0.000 0.000 0.000 0.000 base_events.py:720(is_closed)
1 0.000 0.000 0.000 0.000 inspect.py:2857(__init__)
1 0.000 0.000 0.000 0.000 queues.py:59(_set_timeout)
2 0.000 0.000 0.000 0.000 {method 'extend' of 'list' objects}
1 0.000 0.000 0.000 0.000 {method '_is_owned' of '_thread.RLock' objects}
def mysucc(x, y):
return x + y
%%timeit
mysucc(41, 43)
24 ns ± 0.404 ns per loop (mean ± std. dev. of 7 runs, 10,000,000 loops each)
https://github.com/leanprover-community/repl
Hmm. Ingest response via microlean? Use simp
l.lean_simp
from kdrag.all import *
kd.lean("1 + 1.0")
import kdrag.printers.lean as plean
plean.of_expr
<function kdrag.printers.lean.of_expr(e: z3.z3.ExprRef)>