Impact of additional_imports on MiniF2F

[njuyxw]

I have a few questions regarding the 'additional_imports' argument. I noticed that the BFS prover sets additional_imports=['Mathlib.Tactics']. Could you please clarify if this has any positive impact on proving minif2f? I did not find any usage of it in Reprover (https://github.com/lean-dojo/ReProver). If additional_imports=[] is set, are there certain math problems in minif2f that cannot be proven? If so, why? Thank you very much for your assistance.

[objecti0n]

This code is internally used for testing MiniF2F and Compfiles. Compfiles use this as default import.

[njuyxw]

I encountered an issue while running proofsearch_internLM2-plus.py.
When executing the line 'with Dojo(theorem, hard_timeout=timeout,additional_imports=["Mathlib.Tactic"]) as (dojo, init_state): ', lean_dojo throws an error:
'lean_dojo.interaction.dojo:_read_next_line:530 - MiniF2F/Test.lean:1:0: error: object file './.lake/packages/mathlib/.lake/build/lib/Mathlib/Tactic.olean' of module Mathlib.Tactic does not exist'

However, the code runs successfully when I remove 'additional_imports=[]'. This problem appears unrelated to the version of lean_dojo based on my troubleshooting efforts. I am utilizing the minif2f4.7.0 dataset with lean version 4.7.0. I am uncertain about the cause of this error, hence I asked about the impact of using 'additional_imports=["Mathlib.Tactic"]' and whether this is allowed when proving mathematical problems in minif2f4.7.0.