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:

#meta-tt meta-subjects, i.e., non-mathematical but related to the administrative parts of the course
#cafe any off-topic subject
#test use this to test posting on Zulip
#intro-lang-proofs about low-level language(s) for proofs
#rec-ind recursion and induction
#ints theory of integers
#reals theory of reals
#set-fun-rel sets, functions, relations
#set-theory (axiomatic) set theory
#algebra algebra
#cats category theory
#order-theory order theory
#proofassistants about Lean, Agda, and other proof assistants
#programming about programming
#misc miscellaneous about the (mathematical) content of this course that do not fit anywhere else
#english about english
#portuguese about portuguese
#greek about greek
#fmcbook errors, updates, suggestions regarding fmcbook
#tex about TeX, LaTeX, ConTeXt, Overleaf, ...
#zulip about (the use of) Zulip
#tech about other tools, programs, apps, editors, operating systems, etc.

Exemples:

  1. On p.302 of fmcbook near the end of the page shouldn’t ⊆ be a ⊊? → #fmcbook
  2. Will there be a class tomorrow? → #meta-tt
  3. Is ⟨some subject⟩ something that can be on the final exams of this? → Don’t ask this. Nowhere. Never.
  4. How do you type unicode characters? → #tech
  5. Dá para usar Agda em vez e Coq para formalizar o teorema Θ4.12?
    Depende: se a dúvida é sobre as capacidades das duas linguagens, poste no #proofassistants; se a dúvida é sobre se eu, Thanos, vou aceitar nesta disciplina entregar tal trabalho em Agda em vez de Coq, poste no #meta-fmc1.
  6. Any interesting courses besides this one for this semester? → #cafe
  7. Any good souvlaki recommendations? → #cafe

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. Don’t use Zulip’s «mark as resolved» function.
  4. Don’t post screenshots of your code. Post your actual code using block quotes (preferably indicating the language used).
  5. Avoid the use of Zulip’s “pseudo-LaTeX” functionality. Embrace unicode text when possible.

How to post…

…formatted text?

There is markdown in Zulip, but avoid headers and big stuff like that.

…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.