[tools] AARCH-25405: Clarification οf the IC-Coherence-before and Instruction-read-ordered-before definitions

[TiberiuBucur]

This changes the way miaou7 transliterates variants into LaTeX. In the case of a conjunction of multiple variants as part of a condition, each variant is now a separate \item, which is then translated into exactly one line of markdown. In addition, each variant needs to be uniquely defined in catdefinitions.tex. The generic Variant[1] and NotVariant[1] commands have been removed.

[relokin]

Thanks for this Tiberiu.

I think it would be nice to avoid the post processing step and I am wondering whether we should actually remove the macros \Variant{#1} and \NotVariant{#1} altogether.

If miaou would produce a different macro for each variant we would be able to handle that specific macro in the catdefinitions.tex file correctly. We need to support:

• \Variant{ETS2} which we should change to \ETS2{} and then \ETS2{} would expand to "FEAT_ETS2 is implemented"
• \Variant{ETS3} which we should change to \ETS3{} and then \ETS3{} would expand to "FEAT_ETS3 is implemented"
• \Variant{DIC} which we should change to \DIC{} and then \DIC{} would expand to "The Effective value of DIC is 1"
• \NotVariant{DIC} which we should change to \NotDIC{} and then \NotDIC{} would expand to "The Effective value of DIC is 1"
• \Variant{IDC} which we should change to \IDC{} and then \IDC{} would expand to "The Effective value of IDC is 1"
• \NotVariant{IDC} which we should change to \NotIDC{} and then \NotIDC{} would expand to "The Effective value of IDC is 1"

@fsestini please chime in if you think there is a better solution.

[fsestini]

Unless there’s a particular reason for preferring post-processing the markdown, I would agree with @relokin. Moreover, having dedicated macros in catdefinitions.tex would incidentally also benefit uoaim7, since that tool (at least currently) relies on catdefinitions.tex to match prose to corresponding cat symbols.

[TiberiuBucur]

Thanks for your comments @relokin @fsestini. I made the change you requested, with a small tweak: unfortunately non-alphabetic characters are not supported in the name of new commands, so I transliterated the digits in letters. I converted the PR to ready to review, since the ticket has been communicated.
The CI seems to be failing due to an issue that is not apparent to me. I have not modified the required Ocaml version, nor did I use code that requires a newer version, so perhaps it is a hiccup with the runner.

[fsestini]

I'm assuming these commands should result in printing FEAT_ETS2 or similar.

I don't know to what extent the markdown/pandoc post-processing is affected, but \string_ does not seem to print an actual underscore when run through pdflatex on my local TeX Live installation. \textunderscore{}, however, does.