search

albertqjiang / draft_sketch_prove

Other
61 stars 8 forks source link

Missing file for the Code to Run #1

Closed chuanyang-Zheng closed 1 year ago

chuanyang-Zheng commented 1 year ago

Dear Albert , We are sorry to disturb you.

Does it seem that the needed files are missing in the code? For example

  1. script/alber/In parallel_codex_query_canon.py, there is no the needed aligned_problems/new_complete_mini.jsonl
  2. In autoformalize_minif2f_math.py, there is no the needed aligned/aligned_mathd_minif2f.json and Isabelle2021/src/HOL/Examples.

As I just begin learning the proposed DSP, there may be other missed files that I do not mention above.

Again, thank you very much for your attention and support, and look forward to hearing from you.

Best regards, Chuanyang

albertqjiang commented 1 year ago

Added new_complete_mini.jsonl in newest commit.

I don't think you'd need the autoformalize_minif2f_math.py at all.