If for some reason you're interested in seeing what's being upgraded: github.com/ralsei/types.pl/iss
— ionchy

Show thread

On Saturday, 26 November 2022, at approximately 13:00 EST (18:00 UTC) we'll be doing a minor upgrade of types.pl's Glitchsoc fork from v3.5.3 to v3.5.5. This is a relatively small upgrade, mostly for security patches, so in the ideal scenario where everything goes perfectly there shouldn't be any significant downtime. (If things don't go smoothly you'll be able to tell.)

For now, we're holding off of on upgrading to v4 since it introduces a lot of undesirable features, but mostly because we don't currently have the time to properly test and tweak this bigger upgrade, especially during this ongoing influx of users

— ionchy

official types.pl admin announcement:

i'm gay

Sorry for the downtime everyone. Everything should be functioning properly now, with no changes from before. All your toots are where you left them.
— ionchy

putting this off by a week to November 19th, because I am literally just too busy -hazel

Show thread

Also, if your application is denied, *you can apply again with more information*.

Having an easily searchable username, an old Twitter profile, or a personal site are all very useful so we can figure out who you are and why you want to join.

Show thread

Welcome, new users! Some frequently asked questions:

1. Why are mastodon.social, mas.to, etc silenced?

Due to the size of these instances, as well as the fact that registrations on them are completely open, content moderation becomes very difficult. Mastodon doesn't give us very many tools for talking to an instance when we only want to let some users in without moderating those instances by telephone line.

You can still follow and interact with users on these instances, but when they follow you, you'll get a follow request. This is the only major difference.

2. Why is instance X suspended entirely?

The upside of Mastodon is that anyone can make an instance, and the downside of Mastodon is that anyone can make an instance. There are tons of Mastodon instances for any topic you'd like, but there are also tons of instances for topics you wouldn't like (including, up to, and beyond literal neo-Nazism). Part of our job as an instance administrator is to avoid these instances interacting with us so you don't get awful content in your notifications, or on the federated timeline.

If you want to look at the list of all suspended instances, take a look at types.pl/about/more (it's long!)
Many of these instances don't have immediate reasons for defederation on them, because they were imported from the hellsite.site blocklist back in 2020 when this instance was first created.

3. Will you unsuspend X instance?

Not likely. If you want a larger corner of the fediverse without our (admittedly opinionated, but generally correct) moderation choices, you're free to join another instance.

4. Why is my application pending indefinitely?

There could be two reasons for this.
The first is that your application was bad: "leaving twitter", "why not?", "waiting until musk suspends me" aren't good reasons, and don't verify that you're not a spambot.
We also want to ensure that new users on types.pl meet our code of conduct, which some people in the PL community decidedly do not: no homophobia, no transphobia, et cetera.

The second is that we're slow at accepting account requests. We're getting about 25-75 applications a day, and we can only reasonably process about 15-25. This is because this instance is run by a bunch of busy students.

5. Can I get a custom emoji added to the instance?

Yes. DM an admin with a shortcode and a PNG.

6. Wow, this is very useful! Thanks so much!

me: You're welcome! That's not a question.

gigantic spider above me: dematerializes

we're going down for an indefinite amount of time (hopefully short!) starting at 1PM EST this Saturday, November 12th

the version of Mastodon on this server is 1500 commits behind upstream so I should probably merge it soon

[THIS IS AN OFFICIAL ADMIN ANNOUNCEMENT OF UTMOST IMPORTANCE]

[THIS IS AN OFFICIAL ADMIN ANNOUNCEMENT]

i went to the store and got some fruit juice. it was pretty good. thanks

Show thread

[THIS IS AN OFFICIAL ADMIN ANNOUNCEMENT]

hi

We are silencing mastodon.social and mastodon.online. All future follows from these instances will take manual approval.

We have enough mutuals on these instances to make defederating difficult. However, time and time again, these two instances comprise the overwhelming majority of moderation work done here. Moderation is at best sparse on these instances -- we have had repeated issues with spambots and unsavory users, with reports going largely unnoticed.

We are concerned about these instances becoming a gateway to harassment or spam, due to open registration and lack of proper moderation. This is beyond the actions of any singular user -- it's more of a lot of small offenses that have accumulated over time, and that make moderation work much more difficult.

If you are on these instances, it may be worthwhile to look at migrating.

  • hazel

In plaintext posts, all regular LaTeX syntax should work fine.

Show thread

We changed the LaTeX syntax a bit.

First off:

  • The \$ \$ syntax now works.
  • In Markdown posts, use `\$ content \$` for inlinemath.
  • Also in Markdown posts, use:```latexcontent ...```for displaymath. You have to include the normal displaymath delimiters here -- the latex mode is just an "escape" environment that gives you verbatim content.

example 

$$ \mathsf{funext} : \left( \prod_{x : A} \left( f(x) = g(x) \right) \right) \to (f = g). $$

Show thread

We now support LaTeX.

A couple notes:
- Markdown formatting is slightly broken right now. We're working on it.
- You should always add content warnings when using LaTeX, due to the fact that it's almost inherently screen-reader hostile.
- $ $ for inlinemath doesn't work. Use the other syntax.

we changed "post" back to "toot" -- it got changed in 3.4, for some reason

- hazel

types.pl is going down for scheduled maintenance on Tuesday, June 1, at 1 PM EDT, to likely 2 PM at worst.

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.