search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
478 stars 72 forks source link

get_namespaces() method callable but not implemented #160

Closed AG161 closed 2 months ago

AG161 commented 2 months ago

I tried using the get_namespaces() method on a traced theorem and got the following output:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/agittis/miniconda3/envs/dj/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 352, in get_namespaces
    return self.traced_file.get_namespaces(self)
AttributeError: 'TracedFile' object has no attribute 'get_namespaces'

I checked the source code and the get_namespaces() method in TracedTheorem calls a get_namespaces() method from the corresponding traced file, but TracedFile does not have a get_namespaces() method. When I checked earlier commits, it seems this feature was implemented for Lean 3 and returned a "not implemented" error for Lean 4. Now that LeanDojo only supports Lean 4, the feature does not exist. Are there plans to add this feature (or remove the ability to call the method)? I think it would be useful to have because the namespaces determine how an LLM can or can't call tactics. I don't know if this is just a simple thing that was forgotten about or if it would take a lot of work, so I just wanted to check in and ask. Thanks!

Platform Information

yangky11 commented 2 months ago

Thanks for catching that. I forgot the remove the get_namespaces for TracedTheorem. There is no short-term plan to implement it for Lean 4.