Zulip Chat Archive

Stream: lean4

Topic: benchmark #2800

Schrodinger ZHU Yifan (Nov 01 2023 at 21:25):

This is just an experiment for now. I experienced some differences locally when doing large amounts of numerical operations. I understand such situations are rather rare but I still hope to see if there is any accumulated effect. Thanks!
https://github.com/leanprover/lean4/pull/2800

Scott Morrison (Nov 02 2023 at 05:00):

Are you asking someone to run a benchmark? I'm unclear what this message is intending.

Schrodinger ZHU Yifan (Nov 02 2023 at 06:14):

yeah. if that is possible

Scott Morrison (Nov 02 2023 at 06:14):

Done.

Last updated: Dec 20 2023 at 11:08 UTC