adjust codespace instructions

.vscode/settings.json

@@ -7,33 +7,4 @@
   "files.insertFinalNewline": true,
   "files.trimFinalNewlines": true,
   "files.trimTrailingWhitespace": true,
-  "search.usePCRE2": true,
-  "editor.quickSuggestions": {
-    "comments": "on"
-  },
-  "cSpell.language": "en,en-US",
-  "cSpell.enableFiletypes": [
-    "lean4"
-  ],
-  "cSpell.words": [
-    "monoids",
-    "numref"
-  ],
-  "spellright.language": [
-    "en_US"
-  ],
-  "spellright.documentTypes": [
-    "markdown",
-    "latex",
-    "plaintext",
-    "lean4"
-  ],
-  "spellright.parserByClass": {
-    "lean4": {
-      "parser": "code",
-      "comment_start": "/-",
-      "comment_end": "-/",
-      "comment_line": "--"
-    }
-  }
 }

MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean

@@ -339,10 +339,8 @@ example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
 
   calc
     2 * a * b = 2 * a * b + 0 := by ring
-    _ ≤ 2 * a * b + (a ^ 2 - 2 * a * b + b ^ 2) :=
-      add_le_add (le_refl _) h
+    _ ≤ 2 * a * b + (a ^ 2 - 2 * a * b + b ^ 2) := add_le_add (le_refl _) h
     _ = a ^ 2 + b ^ 2 := by ring
-
 -- QUOTE.
 
 /- TEXT:

user_repo_source/.vscode/settings.json

@@ -6,17 +6,18 @@
         "**/.DS_yml": true,
         "**/.gitpod.yml": true,
         "**/.vscode": true,
-	".docker": true,
-	"build": true,
-	"html": true,
-	"lake-packages": true,
-	".gitignore": true,
-	"lake-manifest.json": true,
-	"lakefile.lean": true,
-	"lean-toolchain": true,
-	"mathematics_in_lean.pdf": true,
-	"MIL.lean": true,
-	"README.md":true,
+        ".devcontainer.json": true,
+        ".docker": true,
+        "build": true,
+        "html": true,
+        "lake-packages": true,
+        ".gitignore": true,
+        "lake-manifest.json": true,
+        "lakefile.lean": true,
+        "lean-toolchain": true,
+        "mathematics_in_lean.pdf": true,
+        "MIL.lean": true,
+        "README.md":true,
     },
     "editor.minimap.enabled": false,
     "editor.acceptSuggestionOnEnter": "off",

user_repo_source/README.md

@@ -52,26 +52,49 @@ followed by `lake exe cache get` inside the `mathematics_in_lean` folder.
 (This assumes that you have not changed the contents of the `MIL` folder,
 which is why we suggested making a copy.)
 
+
 ## To use this repository with Github Codespaces
 
-If you have trouble installing Lean, you can use Lean directly in your browser using Github codespaces.
+If you have trouble installing Lean, you can use Lean directly in your browser using Github
+Codespaces.
 This requires a Github account. If you are signed in to Github, click here:
 
 <a href='https://codespaces.new/leanprover-community/mathematics_in_lean' target="_blank" rel="noreferrer noopener"><img src='https://github.com/codespaces/badge.svg' alt='Open in GitHub Codespaces' style='max-width: 100%;'></a>
 
-* Make sure the Machine type is `4-core`, and then press `Create codespace` (this might take a few minutes).
+Make sure the Machine type is `4-core`, and then press `Create codespace`
+(this might take a few minutes).
+This creates a virtual machine in the cloud,
+and installs Lean and Mathlib.
+
+Opening any `.lean` file in the MIL folder will start Lean,
+though this may also take a little while.
+We suggest making a copy of the `MIL` directory, as described
+in the instructions above for using MIL on your computer.
+You can update the repository by opening a terminal in the browser
+and typing `git pull` followed by `lake exe cache get` as above.
+
+Codespaces offers a certain number of free hours per month. When you are done working,
+press `Ctrl/Cmd+Shift+P` on your keyboard, start typing `stop codespace`, and then
+select `Codespaces: Stop Codespace` from the list of options.
+If you forget, don't worry: the virtual machine will stop itself after a certain
+amount of time of inactivity.
+
+To restart a previous workspace, visit <https://github.com/codespaces>.
+
 
 ## To use this repository with Gitpod
 
-Gitpod is an alternative to Github Codespaces, but is a little less convenient, since it requires you to verify your phone number.
+Gitpod is an alternative to Github Codespaces, but is a little less convenient,
+since it requires you to verify your phone number.
 If you have a Gitpod account or are willing to sign up for one,
-just point your browser to [https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean).
+point your browser to
+[https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean).
 This creates a virtual machine in the cloud,
 and installs Lean and Mathlib.
 It then presents you with a VS Code window, running in a virtual
 copy of the repository.
-We still suggest making a copy of the `MIL` directory, as described
-in step 5 in the last section.
+We suggest making a copy of the `MIL` directory, as described
+in the instructions above for using MIL on your computer.
 You can update the repository by opening a terminal in the browser
 and typing `git pull` followed by `lake exe cache get` as above.
 
@@ -81,7 +104,9 @@ The workspace should also stop automatically
 30 minutes after the last interaction or 3 minutes after closing the tab.
 
 To restart a previous workspace, go to [https://gitpod.io/workspaces/](https://gitpod.io/workspaces/).
-If you change the filter from Active to All, you will see all your recent workspaces. You can pin a workspace to keep it on the list of active ones.
+If you change the filter from Active to All, you will see all your recent workspaces.
+You can pin a workspace to keep it on the list of active ones.
+
 
 ## Contributing