search

jesse-michael-han / lean-gptf

Interactive neural theorem proving in Lean
Apache License 2.0
118 stars 6 forks source link

More care should be taken escaping json (on Windows at least) #2

Closed alexjbest closed 3 years ago

alexjbest commented 3 years ago 
import tactic.gptf

example : ∃ s, "t" = s :=
begin
  gptf,
end

fails on windows with

[gptf_proof_search_step] run_best_beam_candidate UNEXPECTED MESSAGE:
---
["ERROR { \"error\":{ \"code\":null, \n    \"message\":\"Your request contained invalid JSON: Invalid \\\\escape: line 1 column 79 (char 78)\", \n    \"param\":null, \n    \"type\":\"invalid_request_error\"}}"]
---

as the json " escaping introduced in #1 is too simplistic.