Zulip Chat Archive

Stream: lean-gptf

Topic: Troubleshooting


view this post on Zulip Jesse Michael Han (Jan 18 2021 at 17:18):

Known issues:

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

view this post on Zulip Alex J. Best (Jan 19 2021 at 06:03):

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:

view this post on Zulip Jesse Michael Han (Jan 19 2021 at 14:07):

thanks for experimenting with this Alex!

view this post on Zulip Alex J. Best (Jan 19 2021 at 18:23):

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)

view this post on Zulip Alex J. Best (Jan 19 2021 at 18:27):

Oh I guess I can do

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

seems a bit hacky though :grinning:

view this post on Zulip Jesse Michael Han (Jan 19 2021 at 18:30):

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

view this post on Zulip Alex J. Best (Jan 20 2021 at 02:41):

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

view this post on Zulip Jesse Michael Han (Jan 20 2021 at 19:35):

merged, thanks for figuring this out!


Last updated: May 18 2021 at 10:14 UTC