## Stream: general

### Topic: off-topic

#### Andrew Ashworth (Feb 26 2018 at 18:52):

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

#### Kevin Buzzard (Feb 26 2018 at 18:52):

Now we're flooding the topic list.

#### Andrew Ashworth (Feb 26 2018 at 18:57):

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

#### Sean Leather (Feb 26 2018 at 18:58):

I'm here. I'm also confused.

#### 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!

#### Sebastian Ullrich (Feb 26 2018 at 19:32):

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

#### Andrew Ashworth (Feb 26 2018 at 20:27):

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

#### Simon Hudon (Feb 26 2018 at 20:28):

how did you create that meta variable?

#### 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

#### Simon Hudon (Feb 26 2018 at 20:36):

What you can try is:

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


refine (my_fun _),


#### Andrew Ashworth (Feb 26 2018 at 20:37):

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

#### Simon Hudon (Feb 26 2018 at 20:38):

suffices works in tactic mode as well

#### Chris Hughes (Feb 26 2018 at 20:46):

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

#### Moses Schönfinkel (Feb 26 2018 at 20:48):

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

wrong topic

#### Patrick Massot (Feb 26 2018 at 20:51):

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

#### 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 :(.

#### Simon Hudon (Feb 26 2018 at 20:52):

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

#### 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

#### Moses Schönfinkel (Feb 26 2018 at 20:53):

That would mean I have to touch the rodent.

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

#### Reid Barton (Feb 26 2018 at 20:54):

You can also press r or Enter to respond

#### Moses Schönfinkel (Feb 26 2018 at 20:55):

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

#### Andrew Ashworth (Feb 26 2018 at 20:55):

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

Great!

#### Reid Barton (Feb 26 2018 at 20:56):

(Or the up and down keys)

#### Moses Schönfinkel (Feb 26 2018 at 20:56):

Nice! Why does j go down o_O?

#### Andrew Ashworth (Feb 26 2018 at 20:56):

j moves the cursor down in vim

#### Reid Barton (Feb 26 2018 at 20:57):

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

#### Moses Schönfinkel (Feb 26 2018 at 20:58):

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

#### Andrew Ashworth (Feb 26 2018 at 20:58):

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

#### 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?

shrug

#### 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

#### 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

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

#### 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