chore: add setting to prevent accidental editing of dependencies (lea…

…nprover-community#10320)

Adds `**/.lake/**` and `**/.elan/**` to a readonly include list in the VSCode workspace settings. This should prevent users from accidentally editing files in dependencies they might navigate to in VSCode.

.vscode/settings.json

@@ -10,5 +10,9 @@
   "githubPullRequests.ignoredPullRequestBranches": [
     "master"
   ],
-  "git.ignoreLimitWarning": true
+  "git.ignoreLimitWarning": true,
+  "files.readonlyInclude": {
+    "**/.elan/**": true,
+    "**/.lake/**": true
+  }
 }