Kim Morrison

when a batch fails, mark the PRs with an orange dot, not a red cross

1

To me, seeing a red X on a PR means that something is broken and I need to fix it. Now that we're using bors on [https://github.com/leanprover-community/mathlib](mathlib), I frequently see...

install instructions on macOS: "cannot find ocamlfind in your path"

9

Following the instructions at https://github.com/HoTT/HoTT/blob/master/INSTALL.md on macOS, when we get to the `etc/install_coq.sh` step in the HoTT directory, it fails with the following output: ``` $ git submodule sync Synchronizing...

I often have multiple files when writing TeX (e.g. a `preamble.tex` that I `\input` into the main file). The subsidiary files aren't meant to be compiled separately, and I usually...

TeX editor indicates a syntax error on $$\text{if $x>0$}$$

1

The TeX editor highlights the innermost `$` signs in `$\text{if $x>0$}$` in red, incorrectly indicating a syntax error. Other variations, such as `$\text{if $x>0$}$` or `\begin{equation*}\text{if $x>0$}\end{equation*}` work fine.

I've recently switched from using Google Docs to the SageMathCloud TeX editor when doing real-time collaborative writing with other mathematicians. It's superb. The one thing I really miss, however, is...

Runing elan-init.sh under msys2 makes elan available via cmd, but not via msys2.

2

The `elan-init.sh` script doesn't work as I would have expected when run inside `msys2`. It installs everything (and sets up the PATH) in the Windows home directory `C:\Users\scott\.elan`, rather than...

chore: port lint-style.py from mathlib

2

Some of these are no longer relevant, but I want to see what works before cleaning up.

neither computable nor noncomputable

3

(Unfortunately I haven't minimised this to the point we can avoid mathlib.) ``` import set_theory.ordinal inductive G : Type 1 | mk : ∀ α : Type, (α → G)...

See zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Apply.20in.20an.20assumption.3F.

`conv {to_rhs, ...}` behaves poorly with `nat.modeq`.

9

Mario helped me write a proof: ``` lemma foo (n k : ℕ) : k ≡ ((k / 2^n) + (k % 2^n)) [MOD 2^n - 1] := -- See...