tactic mode automatic names

Stream: new members

[jachym simon]

Hi! I opened my old project in a newly installed lean and found out, that the automaticly generated names in tactic mode are super weird-looking -> ᾰ , ᾰ _1 etc. (instead of a, a_1 which were generated before). I dont even know, how to actually write such characters and it also unfortunately messes up my (quite a long) code. Is there some way how to change that? Thanks, Jachym

[Johan Commelin]

@jachym simon hmm, this is somewhat intentional... but I'm sorry that it breaks your code.

[Johan Commelin]

You might want to use the previous version of Lean to avoid this issue.

[Johan Commelin]

This change was introduced in the latest version. The reason is that for a big library like mathlib, relying on auto-generated names is not a good idea. So to discourage this from happening, we chose a hard-to-type unicode character instead.

[Johan Commelin]

How many lines of code is your project?

[Mario Carneiro]

Probably an easy fix is to replace a and a_* with ᾰ and ᾰ_* respectively

[Mario Carneiro]

You can do that with a regex find/replace in a big project (make sure the search for a is a whole word search). But watch out for comments that say e.g. -- A group is ᾰ monoid with inverses afterwards

[Mario Carneiro]

Should we add this character to #translations? I'm torn

[jachym simon]

Ok, i see. It is around 500 lines that are affected (seems like something around 70 places to change). Ill try to rename them (thanks, somehow i didnt consider that), or go to the previous version of lean. Thank you for your replies!

[Mario Carneiro]

the recommended solution is of course to not refer to autogenerated names in the first place

[Mario Carneiro]

but find/replace is an easy way to get the project compiling again

[Reid Barton]

Mario Carneiro said:

the recommended solution is of course to not refer to autogenerated names in the first place

And one way to migrate an old project to this is to introduce the old names explicitly so that they're no longer autogenerated. For example, change cases h to cases h with h_a h_a_1 or whatever.

[jachym simon]

Yes, thank you. Im planning on rewriting it eventually to avoid the autogenerated names, but for now i just want it to run.

[Johan Commelin]

@jachym simon In that case I suggest downgrading to the version of lean from 3(?) weeks ago

[Johan Commelin]

That will cause you the least amount of headaches

[Kevin Buzzard]

but it would also be the most amount of work, if Jachym was going to rewrite it eventually anyway :-)