warning: trigraph ignored

Stream: lean4

[Mario Carneiro]

I got this funny error while compiling Mathlib:

./lake-packages/proofwidgets/build/ir/ProofWidgets/Component/PenroseDiagram.c:1465:456698: warning: trigraph ignored [-Wtrigraphs]

This points into the middle of a very long minified javascript string in _init_l_ProofWidgets_PenroseDiagram___closed__1:

...return r.setEdge({i:Q,j:i,e:o}),[Q,i]},T=a(t.primary);for(;!o.isEmpty();)a(o.dequeue());...
                                                   -- ^ here

I don't really know what trigraph it's talking about there, but maybe long string literals are problematic for the C compiler?

[Mauricio Collares]

Why is this an error? Ignoring a trigraph should be OK, right? Processing it as a trigraph would be bad.

[Mauricio Collares]

The file indeed contains ??(, which should be processed as [ if the compiler is being strict with trigraphs (but we don't want it to, so the warning tells us the compiler is doing what we want).

[Reid Barton]

Assuming that this is a C toolchain invocation that is controlled by Lean, it seems safe to disable the warning (-Wno-trigraphs), though it could also be a good idea to add a test to Lean that it doesn't inadvertently enable trigraph processing.

[Scott Morrison]

@Mac Malone, if this is a C invocation being made by lake, could you please create an issue to track this?

[Scott Morrison]

@Yicheng Qian just made https://github.com/leanprover/lean4/issues/2829.

[Joachim Breitner]

I investigated a bit, more details at the issue.