diff --git a/README.md b/README.md index 273a102..802b5ea 100644 --- a/README.md +++ b/README.md @@ -230,10 +230,10 @@ Performance on 15/04/24 On a machine with 32 processors i9-13950HX and 64G RAM: -| HOL-Light file | dump-simp | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo | -|----------------------|-----------|-----------|-------------|-------------|--------------|-------------|--------------|--------------| -| hol.ml | 3m57s | 3 Go | 8 M | 5679 | 36s | 25s | 0.4 Go | 16m22s | -| Multivariate/make.ml | 1h55m | 52 Go | 89 M | 18866 | 18m11s | 18m43s | 2.3 Go | 8h (*) | +| HOL-Light file | dump-simp | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo | +|------------------------------------|-----------|-----------|-------------|-------------|--------------|-------------|--------------|--------------| +| hol.ml | 3m57s | 3 Go | 5 M | 5679 | 36s | 25s | 0.4 Go | 16m22s | +| Multivariate/make_upto_topology.ml | 48m | 52 Go | 52 M | 18866 | 18m11s | 18m43s | 2.3 Go | 8h (*) | (*) with `make spec; make -j32 vo; make -j8 vo`