Emigrating from Brazil

[andrejbauer]

It seems there's too much controversy with calling it "Brazil". What would be a better name? I am thinking nothing is wrong with tt. Martin Escardo suggested Andromeda, which seems far enough (although we're on a collision course with it).

[jonsterling]

I like Andromeda! TT is a good name for the things from your original tutorials, but since the type theory being played with here is far from a "basic" one, it might be good for that to be reflected in its name.

[pthariensflame]

:+1: for Andromeda!

[andrejbauer]

It can be Andromeda (especially since Martin meant it as a joke). Let's see, how does this sound: "What would Andromedans do?"

[andrejbauer]

Andromeda |anˈdrɒmɪdə|

1. Greek Mythology an Ethiopian princess whose mother Cassiopeia boasted that she herself (or, in some stories, her daughter) was more beautiful than the Nereids. In revenge Poseidon sent a sea monster to ravage the country; to placate him Andromeda was fastened to a rock and exposed to the monster, from which she was rescued by Perseus.
2. Astronomy a large northern constellation between Perseus and Pegasus, with few bright stars. It is chiefly notable for the Andromeda Galaxy (or Great Nebula of Andromeda), a conspicuous spiral galaxy probably twice as massive as our own and located two million light years away.

[martinescardo]

I like Andromeda. Type "andro file.andro" in the command line.

[andrejbauer]

I can argue that Brazil was too close for some Brazilians.

[martinescardo]

Closer than anything else.

[andrejbauer]

Maybe I should wait until the World Cup is over, lest more Brazilians be offended.

[martinescardo]

You mean "not offended".

[andrejbauer]

I don't think so:

lest |lɛst| conjunction with the intention of preventing (something undesirable); to avoid the risk of: he spent whole days in his room, wearing headphones lest he disturb anyone.

[martinescardo]

I mean that I was not offeded, just a little bit irritated by the discussions about your Brazil.

[christopherastone]

Andromeda would be fine, though I'd prefer a shorter extension than .andro. Maybe .and ?

[pthariensflame]

.adr is what I would go for, but it doesn't really matter much.

[andrejbauer]

If we're going down this road, the extension should be .m31. It'll make a nice FAQ.

[martinescardo]

I like m31.

[pthariensflame]

I also like .m31. :D

[jonsterling]

Heh, that's awesome. :thumbsup: on .m31.

[Heimdell]

The .m31 is just awesome.

[andrejbauer]

The question is: should we keep everything in the tt repo, rename tt to andromeda, or create a copy of tt called andromeda?

[christopherastone]

I assumed we'd just rename the brazil sub-component(s) to andromeda, and keeping tt as tt. Otherwise, how do we distinguish the higher-level and lower-level systems/languages?

[pthariensflame]

@christopherastone I'm fine with that, although where do we draw the dividing line?

[andrejbauer]

I always assumed the two would eventually converge. Ooo, ooo, milkyway and andromeda.

[pthariensflame]

@andrejbauer YES!

[martinescardo]

I am not sure what the question is.

But I would support a "historical" approach that keeps visible how things evolved. So I support to create a new copy.

But I leave it up to you to decide, of course.

Greetings from far away, Martin

On 11/07/14 19:05, Andrej Bauer wrote:

The question is: should we keep everything in the |tt| repo, rename |tt| to |andromeda|, or create a copy of |tt| called |andromeda|?

— Reply to this email directly or view it on GitHub https://github.com/andrejbauer/tt/issues/42#issuecomment-48763274.

Martin Escardo http://www.cs.bham.ac.uk/~mhe

[JasonGross]

The point of git is to keep visible how things evolved; if you want to see, you just look in the repository history. Would making a copy add anything to this? (You can always make a tag, or a branch, that you keep around indefinitely, like https://github.com/coq/coq/tree/v8.1.)

[andrejbauer]

Let me explain the option that I like best. If we rename the tt repository to andromeda then:

1. All history, including followers, stars, issues, etc., will be kept
2. Traffic pointing to tt will be automagically redirected to andromeda

The only drawback I can see is that I won't be able to create another repository called tt (I could but that would kill the automatic redirection). If we make a copy we get two copies (duh), but then they evolve separately. Also, people who land in tt will not easily figure out that there is also andromeda. So unless there's a reason not to, I will rename soonish.

[martinescardo]

Rename sounds the option to choose.

On 12/07/14 08:31, Andrej Bauer wrote:

Let me explain the option that I like best. If we rename the |tt| repository to |andromeda| then:

1. All history, including followers, stars, issues, etc., will be kept
2. Traffic pointing to |tt| will be automagically redirected to |andromeda|

The only drawback I can see is that I won't be able to create another repository called |tt| (I could but that would kill the automatic redirection). If we make a copy we get two copies (duh), but then they evolve separately. Also, people who land in |tt| will not easily figure out that there is also |andromeda|. So unless there's a reason not to, I will rename soonish.

— Reply to this email directly or view it on GitHub https://github.com/andrejbauer/tt/issues/42#issuecomment-48804880.

Martin Escardo http://www.cs.bham.ac.uk/~mhe

[andrejbauer]

I have renamed the repository to andromeda. It still remains to rename brazil in the source code, but I am closing the issue now.