Zulip Chat Archive

Stream: general

Topic: off-topic


view this post on Zulip Andrew Ashworth (Feb 26 2018 at 18:52):

or you could have an off-topic topic, very meta

view this post on Zulip Kevin Buzzard (Feb 26 2018 at 18:52):

Now we're flooding the topic list.

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 18:57):

up and down is j and k, feels very vi-like

view this post on Zulip Sean Leather (Feb 26 2018 at 18:58):

I'm here. I'm also confused.

view this post on Zulip Sean Leather (Feb 26 2018 at 18:59):

I'm here. I'm also confused. Doubly confused. Because I didn't know my message was at the bottom!

view this post on Zulip Sebastian Ullrich (Feb 26 2018 at 19:32):

That's okay, the topic list seems to be a most-recently-used cache

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 20:27):

is there a way to give a friendly name to a metavariable while inside a proof?

view this post on Zulip Simon Hudon (Feb 26 2018 at 20:28):

how did you create that meta variable?

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 20:31):

i haven't yet, I'm still in term mode, haha. in tactic mode it'd be from using apply, refine, and friends

view this post on Zulip Simon Hudon (Feb 26 2018 at 20:36):

What you can try is:

let my_mvar, tactic.swap,
refine (my_fun my_mvar),

instead of

refine (my_fun _),

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 20:37):

that looks like what i'd do in term mode with suffices, nice

view this post on Zulip Simon Hudon (Feb 26 2018 at 20:38):

suffices works in tactic mode as well

view this post on Zulip Chris Hughes (Feb 26 2018 at 20:46):

How do I view the automatically generated name of an instance?

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:48):

You could #print instances and check that way, I guess?

view this post on Zulip Simon Hudon (Feb 26 2018 at 20:50):

wrong topic

view this post on Zulip Patrick Massot (Feb 26 2018 at 20:51):

That's the real test: will the stream and topic stuff be useful or irritating?

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:51):

I don't think I have the mental fortitude to carefully tag every message I type :(.

view this post on Zulip Simon Hudon (Feb 26 2018 at 20:52):

I think it would be great if you suggest a different topic for a given post

view this post on Zulip Simon Hudon (Feb 26 2018 at 20:53):

I don't think I have the mental fortitude to carefully tag every message I type :(.

If you click on the message you want to respond to, you're going to respond in the right topic

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:53):

That would mean I have to touch the rodent.

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:54):

I sit on a fitball and my furry friend is a little bit too far usually.

view this post on Zulip Reid Barton (Feb 26 2018 at 20:54):

You can also press r or Enter to respond

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:55):

Can r read my mind as to which message I am replying to?

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 20:55):

you can use j and k to move up and down, ? displays keyboard shortcuts

view this post on Zulip Simon Hudon (Feb 26 2018 at 20:55):

Great!

view this post on Zulip Reid Barton (Feb 26 2018 at 20:56):

(Or the up and down keys)

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:56):

Nice! Why does j go down o_O?

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 20:56):

j moves the cursor down in vim

view this post on Zulip Reid Barton (Feb 26 2018 at 20:57):

http://www.catonmat.net/blog/why-vim-uses-hjkl-as-arrow-keys/

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:58):

It's a little bit fiddle-ey I have to say.

view this post on Zulip Patrick Massot (Feb 26 2018 at 20:58):

help you keep your fingers on the home row

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 20:58):

i always end up installing nano whenever i have to work on the terminal

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:59):

I mean the whole reply-to thing with selecting what exactly it is I am replying to. Might be a bit more work than I would like, perhaps?

view this post on Zulip Moses Schönfinkel (Feb 26 2018 at 20:59):

shrug

view this post on Zulip Andrew Ashworth (Feb 26 2018 at 20:59):

probably just fine to post whatever into general, if something deserves more in depth discussion, someone can always quote and reply to break it off into its own topic

view this post on Zulip Simon Hudon (Feb 26 2018 at 21:08):

for starting conversations, that's good but in the middle of a conversation, commenting on the wrong topic means that some people will see it and others will not

view this post on Zulip Reid Barton (Feb 26 2018 at 21:17):

Everyone sees messages to all topics on the streams they're subscribed to (unless they've explicitly muted a particular topic, which isn't the common case).
An analogy that might be helpful is that streams are like mailing lists while topics are like the subjects of threads on a particular list. Streams are relatively static and stream membership determines what you receive. Topics are ephemeral and clarify the context of a message. If there is a conversation about affine schemes and another conversation about mathlib failing to build, then you can reply to one of the conversations with "it didn't work" and it won't be misunderstood as relating to the other conversation.
You can also choose to view one topic at a time or all topics on a stream (or on all streams) mixed together, but the expectation is that you'll eventually see all messages on a stream regardless of their topics.

view this post on Zulip Reid Barton (Feb 26 2018 at 21:20):

For now, there's little enough traffic (here and on the gitter) that it probably doesn't make sense to create additional streams, but if, say, the stacks project grows to the point where not all lean users want to see all the discussion about the project, that's when having a separate stream would be useful.


Last updated: May 16 2021 at 05:21 UTC