widget tests failing

Stream: general

[Scott Morrison]

I'm getting failures in CI for a branch for leanprover-community/lean, relating to widgets:

  56/1416 Test #1372: leanwidgettest_widget4.input ................................***Failed    0.54 sec
--- widget4.input.expected.out  2021-10-23 04:27:25.805376368 +0000
+++ widget4.input.produced.out  2021-10-23 04:37:08.700235320 +0000
@@ -1,3 +1,3 @@
 {"msgs":[{"caption":"","file_name":"widget4.lean","pos_col":0,"pos_line":3,"severity":"information","text":"(widget)","widget":{"column":0,"id":3,"line":3}}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"response":"ok","seq_num":1,"widget":{"column":0,"html":{"c":[{"a":{"className":"list pl0"},"c":[{"a":{"className":"lh-copy"},"c":[{"a":{"className":"goal-goals"},"c":["expected type:"],"t":"strong"}],"t":"li"},{"a":{"className":"lh-copy"},"c":[{"c":[{"a":{"className":"list pl0 font-code","key":"416938290"},"c":[{"a":{"key":"_mlocal._fresh.10.103"},"c":[{"a":{"className":"goal-vdash b"},"c":["⊢ "],"t":"span"},{"c":[{"c":[{"a":{"className":"expr","key":"695702567"},"c":[{"a":{"className":"expr-boundary","key":"[]"},"c":[{"a":{"key":"true"},"c":["true"],"e":{"onClick":{"h":2,"r":[6,5,4,3]},"onMouseEnter":{"h":1,"r":[6,5,4,3]}},"t":"span"}],"t":"span"}],"e":{"onMouseLeave":{"h":0,"r":[6,5,4,3]}},"t":"span"}]}]}],"t":"li"}],"t":"ul"}]}],"t":"li"}],"t":"ul"}]},"id":3,"line":3}}
+{"response":"ok","seq_num":1,"widget":{"column":0,"html":{"c":[{"a":{"className":"list pl0"},"c":[{"a":{"className":"lh-copy"},"c":[{"a":{"className":"goal-goals"},"c":["expected type:"],"t":"strong"}],"t":"li"},{"a":{"className":"lh-copy"},"c":[{"c":[{"a":{"className":"list pl0 font-code","key":"417325350"},"c":[{"a":{"key":"_mlocal._fresh.10.97"},"c":[{"a":{"className":"goal-vdash b"},"c":["⊢ "],"t":"span"},{"c":[{"c":[{"a":{"className":"expr","key":"695702567"},"c":[{"a":{"className":"expr-boundary","key":"[]"},"c":[{"a":{"key":"true"},"c":["true"],"e":{"onClick":{"h":2,"r":[6,5,4,3]},"onMouseEnter":{"h":1,"r":[6,5,4,3]}},"t":"span"}],"t":"span"}],"e":{"onMouseLeave":{"h":0,"r":[6,5,4,3]}},"t":"span"}]}]}],"t":"li"}],"t":"ul"}]}],"t":"li"}],"t":"ul"}]},"id":3,"line":3}}
ERROR: file widget4.input.produced.out does not match widget4.input.expected.out

It seems this discrepancy can't be very consequential; it is presumably an auto-generated key that has changed.

[Scott Morrison]

Can such tests be made more robust?

[Gabriel Ebner]

In such cases it is useful to use git diff --word-diff. Indeed what has changed is the local unique name of a hypothesis (which is generated by lean using mk_fresh_name).

[Gabriel Ebner]

I don't think it is worth it to make the test more robust. Please just update the expected.out file.