Running `lake` scripts from the command line

Stream: lean4

[Anand Rao Tadipatri]

Previously, I used to run lake scripts from the command line by typing lake run <package-name>/<script-name> (or lake run <script-name> when working from the project where the script is defined). However, this no longer seems to be working for me on lean4:v4.8.0-rc1. Has the behaviour of lake changed with the update? I also tried lake script run ..., but this variant also gives the error message error: unknown script lean-slides/serve-slides.

The actual script in question is this one, which I used to be able to run in downstream dependencies through lake run lean-slides/serve-slides. The name of this script still appears as a suggestion when I run lake scripts, so I'm hoping it's only the command that has changed.

[Kim Morrison]

Pinging @Mac Malone for this one.

[Mac Malone]

This sounds like a bug. The Lake test suite does have a test for run scripts from upstream dependencies, so a breaking #mwe could be helpful. I will also check to see if I can reproduce with lean-slides myself.

[Andrés Goens]

@Mac Malone FWIW I've found an MWE for this, it seems to be something with the name of the script. The following in the lakefile (in an otherwise fresh project)

script foo do
  IO.println "hello"
  return 0

script «foo-bar» do
  IO.println "hello"
  return 0

results in:

[goens@thinkpad-goens:/tmp]$ lake run foo
hello

[goens@thinkpad-goens:/tmp]$ lake run foo-bar
error: unknown script foo-bar

[Andrés Goens]

and for anyone else looking for a workaround, renaming serve-slides to serve or so in the lakefile makes it work

[Eric Wieser]

Does it work if you include the french quotes on the command line?

[Andrés Goens]

Eric Wieser said:

Does it work if you include the french quotes on the command line?

it does! nice!

[Andrés Goens]

(I'd still think it's a bug, right? just that makes the workaround even easier, calling lake run  lean-slides/«serve-slides»)

[Mac Malone]

Fix up at lean4#4564.