making a lean executable available in a project

Stream: lean4

[Damiano Testa]

I have a fundamental misunderstanding of how to make a lake exe myScript available in a different project.

Say that I have new lean project that provides lake exe myScript. I would like now to make the script available in mathlib. What steps should I take?

I imagine that I should add a require line to the lakefile and this seems to work well. What else should I do? Specifically, how do I make sure that the path that lean uses is the correct one inside .lake/package/myScripts? Is there anything else that I should do?

[Damiano Testa]

I have been trying this for a while with no success. I could get lake exe myScript --help to display the help message, but can't get past errors like

uncaught exception: unknown package 'myScript'
You might need to open '/home/damiano/Lean4' as a workspace in your editor

to show up.

[Adam Topaz]

If mathlib requires your project then lake exe myScript should work, no?

[Damiano Testa]

I cannot get it to work.

[Damiano Testa]

I run lake update myScript and it seems to do something (no warnings, nor errors, just infos).

[Damiano Testa]

After that, lake env myScript --help works (note the env, not exe).

[Adam Topaz]

is it a lake executable or a script?

[Damiano Testa]

But anything exe gives me the error above.

[Adam Topaz]

if it's a script then I think lake run projName/myScript is the syntax

[Damiano Testa]

What is the difference between an executable and a script?

[Adam Topaz]

Anyway, @Mac Malone is the person to ask

[Damiano Testa]

I tried to write something like lake exe mk_all, but in a separate repo.

[Adam Topaz]

what does the lakefile of your external project look like?

[Damiano Testa]

This is the repo and the lakefile is

import Lake
open Lake DSL

package updateDeprecations where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩
  ]

require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"

@[default_target]
lean_lib UpdateDeprecations where
--  -- add library configuration options here

/-- `lake exe update_deprecations` automatically updates deprecations. -/
@[default_target]
lean_exe update_deprecations where
  srcDir := "UpdateDeprecations"
  root := `Main
  supportInterpreter := true

[Adam Topaz]

right, so I think lake exe update_deprecations should work in any project that requires this.

[Damiano Testa]

(mostly cargo-culted from elsewhere, so could be nonsense, but in the project, lake exe update_deprecations works.)

[Damiano Testa]

Adam Topaz said:

right, so I think lake exe update_deprecations should work in any project that requires this.

I would have thought so as well, but...

[Adam Topaz]

how do you require this project in another one?

[Damiano Testa]

I added

require UpdateDeprecations from git "https://github.com/adomani/UpdateDeprecations" @ "caps_dev"

after the other requires in mathlib.

[Adam Topaz]

It should be require updateDeprecations from git ... (note the capitalization)

[Damiano Testa]

(caps_dev is a non-master branch in which I am doing some development.)

[Adam Topaz]

as far as I understand the foo in require foo from ... needs to match foo in package foo where ...

[Damiano Testa]

and still lake update updateDeprecations after changing the require, right?

[Adam Topaz]

maybe... may as well just to be safe

[Damiano Testa]

$ lake update updateDeprecations
info: updateDeprecations: cloning https://github.com/adomani/UpdateDeprecations to '././.lake/packages/updateDeprecations'
error: mathlib: package 'UpdateDeprecations' was required as 'updateDeprecations'

[Damiano Testa]

(the capitalisation again...)

[Damiano Testa]

$ lake update UpdateDeprecations
info: updateDeprecations: cloning https://github.com/adomani/UpdateDeprecations to '././.lake/packages/updateDeprecations'
error: mathlib: package 'UpdateDeprecations' was required as 'updateDeprecations'

[Adam Topaz]

sigh... the only guess I have is to purge the lake manifest and/or .lake and try from scratch, but there may be a more surgical fix.

[Damiano Testa]

I have been playing with this for a bit, but I had started by cloning mathlib again...

[Damiano Testa]

Anyway, besides the require line, I should not be adding anything else to the lakefile, right?

[Adam Topaz]

I think that's right.

[Damiano Testa]

(to the lakefile or anywhere else in mathlib)

[Damiano Testa]

I have a feeling that what I am failing to communicate to lake is the path where the code is written.

[Damiano Testa]

(I can see the code in .lake/packages//UpdateDeprecations, but I get the impression that lake expects to find it inside the root dir of mathlib.)

[Adam Topaz]

I tested this in a plain lean project with the following lakefile:

import Lake
open Lake DSL

require updateDeprecations from git "https://github.com/adomani/UpdateDeprecations"

package «test» where
  -- add package configuration options here

lean_lib «Test» where
  -- add library configuration options here


@[default_target]
lean_exe «test» where
  root := `Main

