diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md index 8bb4dc9c19..387453b142 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.md +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -25,7 +25,7 @@ Please put an X between the brackets as you perform the following steps: ### Context -[Broader context that the issue occured in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.] +[Broader context that the issue occurred in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.] ### Steps to Reproduce diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8f0c294f0b..5dcf6b05e8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -316,7 +316,7 @@ jobs: git fetch --depth=1 origin ${{ github.sha }} git checkout FETCH_HEAD flake.nix flake.lock if: github.event_name == 'pull_request' - # (needs to be after "Checkout" so files don't get overriden) + # (needs to be after "Checkout" so files don't get overridden) - name: Setup emsdk uses: mymindstorm/setup-emsdk@v12 with: diff --git a/script/lib/update-stage0 b/script/lib/update-stage0 index 10b5878a30..bb2daa3d59 100755 --- a/script/lib/update-stage0 +++ b/script/lib/update-stage0 @@ -17,7 +17,7 @@ for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do done # special handling for Lake files due to its nested directory -# copy the README to ensure the `stage0/src/lake` directory is comitted +# copy the README to ensure the `stage0/src/lake` directory is committed for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/LakeMain.lean src/lake/README.md ':!:src/lakefile.toml'); do if [[ $f == *.lean ]]; then f=${f#src/lake} diff --git a/src/kernel/instantiate_mvars.cpp b/src/kernel/instantiate_mvars.cpp index b834bf2692..3f1adb614a 100644 --- a/src/kernel/instantiate_mvars.cpp +++ b/src/kernel/instantiate_mvars.cpp @@ -34,7 +34,7 @@ option_ref get_lmvar_assignment(metavar_ctx & mctx, name const & mid) { class instantiate_lmvars_fn { metavar_ctx & m_mctx; std::unordered_map m_cache; - std::vector m_saved; // Helper vector to prevent values from being garbagge collected + std::vector m_saved; // Helper vector to prevent values from being garbage collected inline level cache(level const & l, level r, bool shared) { if (shared) { @@ -142,7 +142,7 @@ class instantiate_mvars_fn { instantiate_lmvars_fn m_level_fn; name_set m_already_normalized; // Store metavariables whose assignment has already been normalized. std::unordered_map m_cache; - std::vector m_saved; // Helper vector to prevent values from being garbagge collected + std::vector m_saved; // Helper vector to prevent values from being garbage collected level visit_level(level const & l) { return m_level_fn(l); diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp index f6192f936c..9d74634edc 100644 --- a/src/runtime/process.cpp +++ b/src/runtime/process.cpp @@ -185,7 +185,7 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & // This needs some thought, on Windows we must pass a command string // which is a valid command, that is a fully assembled command to be executed. // - // We must escape the arguments to preseving spacing and other characters, + // We must escape the arguments to preserving spacing and other characters, // we might need to revisit escaping here. for (auto arg : args) { command += " \""; diff --git a/src/util/output_channel.h b/src/util/output_channel.h index 4cf4b7484b..26fc5299ec 100644 --- a/src/util/output_channel.h +++ b/src/util/output_channel.h @@ -18,11 +18,11 @@ namespace lean { std::unique_ptr out; out = new stdout_channel(); - (*out) << "writting to standard output"; + (*out) << "writing to standard output"; out = new stderr_channel(); - (*out) << "writting to standard input"; + (*out) << "writing to standard input"; out = new file_output_channel("file.txt"); - (*out) << "writting to file"; + (*out) << "writing to file"; */ class output_channel { public: