metaprogramming twitch stream

Stream: general

[Quinn]

https://www.twitch.tv/quinn_dougherty project: jsonable ASTs of proofs for machine learning reasons

[Quinn]

going live in just a sec

[Adam Topaz]

Have you seen https://github.com/andrejbauer/lean2sexp ?

[Quinn]

no, thanks!!!!

[Adam Topaz]

I dont think there anything there that converts sexprs to json, but that should be really easy (it may even be possible to automatically derive a ToJson instance)

[Quinn]

dude this rocks so hard. i had no idea. thanks so much

[Quinn]

#synth ToJson Sexp does fail, but i can hand roll it

[Adam Topaz]

You can try to derive it

[Quinn]

what's the difference between derive and #synth? i thougth they were working with the same underlying capacties

[Quinn]

huh. you're right. going into source and adding deriving ToJson worked, even tho synth failed and when i tried to handroll it i thought i'd have to bypass termination checker or something

[Adam Topaz]

import Lean

inductive Sexp : Type
| atom : String → Sexp
| string : String → Sexp
| integer : Int → Sexp
| double : Float → Sexp
| cons : List Sexp → Sexp
deriving Inhabited, Lean.ToJson

#synth Lean.ToJson Sexp

[Adam Topaz]

you need to tell lean to explicitly derive the instance. #synth is for typeclass instances that already exist.

[Quinn]

oh. i was totally wrong about what synth is then

[Julian Berman]

I'm not sure this is correct (so I'll say it so someone points out a counterexample) but I don't think #foo commands ever have side effects (so it wouldn't create an instance)

[Adam Topaz]

#foo commands could have side effects, but in practice they don't

[Julian Berman]

Yeah I meant stylistically to be clear.

[Quinn]

i basically thought it checked if the synthesis was possible, i didn't think it was actually creating it

[Adam Topaz]

deriving does something different.

[Adam Topaz]

synth just uses the typeclass system, but deriving uses custom handlers to derive instances

[Patrick Massot]

Note that you can use deriving in another file, you don't have to edit the original definition.

[Quinn]

That's a great note as well!

[Adam Topaz]

Right (but I always forget the magic spell for this)

[Quinn]

What does that look like?

[Adam Topaz]

I thought it was deriving instance Lean.ToJson for Sexp or something like that?

[Patrick Massot]

Yes

[Adam Topaz]

@Quinn I'm watching your stream: you probably want IO.FS.Handle.putStrLn together with Json.compress (or just toString)

[Adam Topaz]

compress will make it into a single line

[Adam Topaz]

toString usage is toString j for j : Json

[Adam Topaz]

you can a moduledata from an olean, or from the environment header which is part of an environment