Raise minimal supported Python version to 3.10

[VojtechStep]

We used to support Python 3.8 because of Ubuntu 20.04, which doesn't have LTS anymore. The successor, Ubuntu 22.04, comes with Python 3.10.
By upgrading we get tooling improvements --- we can update pre-commit-hooks and autopep8, the latter of which was disabled IIRC because the version we could use was buggy --- and we can also use new Python features, such as pattern matching and type aliases.

There's no time pressure, so I'm keeping it as a draft for now, since one nested Python dependency has recently been broken for Python 3.10 in nixpkgs, but I submitted a PR (NixOS/nixpkgs#447787) to fix that, and temporarily replicated the fix here (with the disadvantage of it not being prebuilt, hence waiting for the PR to be merged).
I got rid of the broken dependency by removing a dependency on requests. We were only using it to perform a GET requests and looking at its Link header, which can be done quite easily with Python's built-in urllib.

Note that I updated pre-commit/prettier, but it's not maintained anymore, because pre-commit apparently broke something, and IIUC there's now no officially supported way of running prettier in pre-commit 🤷.

Fixes #939

[VojtechStep]

I hate Python tooling man, why does the double-quote-string-fixer change f-strings in the CI but not on my laptop. It's the exact same Python version and the exact same version of the hook...

[fredrik-bakke]

Yeah, it's fucked :( Maybe it has something to do with locale?

[VojtechStep]

Right now I suspect that the rules are still run with a different Python version than the declared 3.10. Since there's no concept of "target Python version" in the formatter, it just formats it for whatever version of Python is running it. But if that's the case then we need to disable it anyway, because e.g. your local Python would then format it differently than the CI

[VojtechStep]

Alright, turns out my pre-commit was bundling its own Python 3.13, so the behavior in the CI was the correct one. When I convinced pre-commit to use the provided 3.10, it behaved the same as the CI, so that's at least something.
On the other hand, it confirms that running the double-quotation hook with newer Python versions will have different behavior, so I'm disabling it again

[VojtechStep]

I'm marking this as ready for review, since the broken dependency went away when I removed requests

[fredrik-bakke]

Very nice, and thanks for the explanations in the PR body, they answered the questions I was going to ask

[fredrik-bakke]

Is there any time frame for how long Ubuntu 22.4 and Python 3.10 will be supported for? It seems a bit stupid to me that we need to maintain a supported Python version alongside an Ubuntu version. These things should just work, unless we want to update for some bug fix or new feature of course.

[fredrik-bakke]

Oh no, we reached the max heap size again

 Checking category-theory.codensity-monads-on-precategories (/home/runner/work/agda-unimath/agda-unimath/repo/src/category-theory/codensity-monads-on-precategories.lagda.md).
agda: Heap exhausted;
agda: Current maximum heap size is 6442450944 bytes (6144 MB).
agda: Use `+RTS -M<size>' to increase it.
Command exited with non-zero status 251
672.64user 10.67system 11:21.95elapsed 100%CPU (0avgtext+0avgdata 4461348maxresident)k
0inputs+513496outputs (0major+3169569minor)pagefaults 0swaps
make: *** [Makefile:100: check] Error 251

[VojtechStep]

Oh no, we reached the max heap size again

That's pretty bad, the library should not take >6GB to typecheck. The memory usage graphs we have are useless, since I set a big pre-allocated buffer to speed up typechecking. I'll probably need to bisect the library to see if it's some rogue formalization bug, or if the library is inherently this big now.

[fredrik-bakke]

It seems to always happen on category-theory.codensity-monads-on-precategories, I'm profiling it right now. I'll write an issue

[fredrik-bakke]

We can bypass the typecheck and merge this one when it's ready

[VojtechStep]

We can bypass the typecheck and merge this one when it's ready

I don't think that's a good idea; if the resource usage is deterministic, then we'd straight up kill typechecking on master

[fredrik-bakke]

It's not deterministic. This has happened a few times before.

[VojtechStep]

Is there any time frame for how long Ubuntu 22.4 and Python 3.10 will be supported for?

I'm not completely sure what the rest of the comment is asking. Us paying attention to Python versions was instigated by #633 — contributors may run mainstream, point-release distros, such as Ubuntu, which fix a minor Python version that one gets from the official package repository on a particular release. For Ubuntu 20.04 this was Python 3.8, for Ubuntu 22.04 it's Python 3.10.

The approach we take is to consider the oldest supported Ubuntu version, and be compatible with that release's Python version. Here "supported Ubuntu version" doesn't mean supported by us, but by Canonical, i.e. "a version of Ubuntu receiving security updates, so people reasonably expect they can run that version as a main OS". The support period is documented in the Ubuntu release cycle

For how long a particular Python version is supported by Python developers doesn't factor into this, since Ubuntu is supported for longer than its Python version (Ubuntu 22.04 has support until April 2027; Python 3.10 has support until October 2026).

[VojtechStep]

It's not deterministic. This has happened a few times before.

But only recently, on PRs right? That sounds like we're edging the limit anyway, so I'd rather investigate first

[fredrik-bakke]

It's not deterministic. This has happened a few times before.

But only recently, on PRs right? That sounds like we're edging the limit anyway, so I'd rather investigate first

Yes, though the file it fails on is also recent.

[fredrik-bakke]

The checks pass now. Is this one otherwise ready to be merged, @VojtechStep? :)

[VojtechStep]

Yup, all good on my part