Search with local data not working

[timechess]

When I updated the lean-explore package to v1.0.0 and ran lean-explore data fetch, I got the following output:

Downloading file 'lean_explore_data.db.gz' from 'https://pub-48b75babc4664808b15520033423c765.r2.dev/assets/0.2.0/lean_explore_data.db.gz' to '/home/yicheng/.lean_explore/cache/0.2.0'.
Decompressing '/home/yicheng/.lean_explore/cache/0.2.0/lean_explore_data.db.gz' to '/home/yicheng/.lean_explore/cache/0.2.0/lean_explore_data.db' using method 'auto'.
Downloading file 'main_faiss.index.gz' from 'https://pub-48b75babc4664808b15520033423c765.r2.dev/assets/0.2.0/main_faiss.index.gz' to '/home/yicheng/.lean_explore/cache/0.2.0'.
Decompressing '/home/yicheng/.lean_explore/cache/0.2.0/main_faiss.index.gz' to '/home/yicheng/.lean_explore/cache/0.2.0/main_faiss.index' using method 'auto'.
Downloading file 'faiss_ids_map.json.gz' from 'https://pub-48b75babc4664808b15520033423c765.r2.dev/assets/0.2.0/faiss_ids_map.json.gz' to '/home/yicheng/.lean_explore/cache/0.2.0'.
Decompressing '/home/yicheng/.lean_explore/cache/0.2.0/faiss_ids_map.json.gz' to '/home/yicheng/.lean_explore/cache/0.2.0/faiss_ids_map.json' using method 'auto'.
Installed data for version 0.2.0

But when I initialized a Service instance, I got the following error:

Traceback (most recent call last):
  File "/home/yicheng/TheoremForge/test.py", line 10, in <module>
    asyncio.run(main())
  File "/usr/lib/python3.12/asyncio/runners.py", line 194, in run
    return runner.run(main)
           ^^^^^^^^^^^^^^^^
  File "/usr/lib/python3.12/asyncio/runners.py", line 118, in run
    return self._loop.run_until_complete(task)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/lib/python3.12/asyncio/base_events.py", line 687, in run_until_complete
    return future.result()
           ^^^^^^^^^^^^^^^
  File "/home/yicheng/TheoremForge/test.py", line 5, in main
    service = Service()
              ^^^^^^^^^
  File "/home/yicheng/TheoremForge/.venv/lib/python3.12/site-packages/lean_explore/search/service.py", line 21, in __init__
    self.engine = engine or SearchEngine()
                            ^^^^^^^^^^^^^^
  File "/home/yicheng/TheoremForge/.venv/lib/python3.12/site-packages/lean_explore/search/engine.py", line 108, in __init__
    self._validate_paths()
  File "/home/yicheng/TheoremForge/.venv/lib/python3.12/site-packages/lean_explore/search/engine.py", line 121, in _validate_paths
    raise FileNotFoundError(
FileNotFoundError: Required file not found at /home/yicheng/TheoremForge/.venv/lib/python3.12/data/0.2.0/informalization_faiss.index. Please run 'lean-explore data fetch' to download the data.

It seems that the files were not downloaded correctly.

[justincasher]

This should be fixed in PR #63. The issue was that the data fetch was using an outdated manifest with old file names.

[justincasher]

v1.0.1 is now live on PyPI. To upgrade:

pip install --upgrade lean-explore
lean-explore data fetch

[timechess]

Now the data can be downloaded properly, but I have another concern. For now, after data fetch the following code still produces errors:

import asyncio
from lean_explore.search.service import Service

async def main():
    service = Service()
    results = await service.search("test query")
    print(results)

if __name__ == "__main__":
    asyncio.run(main())

Traceback (most recent call last):
  File "/home/yicheng/TheoremForge/test.py", line 10, in <module>
    asyncio.run(main())
  File "/usr/lib/python3.12/asyncio/runners.py", line 194, in run
    return runner.run(main)
           ^^^^^^^^^^^^^^^^
  File "/usr/lib/python3.12/asyncio/runners.py", line 118, in run
    return self._loop.run_until_complete(task)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/usr/lib/python3.12/asyncio/base_events.py", line 687, in run_until_complete
    return future.result()
           ^^^^^^^^^^^^^^^
  File "/home/yicheng/TheoremForge/test.py", line 5, in main
    service = Service()
              ^^^^^^^^^
  File "/home/yicheng/TheoremForge/.venv/lib/python3.12/site-packages/lean_explore/search/service.py", line 21, in __init__
    self.engine = engine or SearchEngine()
                            ^^^^^^^^^^^^^^
  File "/home/yicheng/TheoremForge/.venv/lib/python3.12/site-packages/lean_explore/search/engine.py", line 108, in __init__
    self._validate_paths()
  File "/home/yicheng/TheoremForge/.venv/lib/python3.12/site-packages/lean_explore/search/engine.py", line 121, in _validate_paths
    raise FileNotFoundError(
FileNotFoundError: Required file not found at /home/yicheng/TheoremForge/.venv/lib/python3.12/data/20260127_103630/informalization_faiss.index. Please run 'lean-explore data fetch' to download the data.

The path is not correct. I found the problem is in SearchEngine. The parameter use_local_data says If True, use DATA_DIRECTORY paths. If False, use CACHE_DIRECTORY paths (for downloaded remote data), which can cause confusion, especially when it is default to True. The following code works well:

import asyncio
from lean_explore.search.service import Service
from lean_explore.search.engine import SearchEngine

async def main():
    service = Service(
        engine=SearchEngine(
            use_local_data=False,
        ),
    )
    results = await service.search("test query")
    print(results)

if __name__ == "__main__":
    asyncio.run(main())

But it does not match the documentation. Maybe you need to update the doc page or change the default value.