Many missing premises while training premise selector.

[ketchupfan]

Hello, I was trying to train the premise selector (specifically, this command: python retrieval/main.py fit --config retrieval/confs/cli_lean4_random.yaml --trainer.logger.name train_retriever_random --trainer.logger.save_dir logs/train_retriever_random) and after wandb sets itself up, I get a very long list of Warnings stating that it "cannot locate premise" for various different premises. After checking the requirements, I believe I have gone through all of the steps to get started. Furthermore, when I check ReProver/data/leandojo_benchmark_4/corpus.jsonl, I do find that all of the premises seem to be there. Any help as to how to resolve this would be greatly appreciated!

Warning message looks like this:

2025-02-19 10:01:14.550 | WARNING  | common:get_all_pos_premises:352 - Cannot locate premise: {'full_name': 'HasSubset.Subset.antisymm', 'def_path': 'Mathlib/Order/RelClasses.lean', 'def_pos': [658, 7], 'def_end_pos': [658, 32]}

except, there are many more similar such messages, each with reagards to a different premise (at least on first glance).

When editing get_all_pos_premises in common.py to tell me when premises were found, it appeared that a majority of the premises were being detected, so I'm not sure what's causing some of the other premises from being detected.