[Damiano Testa]

... and it works?

[Adam Topaz]

running lake exe update_deprecations worked with no errors (except for "There are out of date oleans. Run lake build or lake exe cache get first", which may be expected)

[Damiano Testa]

Would you mind adding this file

theorem hi : True := .intro

@[deprecated hi]
theorem True.the_old_hi : True := .intro

open True
example : True ∧ True := by
  constructor
  exact True.the_old_hi
  exact the_old_hi

and running lake exe update_deprecations --mods pathToFile?

[Damiano Testa]

(after lake build file?)

[Damiano Testa]

Ideally, the script should change the file to

theorem hi : True := .intro

@[deprecated hi]
theorem True.the_old_hi : True := .intro

open True
example : True ∧ True := by
  constructor
  exact hi
  exact hi

[Damiano Testa]

(in particular, it should succeed!)

[Adam Topaz]

It ran with no output to stdout, and the file remained

theorem hi : True := .intro

@[deprecated hi]
theorem True.the_old_hi : True := .intro

open True
example : True ∧ True := by
  constructor
  exact True.the_old_hi
  exact the_old_hi

[Damiano Testa]

Hmm, it should have told you that it changed 1 file, 2 replacements and should have changed the file...

[Damiano Testa]

Ok, thanks, I'll play with an "empty" project for a bit.

[Adam Topaz]

what's the path? is it the name of the module or the actual filepath?

[Damiano Testa]

Whichever you prefer: the script handles both.

[Damiano Testa]

(unlike lake build file)

[Adam Topaz]

I ran it, but now it's giving me the message "There are out of date oleans..." no matter how many times I build the file.

[Adam Topaz]

But in any case, the executable seems to be working in my test project.

[Damiano Testa]

Ok, thank you very much for trying! I'll debug more. It is encouraging that it seems to run, maybe with bugs in my script!

[Adam Topaz]

No problem!

[Damiano Testa]

Adam, I suspect that what you were seeing was maybe since your toolchain was not on leanprover/lean4:v4.8.0-rc1 or later. However, even with that, I still get the same error

$ lake env update_deprecations --mods Test/withDeprecations.lean
uncaught exception: unknown package 'UpdateDeprecations'
You might need to open '/home/damiano/gclones' as a workspace in your editor

:shrug:

[Jon Eugster]

Interesting: It works perfectly fine if I clone your repo and require it as a local dependency, but it gives the error you mentioned when requiring it from github...

And I think the problem is in the line

let env : Environment ← importModules #[{module := `UpdateDeprecations.Main}] {}

which throws the mentioned error unknown package UpdateDeprecations. However, I do not know why either.

[Jon Eugster]

So with require updateDeprecations from ".." / "UpdateDeprecations" it does the following modifications as expected:

--- a/Test/Basic.lean
+++ b/Test/Basic.lean
@@ -8,5 +8,5 @@ theorem True.the_old_hi : True := .intro
 open True
 example : True ∧ True := by
   constructor
-  exact True.the_old_hi
-  exact the_old_hi
+  exact hi
+  exact hi

[Jon Eugster]

Actually, I think it's the srcDir in the lean_exe config that messes things up. With the following entry the script runs perfectly fine for me:

