Also prevent accidental modification of project dependencies.

Matches the current Mathlib setting (which is done via
`vscode/settings.json` -- maybe at some point we'll attempt to parse
this).

See e.g. https://leanprover.zulipchat.com/#narrow/channel/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/.E2.9C.94.20Local.20build.20issue/near/481118068

.luacheckrc

@@ -12,6 +12,8 @@ globals = {
     fields = {
       "contents",
       "message",
+      "is_falsy",
+      "is_truthy",
     }
   },
 }

lua/lean/config.lua

@@ -52,6 +52,8 @@ local DEFAULTS = {
   ft = {
     nomodifiable = {
       '.*/src/lean/.*', -- Lean core library
+      '.*/.elan/.*', -- elan toolchains
+      '.*/.lake/.*', -- project dependencies
     },
 
     ---Check whether a given path should be modifiable.

spec/fixtures.lua

@@ -16,9 +16,17 @@ local fixtures = {
     some_nonexisting_file = child 'DoesNotExist.lean',
     some_nested_existing_file = child 'Test/Squares.lean',
     some_nested_nonexisting_file = child 'Test/DoesNotExist.lean',
+
+    some_dependency_file = child '.lake/packages/importGraph/ImportGraph/Imports.lean',
   },
 }
 
+assert.is_truthy(vim.uv.fs_stat(fixtures.project.some_existing_file))
+assert.is_falsy(vim.uv.fs_stat(fixtures.project.some_nonexisting_file))
+assert.is_truthy(vim.uv.fs_stat(fixtures.project.some_nested_existing_file))
+assert.is_falsy(vim.uv.fs_stat(fixtures.project.some_nested_nonexisting_file))
+assert.is_truthy(vim.uv.fs_stat(fixtures.project.some_dependency_file))
+
 function fixtures.project:files()
   return vim.iter {
     ['existing'] = self.some_existing_file,

spec/ft_spec.lua

@@ -35,8 +35,13 @@ describe('ft.detect', function()
     assert.is_falsy(vim.bo.modifiable)
   end)
 
+  it('marks dependency files nomodifable by default', function()
+    vim.cmd.edit { project.some_dependency_file, bang = true }
+    assert.is_falsy(vim.bo.modifiable)
+  end)
+
   it('does not mark other lean files nomodifiable', function()
-    vim.cmd('edit! ' .. project.some_existing_file)
+    vim.cmd.edit { project.some_existing_file, bang = true }
     assert.is_truthy(vim.bo.modifiable)
   end)
 end)