coq export: check that identifiers are valid in rocq

[fblanqui]

This PR fixes #1391. The translation of an identifier is as follows:

• We first check whether it must be renamed using the maps given with the options --renaming and --mapping. If so, we just return the string given by the renaming maps without checking it further.
• Otherwise, we check that it is an ASCII identifier valid in Rocq. If not, we fail.

Hence, for instance, ε will fail, unless it is renamed to itself in the --renaming map (this works because we do not check the validity of strings to which identifiers are renamed).

Recognizing the unicode identifiers accepted by Rocq is non trivial (see https://github.com/rocq-prover/rocq/blob/master/clib/unicode.ml and https://github.com/rocq-prover/rocq/blob/master/parsing/cLexer.ml). As files do not usually contain so many unicode identifiers, asking users to declare them in --renaming seems like a good compromise.

Impact on performances:

• on holide library (626 Mb of dk files): the PR takes 33.3s while master takes 32.3s (+3%)

Other changes:

• We check that identifiers declared with the options --renaming and --mapping are not renamed twice.

TODO:

• measure impact of identifier validity checking on performances
• add option to deactivate validity checking ?
• port these changes to lean export (Add export to Lean #1197)

[fblanqui]

@melanie-taprogge @agontard @navimath Do you agree with those changes?

[melanie-taprogge]

@melanie-taprogge @agontard @navimath Do you agree with those changes?

I agree with the changes. You are of course right that automatic renaming could introduce collisions and make names harder to trace. Fail-fast behaviour together with explicit renaming is surely the better solution. I can sure work with this solution in my translation pipeline. Thank you for looking into it Frédéric.