/-- `lake exe update_deprecations` automatically updates deprecations. -/
@[default_target]
lean_exe update_deprecations where
  -- srcDir := "UpdateDeprecations"
  root := `UpdateDeprecations.Main
  supportInterpreter := true

Don't ask me why... :sweat_smile: I'd love to understand why the srcDir only messes with things in the case where one has require ... from git ..., but not when require ... from ".." / ...

[Adam Topaz]

Is this a bug in lake?

[Damiano Testa]

@Jon Eugster thank you so much! I will do some testing soon, but I am glad that you could get it to work!

[Damiano Testa]

I had also zoomed in on importModules, as you can see from the dbg_traces around it, but could not use that to fix the issue anyway...

[Damiano Testa]

By the way, I think that all the lake exe cmds that mathlib uses are from scripts that are contained in mathlib's root dir. I wonder whether this is just because something similar goes on there and it is not possible to just make them available in .lake/packaged...

[Damiano Testa]

E.g., if I wanted to disengage lake exe mk_all from mathlib, I would probably run in the same issue, right?

[Damiano Testa]

I tried, but I could not get the script to work on a new project even in the form require ... from ".." / .... I assume that ".." / ... refers to the relative path of the dir with the local clone of the UpdateDeprecations repo, right?

[Jon Eugster]

yes, relative from the downstream's project folder, so if e.g. mathlib and std were both folders inside a Lean folder, you could write require std from ".." / "std" in the mathlib's lakefile.

I can try to recreate a fully reproducible setup tomorrow and maybe also use it to issue an issue about the srcDir behaviour

[Mac Malone]

Adam Topaz said:

Is this a bug in lake?

It certainly sounds like one. :disappointed:

[Damiano Testa]

Well, hopefully it is one that can be fixed! :smile:

[Jon Eugster]

@Damiano Testa could you try if just calling lake build updateDeprecations (or capital U, forgot which one you had) before the lake exe update_deprecations works for you? (that's all in the repo the requires your updateDeprecations)

Here is a repo with a full reproduction of what I think happens: https://github.com/joneugster/test_deprecation . I think it's just that UpdateDeprecations.Main is not built and therefore it cannot be imported. You can work around this by adding a post-update hook like this one: build gameserver

[Damiano Testa]

Jon, I followed the steps in your repo and I can reproduce your results for the initial version, requiring from git. However, I was not able to get the "local" one to work: I used the commented out line in the lakefile, and commented out the initial one (from git) instead.

$ lake exe update_deprecations
⚠ [1/3] Built Main
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:4:10: unused variable `args`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:15:6: unused variable `mFile`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:19:6: unused variable `env`
note: this linter can be disabled with `set_option linter.unusedVariables false`
current dir: /home/damiano/gclones/test_deprecation
first entry of search path: ./././UpdateDeprecations/.lake/build/lib
Use `ls` to see if it contains `UpdateDeprecations/Main.olean`
uncaught exception: unknown package 'UpdateDeprecations'
You might need to open '/home/damiano/gclones/test_deprecation' as a workspace in your editor

[Jon Eugster]

I just deleted the instructions for the local case, because I think that analysis was wrong and it doesn't actually matter if it's local or not.

The only thing that matters is whether ./UpdateDeprecations/.lake/build/lib/UpdateDeprecations/Main.olean exists or not.

what does ls ./UpdateDeprecations/.lake/build/lib show right now?

[Damiano Testa]

Here is what I see:

$ ls ./UpdateDeprecations/.lake/build/lib
Main.ilean  Main.ilean.hash  Main.log.json  Main.olean  Main.olean.hash  Main.trace

[Jon Eugster]

and lake exe update_deprecations still gives you that error?

[Damiano Testa]

Just now, next command issued after the one above:

$ lake exe update_deprecations
⚠ [1/3] Replayed Main
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:4:10: unused variable `args`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:15:6: unused variable `mFile`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:19:6: unused variable `env`
note: this linter can be disabled with `set_option linter.unusedVariables false`
current dir: /home/damiano/gclones/test_deprecation
first entry of search path: ./././UpdateDeprecations/.lake/build/lib
Use `ls` to see if it contains `UpdateDeprecations/Main.olean`
uncaught exception: unknown package 'UpdateDeprecations'
You might need to open '/home/damiano/gclones/test_deprecation' as a workspace in your editor

[Jon Eugster]

and the lake-manifest currently does have the local dependency in it?

[Jon Eugster]

then something isn't quite rigtht with that part of the analysis :(

[Damiano Testa]

$ cat lake-manifest.json
{"version": 7,
 "packagesDir": ".lake/packages",
 "packages":
 [{"type": "path",
   "name": "updateDeprecations",
   "manifestFile": "lake-manifest.json",
   "inherited": false,
   "dir": "./UpdateDeprecations",
   "configFile": "lakefile.lean"}],
 "name": "test_deprecation",
 "lakeDir": ".lake"}

[Damiano Testa]

(Note that I am not following very well what is going on, so I am not really able to help much more than by being willing to try things out on my computer...)

[Jon Eugster]

Ah

[Jon Eugster]

so you get this:

$ ls ./UpdateDeprecations/.lake/build/lib
Main.ilean  Main.ilean.hash  Main.log.json  Main.olean  Main.olean.hash  Main.trace

now if you do

lake build updateDeprecations
ls .lake/packages/updateDeprecations/.lake/build/lib

you might get more in that folder:

Main.ilean       Main.log.json  Main.olean.hash  UpdateDeprecations        UpdateDeprecations.ilean.hash  UpdateDeprecations.olean       UpdateDeprecations.trace
Main.ilean.hash  Main.olean     Main.trace       UpdateDeprecations.ilean  UpdateDeprecations.log.json    UpdateDeprecations.olean.hash

[Damiano Testa]

Here is what I get with literally what you said:

$ lake build updateDeprecations
⚠ [1/6] Replayed UpdateDeprecations.Main
warning: ./././UpdateDeprecations/././UpdateDeprecations/Main.lean:4:10: unused variable `args`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/././UpdateDeprecations/Main.lean:15:6: unused variable `mFile`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/././UpdateDeprecations/Main.lean:19:6: unused variable `env`
note: this linter can be disabled with `set_option linter.unusedVariables false`
⚠ [4/6] Replayed Main
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:4:10: unused variable `args`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:15:6: unused variable `mFile`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:19:6: unused variable `env`
note: this linter can be disabled with `set_option linter.unusedVariables false`
Build completed successfully.

$ ls .lake/packages/updateDeprecations/.lake/build/lib
ls: cannot access '.lake/packages/updateDeprecations/.lake/build/lib': No such file or directory

[Damiano Testa]

Let me search for where Main.ilean.hash really is, though.

[Damiano Testa]

$ find . -iname '*Main.ilean.hash*'
./UpdateDeprecations/.lake/build/lib/Main.ilean.hash
./UpdateDeprecations/.lake/build/lib/UpdateDeprecations/Main.ilean.hash

[Damiano Testa]

$ ls ./UpdateDeprecations/.lake/build/lib/UpdateDeprecations/
Main.ilean  Main.ilean.hash  Main.log.json  Main.olean  Main.olean.hash  Main.trace

I seem to be missing the UpdateDeprecations files.

[Jon Eugster]

Yes, that's what I meant to say, so without lake build updateDeprecations it doesn't have these and my claim is that if you run this build command and look at the same folder again, you'll find them there

[Jon Eugster]

wait I'll better write that up again :sweat_smile:

[Damiano Testa]

Ah, but was this not what I did before? I seem to be getting something different now:

$ lake build updateDeprecations
⚠ [1/6] Replayed UpdateDeprecations.Main
warning: ./././UpdateDeprecations/././UpdateDeprecations/Main.lean:4:10: unused variable `args`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/././UpdateDeprecations/Main.lean:15:6: unused variable `mFile`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/././UpdateDeprecations/Main.lean:19:6: unused variable `env`
note: this linter can be disabled with `set_option linter.unusedVariables false`
⚠ [4/6] Replayed Main
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:4:10: unused variable `args`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:15:6: unused variable `mFile`
note: this linter can be disabled with `set_option linter.unusedVariables false`
warning: ./././UpdateDeprecations/./UpdateDeprecations/Main.lean:19:6: unused variable `env`
note: this linter can be disabled with `set_option linter.unusedVariables false`
Build completed successfully.

$ ls ./UpdateDeprecations/.lake/build/lib
Main.ilean       Main.log.json  Main.olean.hash  UpdateDeprecations        UpdateDeprecations.ilean.hash  UpdateDeprecations.olean       UpdateDeprecations.trace
Main.ilean.hash  Main.olean     Main.trace       UpdateDeprecations.ilean  UpdateDeprecations.log.json    UpdateDeprecations.olean.hash

[Damiano Testa]

But this is (at least) the second time that I run lake build updateDeprecations, so does this mean that you need to run it a few times before it is done updating all that it should?

[Damiano Testa]

(I am really trying to understand, but I can clearly see that there is something very basic that I am still failing to grasp.)

[Jon Eugster]

I think with these tests, there are two folders .lake/ and UpdateDeprecations/.lake and it's really hard to really do any clean tests and not accidentially have builds in these folders without realising, making it hard to really construct something reproducible.

Anyways, I think the "local repo" was a distraction and has nothing to do with it. And I just got lucky because I had the local repo built accidentially and didn't clear that properly.

I think the behaviour that is important here is the following:

start from a fresh copy of the repo, e.g. git cloneor in the repo:

git checkout -- .
rm -rf .lake/

lake exe update_deprecations
ls .lake/packages/updateDeprecations/.lake/build/lib/

shows:

Main.ilean  Main.ilean.hash  Main.log.json  Main.olean  Main.olean.hash  Main.trace

but then doing

lake build updateDeprecations
lake exe update_deprecations
ls .lake/packages/updateDeprecations/.lake/build/lib/

shows

Main.ilean       Main.log.json  Main.olean.hash  UpdateDeprecations        UpdateDeprecations.ilean.hash  UpdateDeprecations.olean       UpdateDeprecations.trace
Main.ilean.hash  Main.olean     Main.trace       UpdateDeprecations.ilean  UpdateDeprecations.log.json    UpdateDeprecations.olean.hash

the first round of theses then fails because it doesn't find a file .lake/packages/updateDeprecations/.lake/build/lib/UpdateDeprecations/Main.olean and while the second round succeeds, there are now two identical files

.lake/packages/updateDeprecations/.lake/build/lib/Main.olean
.lake/packages/updateDeprecations/.lake/build/lib/UpdateDeprecations/Main.olean

floating around.

[Damiano Testa]

Ok, I can empirically confirm that this is indeed what seems to happen. The expectation though would be that running lake exe update_deprecations should implicitly run lake build updateDeprecations, in case this was not ran already? And that there should not be duplication, I imagine?

[Jon Eugster]

That seems correct. Here is a smaller reproduction: https://github.com/joneugster/testSrcDir2

I guess if the duplication caused by srcDir is considered a bug, and that one would be addressed, then the implicit calling of lake build ... wouldn't be necessary.

[Jon Eugster]

lean4#4419

[Mac Malone]

Mac Malone said:

Adam Topaz said:

Is this a bug in lake?

It certainly sounds like one. :disappointed:

I just saw the report in lean4#4419. I left a comment there, but I will repeat and elaborate a bit there. It was not clear to me orginally that the source of this issue was the attempt to import the main module of an executable. That is purposely designed to not be directly doable. This is because importing an module that defines main causes a number of problems for Lean. Thus, it appears things were working as intended.

On the flip side, the fact that the issue here was unclear indicates there is probably something Lake should be doing to make this more obvious for the end user. One possibility is for Lake to complain if a library imports a module defined as an executable.

[Jon Eugster]

Once I understood what happened I also assumed that it might be "working as intended", which I guess I didn't really write in the report explicitely. But by the time I understood what was happening, I thought it might be as well noted in form of an issue.

I agree that just failing better from Lean's/lake's side would be good. I think I deleted that sentense accidentially but I meant to write something like

A simpler fix could be to just improve the error message as the current message You might need to open 'parentDir/' as a workspace in your editor (from here) is in this case wrong and misleading

[Damiano Testa]

So, here is a summary to clear up some of my confusion.

I define a lean command in a myCmd repo. In this repo, I add it as lean_exe in my lakefile and it just works for me.

However, I would like to run it lean exe myCmd in a separate repo newRepo. For this, I add a require statement to the lakefile of newRepo and in that same lakefile I add lean_lib myCmd and not a lean_exe entry.

Is this correct?

[Mac Malone]

Damiano Testa said:

I define a lean command in a myCmd repo. In this repo, I add it as lean_exe in my lakefile and it just works for me.

However, I would like to run it lean exe myCmd in a separate repo newRepo. For this, I add a require statement to the lakefile of newRepo and in that same lakefile I add lean_lib myCmd and not a lean_exe entry.

Is this correct?

No. The problem here was not the configuration of lean_exe/lean_lib. You should run a lean_exe myCmd always as lake exe myCmd.

The problem here is with how your UpdateDeprecations.Main is defined. You should generally never be importing a module which defines main (i.e., the root of of lean_exe) as Lean does special compilation for such modules that makes them not intended for libraries. Currently your UpdateDeprecations.Main is imported by UpdateDeprecations and is also imported via importModules.

The best way to fix this would to be to define a root-level Main.lean file containing the main function which imports UpdateDeprecations (the library) and have importModules similar import UpdateDeprecations. And ideal folder structure would look like:

repo/
  UpdateDeprecations.lean -- `UpdateDeprecations.Main` w/o `main`
  TUD.lean -- your practice file
  Test.lean -- your test file
  Main.lean -- file with `main` function
  lakefile.lean

The contents of Main.lean would be:

import UpdateDeprecations

/-- The entrypoint to the `lake exe update_deprecations` executable. -/
def main (args : List String) : IO UInt32 := UpdateDeprecations.updateDeprecations.validate args

And your lakefile lean_lib / lean_exe would then look like this:

lean_lib UpdateDeprecations

/-- `lake exe update_deprecations` automatically updates deprecations. -/
@[default_target]
lean_exe update_deprecations where
  root := `Main
  supportInterpreter := true

You can then run your update_deprecations executable from any package (itself or downstream dependecies like newRepo) using lake exe update_deprecations.

[Damiano Testa]

@Mac Malone thank you so much for this detailed explanation! I could follow all the steps, correct my mistakes and now indeed I was able to use the UpdateDeprecations via lake exe update_deprecations on Mathlib with just the require line!