RFC: `lake exe` should provide suggestions

[kim-em]

Currently lake exe errors with error: missing executable name.

Can it list the available exes defined in the current and upstream projects? This would help discoverability.

[tydeu]

With this suggestion, should it still print an error / return exit code 1 or should it just produce the listing and exit normally?

[kim-em]

I think exit code 1 is appropriate, because only humans should ever be doing it: if a script called lake exe I'd still want it to fail.

(If there were lake describe exe or something, then that should exit normally.)

[tydeu]

@semorrison

(If there were lake describe exe or something, then that should exit normally.)

There is lake help exe, but loading the workspace as part of help seems like undesirable overhead,

[sullyj3]

Is there any reason lean exe couldn't just execute the default_target? Similar to cargo run.

[tydeu]

@sullyj3 It could, but there are some things to consider:

1. Unlike cargo run, arguments are passed without a -- separator, so a lake exe with a named exe would have to take no arguments.
2. A package can have multiple executables and multiple default targets, and the default targets do not have to be executables. Thus, it could be quite unclear what executable would run.

[digama0]

Unlike cargo run, arguments are passed without a -- separator, so a lake exe with a named exe would have to take no arguments.

In many/most CLIs the -- separator is only for disambiguation purposes and can be omitted. So you could still allow lake exe <args>, provided that the <args> are not interpretable as lake arguments or an exe name. And -- would be available when this results in an incorrect interpretation, i.e. lake exe -- <args> unambiguously calls the default target with <args>.

Re: 2, you could have another attribute or workspace setting for defining the default executable in ambiguous cases.

[sullyj3]

This is how it works in cargo: (from the man page)

Target Selection
       When no target selection options are given, cargo run will run the binary target. If there are
       multiple binary targets, you must pass a target flag to choose one. Or, the default-run field
       may be specified in the [package] section of Cargo.toml to choose the name of the binary to run
       by default.

       --bin name
           Run the specified binary.

I think this behaviour makes a lot of sense; executing the sole exe of your project if it is the sole exe, and only requiring you to specify in case of ambiguity

[digama0]

This does make the very common invocation lake exe cache get significantly longer though: lake exe --bin cache -- get.

Note that cargo has an alternative mechanism to mitigate this, namely cargo install, which allows you to create custom cargo commands called like cargo my-exe <args>.

[sullyj3]

This does make the very common invocation lake exe cache get significantly longer though: lake exe --bin cache -- get.

I'm not necessarily suggesting the --bin flag, just the selection in case of no exe specified.

[sullyj3]

how about:

• lake exe cache get continues to work as is
• lake exe -- arg1 arg2 executes the sole executable if it exists and fails if there are a non-one number of executables.
• lake exe arg1 arg2 intending to execute the sole executable should fail with a message along the lines of

error: unknown executable arg1 If you meant to pass arguments to my-sole-exe, run lake exe -- arg1 arg2

[nomeata]

Is that complexity really helpful, compared to the straight forward status quo? The current design is more uniform, works independent whether you are in the project of the executable or a downstream project, and you can add more executables to your project without breaking existing scripts/muscle memory.

[digama0]

If it is possible to select the default executable, then it is possible to add executables without breaking existing scripts / muscle memory. If there is only one executable though I agree there is no need to set a default.

[sullyj3]

I think there should be a strong presumption towards making the overwhelmingly common case convenient. The overwhelmingly common case is running the program you're writing.

Typing out the name of my exe is annoying, and the fact that it's trivial to infer adds insult to injury. In the scheme of things this is a minor issue. However, in my opinion small inconveniences add up, and they should be eliminated wherever they arise in order to make the overall experience attractive. I think accretion of minor annoyances is the sort of thing that turns people off of established languages. Lean is young, so we put up with mild annoyances temporarily. But I think the aim should be to make UX seamless if the goal is to attract users.