Sanitize Lean file name

Stream: Is there code for X?

[Jakob von Raumer]

Is there a canonical function that turns a String into a string suitable as a Lean file name stem, e.g. returns foo123 for foo(123=!)?

[Damiano Testa]

What should it do with A.B? Drop .B? You could also use «most characters work here»!

[Jakob von Raumer]

For other identifiers, I'd be happy with «...», but I'm a bit hesitant to have them in file names. Not sure about ., maybe convert to a _ or something?

[Eric Wieser]

The «...» isn't legal in a filename

[Eric Wieser]

import «foo (123-!)» is the syntax for importing foo (123-!).lean

[Eric Wieser]

So this isn't necessarily a question about legal lean filenames, but about legal operating system filenames

[Jakob von Raumer]

I thought the Lake source must have something, but I've not found anything.

[Eric Wieser]

If it did have that code, it would only be for lake new

[Damiano Testa]

Ah, you are asking about file names, not docs#Lean.Name.

[Damiano Testa]

Why not simply keeping all alphanumeric characters?

[Eric Wieser]

Why not simply keep all characters?

[Damiano Testa]

I think that / is not a valid file name (at least on my Linux computer).

[Jakob von Raumer]

Yes, I'd at least want to strip non-ASCII, \, and /, was just wondering if there was already a canonical solution to this

[Eric Wieser]

I guess the question is whether it's better to report the error back to the user and have them choose a better name

[Jakob von Raumer]

This is for a transpiler kind of scenario

[Eric Wieser]

I think there's no canonical solution for this because this is an OS-level or stylistic decision, not a Lean one; Lean will allow you to call modules whatever you like

[Eric Wieser]

Jakob von Raumer said:

This is for a transpiler kind of scenario

So you already have a filename from a different language?

[Jakob von Raumer]

Already have some identifier from a different language, which shall serve as (the approximation of) the file name

[Julian Berman]

Why disallow non-ASCII filenames?

[Jakob von Raumer]

Just some vague encoding PTSD

[Weiyi Wang]

This reminds me of Con.lean https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Never.20name.20a.20file.20Con.2Elean/with/531319786