Checker "con-leche" on test "navier-stokes-euler"
Checker: con-leche 路 Version: 0d2f467 路 馃搫 Declaration 路 馃敆 Source
Test: navier-stokes-euler 路 Expected: 馃憤 accept 路 Size: 1.5鈥疓B 路 Lines: 28.6鈥疢 路 lean4export: 3.1.0 路 Lean: 4.34.0-rc2 路 Timeout: 40.0鈥痬in 路 馃搫 Declaration 路 馃敆 Source
Result: 馃憤 accepted 路 exit code 0 路 wall time: 84.2鈥痵 路 instructions: 2.7鈥疶 路 max rss memory: 1.4鈥疓B 路 run 2026-10-24 20:10:08 UTC
stdout:
con-leche: accepted 126468 declarations (--verified)
stderr:
con-leche: stats: phases: parse 3.2s, install 2.9s, check 77.9s con-leche: stats: install pool: 2.399s wall, 4 workers + the commit thread, 126468 records, busy 10.014s (83.4%); tail 0.000s after the last start, 1 busy then, 0.000s worker-time in it (4.4%) con-leche: stats: slowest installs: 0.261s def Nat.land (#1659); 0.162s inductive EulerMeanVariationalInverse.StrongMeanEvolution (#95851); 0.150s inductive EulerPacketMovingFrame.PhysicalGeometryData (#104023); 0.121s inductive EulerMeanPacketProvider.Data (#95680); 0.117s inductive EulerTransversePacketJoin.Budget (#104861) con-leche: stats: check pool: 77.917s wall, 4 workers, 124834 records, busy 311.546s (99.9%); tail 0.005s after the last start, 4 busy then, 0.004s worker-time in it (18.3%) con-leche: stats: slowest checks: 0.891s theorem NavierStokes.FiveProfileMoments.quadraticBilin._proof_6 (#50132); 0.569s theorem NavierStokes.FiveProfileMoments.quadraticBilin._proof_9 (#50135); 0.498s theorem EulerSourcePotentialCoefficient.timeNormalPath_bound (#106921); 0.492s theorem NavierStokes.TerminalCompensation.quadraticBilin._proof_6 (#57739); 0.451s theorem EulerBoundedFieldGramInverse.inversePath_gevrey (#106901) con-leche: stats: peak RSS 1.39 GiB