Zulip

What is this?

Zulip is the platform we will use to communicate about any subject (meta or otherwise) related to this course.

Note that there are plenty of zulips being used by various communities; the relevant one for this course is fmcthanos.zulipchat.com.

How does it work?

If you have never used Zulip before, first see [the tour] and also the Why Zulip? which appears at the end of the tour.

How do I enter/use it?

Send me an email, and I will send you an invitation. That is all. Once you are in, please fill-in your profile and use an actual photo of yours.

In which channels should I subscribe to?

You will be automatically subscribed to the relevant channels for this course.

In which channel should I post?

Each post is associated to a topic, and each topic lies within a channel.

The relevant channels, are:

Exemples:

1. Will there be a class tomorrow? → #meta-tt
2. Is ⟨some subject⟩ something that can be on the final exams of this? → Don’t ask this. Nowhere. Never.
3. How do you type unicode characters? → #tech
4. Can we use Agda instead of Lean to formalize Theorem Θ4.12?
   It depends: if the question is about the capabilities of the two languages, post it on #proofassistants; if the question is whether I, Thanos, will accept a solution written in one language and not the other, post it on #meta-tt.
5. Any interesting courses besides this one for this semester? → #cafe
6. Any good souvlaki recommendations? → #cafe
7. On the homework section the last two homeworks (hw4 and hw5) have the same date. → #website
8. The blackboards PDF link on the site is broken. → #website
9. On p.302 of fmcbook near the end of the page shouldn’t ⊆ be a ⊊? → #fmcbook

Create a new topic for your message, unless you want to contribute to an existing conversation.

If you are not sure on which channel to post, just post anywhere. I will move your message to the appropriate channel later of if you post on the wrong place.

How not to post

1. In the vast majority of cases do not direct your message/question to me. Just ask: «I did not understand how…». The idea is to start an open discussion (𝑛-alogue), not a public dialogue.
2. In the vast majority of cases do not use the «quote and reply» function of Zulip. This is something that makes more sense in other models of communication (email, discord, slack, etc.) but in Zulip it ends up being clumbersome. Just respond what you want to say, and the context should be enough for everyone to follow allong. If it isn’t, a short quotation with > that minimally mentions the context is OK.
3. Do not use Zulip’s «mark as resolved» function.
4. Do not post screenshots of your code. Post your actual code using block quotes (preferably indicating the language used).
5. Avoid posting images of text that you wrote. Type your text instead, if possible.
6. Avoid the use of Zulip’s “pseudo-LaTeX” functionality. Embrace unicode text when possible, resort to Zulip’s pseudo-LaTeX when needed.

How to post…

…text?

There is markdown in Zulip, but avoid headers and big stuff like that. You are most likely writing a message, not a book or an article.

…math?

Zulip understands some (La)TeX but, surprise: most of the times it is better to simply use unicode text.

For inline math: se usar TeX para mencionar, por exemplo, variável x o modo TeX já vai destacá-la numa maneira legal no meio do texto normal; mas uma outra maneira legal para destacá-la seria usar os backticks para escrevé-la como se fosse um codigozinho (como eu acabei de fazer aqui que falei «variável x …» em vez de «variável x …».

For display math: If you want to use TeX you write the code block using math as the chosen language of the block. If you want to use text (with Unicode) just write in a code block without a language (or choose some that ends up highlighting nicely your text). (See also the next question.)

…proofs?

Try to write your proofs using code blocks (with ```) in stead of writing in normal text. This way it is easier to separate the object-language that we are discussing (like a language in which we write proofs in), from the metalanguage (greek or english or whatever) that we are using to speak about it. More over, this is reinforces the idea of «lines of code» about proofs.

…computations?

Instead of writing like this:

bla bla bla bla = blu blu  [foo.2]
                = blu bli  [bar.2]
                = meh boo  [meh.1]

which is a PITA to align correctly if you are typing in a browser and wastes too much space in general, write either like this:

bla bla bla bla
  = blu blu  [foo.2]
  = blu bli  [bar.2]
  = meh boo  [meh.1]

or like this:

  bla bla bla bla
=   [foo.2]
  blu blu
=   [bar.2]
  blu bli
=   [meh.1]
  meh boo

All three of these forms are nice and valid on paper; but the first one is tiresome to read as well as to write on Zulip.