Files opened under */src/lean/ are unmodifiable

[mars0i]

This seemed pretty strange, but I have now figured out the source of the problem.

If I open any file named .lean in neovim in a directory named "lean" under one named "src", and if I try to modify the file, I get nvim error "E21 Cannot make changes, 'modifiable' is off" until I run :set modifiable, regardless of file permissions.

I think this has to do with the nomodifiable configuration option. If I add this line

 \ ft = { nomodifiable = {}, },

within

lua require('vfiler/config').setup{ options = {
...
}

the problem goes away. This line in ft.lua seems to be the cause:

    '.*/src/lean/.*', -- Lean 4 standard library

This problem was a real pain to figure out. I had no idea where to look until I did a lot of testing to find what I could and could not edit files. It wasn't clear that lean.nvim was the culprit.

From my point if view, it's natural to put all of my source in a directory named src, and within that, I classify different kinds of source code by the name of the language. So of course when Is started using Lean, I put my Lean source in src/lean. This seems like a reasonable thing to me.

I understand why it's reasonable to include a test for the standard library to prevent editing it by accident. Would it be possible to add more complicated test to find the standard lib directory instead?

If not, maybe the README could include a warning that certain directory path patterns will cause problems.

(I'd be happy to add a PR for the README if you want. I don't know enough about the standard library to change the path regex test, though.)

Thanks. lean.nvim is great! It's a real pleasure to use. (At first I was working in a directory that wasn't under src/lean.)

[Julian]

Sorry for the trouble.

Would it be possible to add more complicated test to find the standard lib directory instead?

I don't think there is a simple one unfortunately. There's no other reliable way of knowing which directory is the standard library one that we could think of, which seemed still reasonably safe given that in Lean 4 it's discouraged to use src directories within packages. Of course your setup is precisely the one that would be a false positive (and seems otherwise fine certainly) -- but ultimately some false positive seems unavoidable when just looking at paths. And to be explicit -- new users who accidentally modify some core lean file ultimately ended up having huge troubles historically, so it seemed like a good tradeoff even if it has some potential for false positives.

We could make the check more complicated by trying to read files in the directory we suspect is the stdlib (e.g. to look for Lean.lean). But really I think upstream (i.e. Lean itself) gives us no guarantees here so it's a recipe for wasting time if the layout changes there if we get clever.

The README already mentions the nomodifiable setting, is there some other spot you think would have helped? I'm happy to merge a small PR for the README, though given I would suspect the likelihood of anyone else running into this (i.e. anyone using precisely your way of laying out your system) to be quite small, I wouldn't want it to be hugely much more prominent than what we have. But certainly open to ideas, or to rethink things.

Thanks. lean.nvim is great! It's a real pleasure to use. (At first I was working in a directory that wasn't under src/lean.)

Thanks for the kind words, I hope this is the worst issue you run into :D

[mars0i]

Thanks @Julian! I accept that it might be impossible to test reliably for the standard lib directory. I see that in std4 there's a file named "Std.lean", and lakefile.lean contains the line "package std where", but the presence of those could change, or someone could put them in their project for some reason, which would recreate the problem.

I spent at least a couple of hours on this. The error was very mysterious. It was an easy thing to fix once I understood (I renamed src/lean) but I do think it's worth adding a brief remark to the README to allow people to diagnose the problem. One could add something like this:

If the path above your source directory includes any of the sequences "src/lean", "lib/lean/src", "lean_packages", or "_target", you may find that you can't modify your source files, and that nvim gives you the E21 error. This is because lean.nvim tries to prevent users from accidentally shooting themselves in the foot by modifying the Lean standard library, and those directories are part of standard paths for the standard library. The easiest way to fix this is to move your project or rename the directories that are higher up. Another solution is to modify the nomodifiable table entry, preferably after consulting its definition in lean.nvim/lua/lean/ft.lua.

