Steven Clontz

warn when using `xi:include` without `xmlns:xi="http://www.w3.org/2001/XInclude"`

2

Just bit me today: an `` is happily ignored without the namespace declaration in *every* file of the project. I think we should warn every project that doesn't declare the...

Use oscarlevin:full by default in codespace

2

Would have prevented https://groups.google.com/g/pretext-support/c/5EhXaz_MHwA/m/iRtDPVbRCAAJ - I don't think the extra minute saved is worth the headache of explaining to users how to get Sage installed in their codespace.

Document Cloudflare/GitHub Pages deploy by action

5

> I'm also interested in adding support for Cloudflare Pages, where every push to a repository could be built and deployed to a preview URL, with merges to main going...

Non-triviality conditions in theorems

1

> @danflapjax @StevenClontz Sorry I did not have the chance to comment. But I don't think this change is an improvement. > I agree it is in general preferable to...

Apologies if this is possible already, but I was unable to figure it out from the hosted preview if so. It would be nice to have points-based racing that prioritizes...

Use relative paths for imports on test server?

1

Thanks for the cool project! I tried to experiment with this library using a GitHub Codespace today. It seems that when I run `pygbag test`, the test server spins up...

Add some traits for S18 Double pointed cocountable topology on R

4

Fixes #1151 by @Moniker1998 Closes #1151

use coherent terminology

3

Inspired by recent discussions in mathlib, e.g. https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2318397.20rename.20RestrictGenTopology.20to.20IsRestrictGen There are several inequivalent notions of "generated" in the literature: generated by maps, generated by subspaces, generated by a subbasis... However, I...