off-topic

Stream: general

[Andrew Ashworth]

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

[Kevin Buzzard]

Now we're flooding the topic list.

[Andrew Ashworth]

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

[Sean Leather]

I'm here. I'm also confused.

[Sean Leather]

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

[Sebastian Ullrich]

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

[Andrew Ashworth]

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

[Simon Hudon]

how did you create that meta variable?

[Andrew Ashworth]

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]

What you can try is:

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

instead of

refine (my_fun _),

[Andrew Ashworth]

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

[Simon Hudon]

suffices works in tactic mode as well

[Chris Hughes]

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

[Moses Schönfinkel]

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

[Simon Hudon]

wrong topic

[Patrick Massot]

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

[Moses Schönfinkel]

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

[Simon Hudon]

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

[Simon Hudon]

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]

That would mean I have to touch the rodent.

[Moses Schönfinkel]

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

[Reid Barton]

You can also press r or Enter to respond

[Moses Schönfinkel]

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

[Andrew Ashworth]

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

[Simon Hudon]

Great!

[Reid Barton]

(Or the up and down keys)

[Moses Schönfinkel]

Nice! Why does j go down o_O?

[Andrew Ashworth]

j moves the cursor down in vim

[Reid Barton]

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

[Moses Schönfinkel]

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

[Patrick Massot]

help you keep your fingers on the home row

[Andrew Ashworth]

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

[Moses Schönfinkel]

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?

[Moses Schönfinkel]

shrug

[Andrew Ashworth]

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]

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]

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]

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.