That can be made slightly shorter in various ways. (I know that the way that I described the paths is not precisely accurate, but I was trying to be brief; that's why I used "may find".)

If that seems too long, here's another option:

If you find you can't modify your source files due to the nvim E21 error, this might be due to lean.nvim's effort prevent users from accidentally shooting themselves in the foot by modifying the Lean standard library. See the definition of nomodifiable in lean.nvim/lua/lean/ft.lean.

Or:

If you find you can't modify your source files due to the nvim E21 error, see the definition of nomodifiable in lean.nvim/lua/lean/ft.lean.

The important information is to connect the error to lean.nvim (if you don't know that, it could be anything--filesytem corruption, some weird hidden file attribute, another plugin), and then to information that lets one easily see which paths are affected--at least the relevant lean.nvim source file. Once the user has that information, they can either use the "Configuration and Settings" section of the README to change nomodifiable, or they can modify their file paths.

Again, happy to submit a PR, but I thought I'd float some ideas here first. Thanks!

[Julian]

I see that in std4 there's a file named "Std.lean", and lakefile.lean contains the line "package std where", but the presence of those could change, or someone could put them in their project for some reason, which would recreate the problem.

(That's Std, but here we're talking about Lean (which the comment is confusing about but Std didn't even exist back then). These days it would be called "core Lean". Specifically it's these files)

The second option there seems more or less fine with me though to add if you care for a PR (perhaps with referencing "the nomodifiable configuration option" rather than sending users to look at "lua/lean/ft.lua"?)

[mars0i]

Ah, I see. Yes, it would be very bad to mess with the Lean source!

If ft.lua isn't mentioned, or its contents isn't summarized, how will a user know what aspect of their path is causing the problem? One can fix the problem by zeroing out nomodifiable, but that's not a good solution.

[mars0i]

Oh, I get it. One can display the contents of nomodifiable, without looking at ft.lua. OK.

[mars0i]

Except that I have no idea how to display the contents of nomodifiable. This is an entry in a local variable, options, set in ft.lua. Passing ft.nomodifiable to setup in init.lua causes it to be passed to enable in ft.lua, and which then overrides the value of nomodifiable in the local table options. afaict, without looking at ft.lua there is no way to know what one is overriding.

Maybe there is a way to print the contents of chunk-local variables in Lua. I'm not a Lua expert, and I don't know what that is. In most languages, the only way to display the contents of a local variable is by instrumenting the source code with print statements, or by using a debugger. I did do some investigation of this question, but without serious study of Lua (something I should do sometime, but not now), this is the sort of information that doesn't come up readily in response to search strings.

I understand that you don't want to walk a user of lean.nvim through basic Lua or plugin information, but I feel that there should be enough documentation that it shouldn't be necessary to grep through the source tree and then examine source files to find out details of something that could cause lean.nvim to make it impossible to edit one's own source files.

So my feeling is if the README doesn't list the default contents of nomodifiable, it should point users to ft.lua. (Theoretically, I'd rather see this the contents of nomodifiable listed in the README, but then that has to be kept in sync with the source code, so maybe it's better to point people to ft.lua.) Or if there is an easy way to print the local variable without looking at ft.lua, then the README could include a pointer to that technique. Or maybe add a function somewhere that would cause the contents of options.nomodifiable to be printed out? Or make nomodifiable global, but that's probably undesirable.

(Sorry to use up so much of your time on this. I do appreciate it. And I do feel bad about using up your time on this. lean.nvim is one of the things that makes learning Lean such a pleasure. I'm very happy to be able to remain in my vim/nvim "home", and not have to keep running into walls using vim emulation in VSCode or Emacs.)

[Julian]

One can fix the problem by zeroing out nomodifiable, but that's not a good solution.

Can you elaborate on why this isn't a good solution?

More generally in your specific case, the issue sounded like you didn't know what it was that was causing the behavior you were observing. That's the problem I'm interested in fixing -- making sure it's mentioned in a way you think you'd have seen.

Once someone knows what functionality exists that is relevant to what they see, it's true they then may need to know how it's currently configured. I'm pretty sure someone who gets this far will be able to figure out where to look. Including extra detail though just makes more work (for me, if I ever change the package layout, or the value of the setting) and for every other person reading the README who isn't in this scenario but who might be confused by something they don't need to know.

(And thanks for the kind words of course! No worries here, we may as well get it right so long as we're discussing it).

[mars0i]

Thanks @Julian. I understand. I'll submit the PR without the extra information.

One can fix the problem by zeroing out nomodifiable, but that's not a good solution.

Can you elaborate on why this isn't a good solution?

I was thinking that though emptying nomodifiable was an easy solution, it defeats the purpose of preventing someone from modifying Lean without knowing what they're doing. A smaller change to nomodifiable could allow the user to edit their source while still preventing them from editing some installations of the Lean source. But as you say, someone can figure that out if they know they need to investigate.

[Julian]

Will call this closed after your PR I think but any further feedback always welcome!