LeanInk: unknown command 'print-paths'

Stream: lean4

[Utensil Song]

As I have been using leanprover/LeanInk with Alectryon, I just noticed that after bumping to lean4:v4.4.0-rc1, it fails with

error: unknown command 'print-paths'
uncaught exception: Using lake failed! Make sure that lake is installed!

This can be traced back to its LeanInk/Analysis/LeanContext.lean which relies on print-paths to initializeLakeContext. As this command line option is gone since lean4#2858 , leanprover/LeanInk no longer works.

doc-gen4 survived because it depends on https://github.com/hargoniX/LeanInk/ which is 30+ commits behind and doesn't have that file. I can't figure out how Alectryon in Lean 4 repo survived, except maybe because it's in nix workflow.

[Marc Huisinga]

I'm a bit surprised that there are so many downstream users of this supposedly internal command for communication between Lake and the language server.
print-paths <imports of a file> has been replaced by setup-file <path to the file> <imports of the file>.
For some duct-tape; if you are not interested in the per-package server options for the file and you somehow can't find the path of the file, you should also be able to pass a bogus path to setup-file.

[Utensil Song]

The rename of the option is known to break nix workflow, mathport, and now LeanInk, and barely missed doc-gen4. These are not exactly downstream projects developed by users but projects of the "inner-circle" of Lean ecosystem.

[Utensil Song]

It seems that I can't fix LeanInk by a simple replace with setup-file because the extra <imports of the file>.

[Mario Carneiro]

you already have the imports, what is new is the path to the file itself

[Mario Carneiro]

I think the name of the file is available though if you pass it through

[Utensil Song]

Oh

[Utensil Song]

Thanks, I'll try fixing in that way

[Mario Carneiro]

not sure if this is a real file though

[Utensil Song]

I'm also not sure if I should use setup-file in LeanInk as it might still be considered as an "internal command for communication between Lake and the language server". Is there a more idiomatic way?

[Mario Carneiro]

I think the problem is that lake doesn't currently have any non-internal ways to export information like this

[Mario Carneiro]

so the existing projects are making do with what exists

[Mario Carneiro]

@Mac Malone said that he was working on a new "workspace" file which should contain enough path information to replicate this functionality without otherwise calling lake

[Utensil Song]

The output of 'print-paths' has also changed so it took a little longer to make it work. leanprover/LeanInk#55 .

[Utensil Song]

The subtlety is that maybe I should fix the issue without bumping Lean for LeanInk, because it seems that LeanInk can be built in its old toolchain, then use the new toolchain for the target Lean file.

[Utensil Song]

There is no way I can pass the tests for LeanInk. I tried the 2 approaches:

1. bumping Lean for LeanInk, so LeanInk itself and the target Lean program are both on v4.4.0, but tests in LeanInk are outdated by this leap of Lean toolchain, causing many failures that I don't intend to fix in this PR (or should I?). (this is now at my fix-print-path-bump branch)
2. don't bump Lean for LeanInk, so LeanInk itself is on old Lean (on this PR branch), it works fine for a target Lean program on v4.4.0 (locally), but tests in LeanInk are still failing because now the target Lean programs are the tests in LeanInk on the old Lean toolchain which doesn't play with setup-file.

[Utensil Song]

I don't know which approach should I pursue, 1 involves a lot of fixes to LeanInk tests (but potentially worth doing), 2 requires the tests to run on a different toolchain and I don't see how that's possible in the same project.

[Mario Carneiro]

I think 1 is the better long term solution

[Utensil Song]

Thanks, I'll see what I can do with 1.

[Patrick Massot]

I think there is no point investing time in 2 if nobody wants to rescue LeanInk. So 1 is really the only way.

[Utensil Song]

1 is done and CI is green.

[Utensil Song]

I've marked a few places that Lean has changed a bit, nothing serious.

[Utensil Song]

But I'm not sure this PR should be merged or not, as I don't know which projecs are the major users of leanprover/LeanInk as doc-gen4 is using @Henrik Böving 's hargoniX/LeanInk anyway.

[Patrick Massot]

My guess is that nobody uses LeanInk, which is a shame. It should really be rescued.

[Utensil Song]

I guess when the need for something else rises, it could be incorporated into that.