Kim Morrison
Kim Morrison
I'd be very interested in this too. I'd like to switch over to Joda Time soon, but having to translate to and from Dates to talk to Circumflex is slowing...
This has been fixed in the latest nightly, available from https://github.com/leanprover/lean-nightly/releases. If you tell your students to install Lean by using elan (e.g. see instructions at https://github.com/leanprover/mathlib/blob/master/docs/elan.md), and give them...
What would this do that `sorry` doesn't already achieve?
Lean 3 is essentially frozen while the developers work on Lean 4, so without any easy-to-reproduce test case it's unlikely that you'll get much help. I would suggest trying to...
It's early days yet --- I'd just break the existing URLs rather than have to carry along a hack forever.
> I didn't have time to look into this in detail (and patience, as VS Code takes ages to check the file) but apparently there has been a recent refactoring...
@manzyuk, it needs to finish CI first (so that the `awaiting-CI` label gets removed) before you can ask bors to merge.
Perhaps syntax highlighting is done by an external library --- if that's the case and someone tells me which it is, I'm happy to carry the issue upstream.
(Our mathlib3 [instructions for windows](https://leanprover-community.github.io/install/windows.html) currently advise against using `msys2`, and instead using `git bash`, so presumably this hasn't been affecting people.)