chore: split deps and test tasks in Taskfile.yml

[aumrp77]

This PR separates the “deps” and “test” steps in our Taskfile, so that installing dependencies and running tests are two independent tasks:

• deps task now only:
  • upgrades pip
  • installs Python packages from requirements.txt
  • installs Lean (via elan)
• test task now:
  • depends on deps
  • sources the elan env
  • sets PYTHONPATH
  • runs pytest

This makes CI faster (tests aren’t run during deps) and ensures Lean is on PATH when pytest spins up.

Verification

task test   # ✅ 9 tests passed, 1 warning

[Adarsh321123]

Hi @aumrp77! Thanks for this contribution! Can you please verify that the code in this PR still produces the same results as the original paper? For sanity checking correctness, we can simply run the new task run workflow on a small set of repos (like just Compfiles and MIL) and compare key metrics/outputs against those in the paper. Moreover, to check that the entire workflow works, we can use a separate blank repo. You can quickly do these by following the README.md and then hardcoding those repositories in leanagent.py.

[motiwari]

Hi @aumrp77 , my apologies for the delay in getting back to you after our 1:1 discussion.

As @Adarsh321123 mentioned, are you able to run some sanity checks to reproduce the approximate numbers from the paper for 1 or 2 repos? This would help give us confidence that your code changes don't break anything. (He updated the comment with more instructions, which may not have sent you a new notification).

I spoke with @Adarsh321123 and it seems the only way to do this would be to have access to GPUs and run the experiments for some time.

@Adarsh321123 can you remind me of our discussion, and how we were discussing testing the code changes in the fastest way possible, to ensure the new changes don't break anything? I believe we talked about caching the static data, and then we should be able to run on a single repo in an hour or two. Could you remind me of the details and plan on how to do that?