Leancrawler minimal example?

Stream: new members

[Mike Vaiana]

Does anyone have a minimal example of using leancrawler?

I followed these instructions to setup a new project and then I created Test.lean as described.

I installed leancrawler and ran it against Test.lean which does produce a crawl.lean file. But when I try lean --run crawl.lean I get a wall of errors. I'm doing everything in the terminal on Mac OS.

crawl.lean:1:0: error: unknown package 'MyProject'
You might need to open '/Users/mike/ae/alignment/provably-safe/lean/my_project' as a workspace in your editor
crawl.lean:6:5: error: unknown namespace 'tactic'
crawl.lean:6:45: error: unexpected token '('; expected command
crawl.lean:10:4: error: unexpected token ','; expected '↦', '=>'
crawl.lean:12:5: error: unexpected token 'attribute'; expected 'binder_predicate', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'postfix', 'prefix' or 'syntax'
...

[Alex J. Best]

Leancrawler is a tool for lean 3, and it looks like you are trying to run with/on a lean 4 project

[Mike Vaiana]

Oh ok, thanks. The README says "Lean 3.26 or later" but they probably just mean the minor version. Is there any tool that can be used map out dependencies in Lean4?

[Patrick Massot]

I’ll add a deprecation banner right now, sorry about the confusion.

[Mike Vaiana]

@Patrick Massot No problem! Thanks for the reply. Do you know if anyone has any plans to do something like this for Lean4?

[Patrick Massot]

I’m sure I saw messages about such tools. Maybe @Scott Morrison knows?

[Kim Morrison]

@Mike Vaiana, could you say what you are trying to do?

I'm not sure there is a drop-in replacement for leancrawler. Mostly in Lean 4 this sort of stuff is so much easier, that often people just write one off metaprograms for their task.