Troubleshooting

Stream: lean-gptf

[Jesse Michael Han]

Known issues:

• the openai backend currently uses io.run_cmd curl ... and i'm unsure if this works on Windows; PRs welcome

[Alex J. Best]

Jesse Michael Han said:

Known issues:

• the openai backend currently uses io.run_cmd curl ... and i'm unsure if this works on Windows; PRs welcome

I just tried this, I modified a few different things but I think the only one that actually mattered in the end was that I had to escape the " in the JSON passed to curl i.e.

, json.unparse serialized_req

I changed to

, "\\\"".intercalate ((json.unparse serialized_req).split (= '\"'))

I'm not sure how much time I'll have to verify/check this and make a PR tomorrow, so I'll just leave it here for now and come back to this in a couple days if you don't fix it first :smile:

[Jesse Michael Han]

thanks for experimenting with this Alex!

[Alex J. Best]

Is anyone able to confirm if this change is breaking on osx / linux? I just was thinking about making a PR and I realised I have no idea how to detect from within lean the OS, so if the change isn't breaking that seems the easiest path. (Even if this does work, I would assume there must be a way to detect the OS without having to add a feature to lean and I'd love to know how if anyone does)

[Alex J. Best]

Oh I guess I can do

tactic.unsafe_run_io $ io.env.get "OS"

seems a bit hacky though :grinning:

[Jesse Michael Han]

please proceed with the PR, i can try it out on my linux machine :thumbs_up:

[Alex J. Best]

jesse-michael-han/lean-gptf#1 any other testers on osx or cygwin or anything welcome too :smile:

[Jesse Michael Han]

merged, thanks for figuring this out!