lean-dojo / LeanDojoChatGPT

ChatGPT plugin for theorem proving in Lean
https://leandojo.org
MIT License
112 stars 14 forks source link

Plugin for id complete-manifest not found - localhost plugins #4

Closed riccitensor closed 6 months ago

riccitensor commented 10 months ago

The plugin gets installed properly

Bildschirmfoto 2023-12-17 um 12 09 58

but then I can't make it work.

Bildschirmfoto 2023-12-17 um 12 13 04
yangky11 commented 10 months ago

This seems to be a known issue and is awaiting OpenAI's fix: https://community.openai.com/t/local-plugin-failure-via-localhost-plugin-id-not-found/475197/30

yangky11 commented 9 months ago

Related https://github.com/lean-dojo/LeanDojoChatGPT/issues/5