Running benchmarks interactively?

Stream: lean4 dev

[Rish Vaishnav]

Hi, I'm trying to interactively see the results from a benchmark test file (specifically tests/bench/workspaceSymbols.lean) but it seems that if I modify the relevant files and then reload the benchmark file, it doesn't pick up my changes. I was wondering why this situation would be different from modifying anything else in our codebase (as changes seem to be picked up fine elsewhere).

Also, how do I run a particular benchmark test (or test in general) non-interactively? There's probably a way to pass in the name of a specific test when doing make test right? (and let me know if there's some documentation I've neglected to read). Thanks!

[Gabriel Ebner]

Yeah, you need to run make first if you work on core. Unlike lake-based projects, dependencies are not recompiled automatically.

[Rish Vaishnav]

Oh really! Then I'm not sure why I was under the impression that this had worked before lol, I guess I assumed I would have noticed it by now if it didn't but in reality I've only modified one file at a time so far :laughing:

So your workflow when modifying a dependency in core is to run make and then restart the language server right?

[Gabriel Ebner]

You don't need to restart the server, just the file (i.e, :e or :LeanRestartFile).

[Rish Vaishnav]

Oh right that make sense, because all you need is for the .oleans to be updated. Thanks for adding that command to the neovim plugin :pray:

[Rish Vaishnav]

A somewhat related question, is there a way to fetch the latest master binary, and all of the make dependencies along with it? I did a rebase of lean4#1710 onto master today and make took ~20 minutes to run for me...

[Rish Vaishnav]

(like, an analogue of leanproject get-mathlib-cache for developers)

[Sebastian Ullrich]

Only the Nix setup supports this currently (because it was trivial there)

[Sebastian Ullrich]

Make sure you have ccache installed to avoid most of the recompilation time