Breakage in lean4+nix workflow

Stream: new members

[Graham Leach-Krouse]

Something seems to have gone wrong recently with my setup for using nix and lean together. I'm wondering if anyone else might be experiencing anything similar, or if anyone can tell whether this is worth a github issue somewhere. Basically, a fresh lean project, created using

nix flake init -t github:leanprover/lean4

throws an error when I open the MyPackage.lean file in nvim (with lean.nvim for LSP):

`/nix/store/z8sin8scrnbkqrm3gxhrx4ywf9gr9bvp-lean-dev/bin/../bin/../bin/lake setup-file /home/graham/Projects/lean-tests/cozy-verif/MyPackage.lean Init` failed:
   This is just a simple Nix adapter for `lake print-paths|serve`.

I'm not sure, but I'm wondering if this might be a regression in leanprover/lean4 - the reason being that the same project (again, straight from the template in leanprover/lean4) works fine with lean.nvim when I use an earlier version of leanprover/lean4 in my flake.lock.

[Sebastian Ullrich]

The experimental Nix setup is being deprecated for interactive use. If there is interest in continuing its development, this should be done in a new repo.

[Graham Leach-Krouse]

Ah, OK. Thanks for the quick reply!

[Sebastian Ullrich]

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/setting.20up.20a.20project.20with.20nix/near/405368794

[Graham Leach-Krouse]

Just in case someone is interested in tracking this down in the future, the first non-working commit seems to be: https://github.com/leanprover/lean4/commit/7ff7cf9b5a7246d584a4b31fad35feb72ce1adf8

[Marc Huisinga]

See also this comment. The API for print-paths (now setup-file) changed and the Nix side wasn't adjusted with it.

[Graham Leach-Krouse]

Apropos: https://github.com/leanprover/lean4/pull/2858#issuecomment-1824045672

I've tried to put together a minimal fix. It gets the interactive nix features working for nvim and for lean's nix-bundled emacs and vscode. Would it be OK if I put in a PR?

[Sebastian Ullrich]

Please see above:
Sebastian Ullrich said:

The experimental Nix setup is being deprecated for interactive use. If there is interest in continuing its development, this should be done in a new repo.

[Graham Leach-Krouse]

Right, apologies, I did see that. The linked issue comment says

If you are using Lean 4 with Nix and stumbled upon this PR because it broke your environment, feel free to submit a PR to adjust the Nix side as well!

So I thought a quick band-aid might be OK, until e.g. a lake wrapper like Joachim Breitner was envisioning appears. But of course, I understand if it's too much hassle (that's why I asked!)

[Sebastian Ullrich]

Yes, the PR comment is older than the one above :) . I think interactive support is relatively independent of a Lake wrapper

[Sebastian Ullrich]

But I would also caution against spending too much time on interactive support. Inevitably there will be Lean/Lake features based on some controlled amount of impurity that Nix will not be able to support as effectively or efficiently so at best it could be useful for building full packages non-interactively for deployment or for providing built dependencies to Lake.

[Graham Leach-Krouse]

Fair enough! Thanks for the warning. :)

Yes, I wasn't really planning on doing too much with it beyond this, just temporarily patching my old workflow.

[Graham Leach-Krouse]

(deleted)