Skip to content

Commit

Permalink
update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
fblanqui committed Jan 17, 2025
1 parent bfed5bd commit 8c5cf1a
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -239,10 +239,10 @@ Performances

On a machine with 32 processors i9-13950HX, 64 Gb RAM, Hol2dk master, HOL-Light 3.0.0, OCaml 5.2.1, Camlp5 8.03.01, Lambdapi c24b28e2 and Coq 8.20.0:

| HOL-Light file | dump | size | steps | thms | lp | v | size | vo |
|------------------------------|-------|--------|-------|-------|-----|-----|-------|---------|
| hol.ml | 3m58s | 3 Gb | 3 M | 5687 | 40s | 37s | 1 Gb | 52m21s |
| Multivariate/make_complex.ml | 3h | 135 Gb | 85 M | 40728 | 48m | 31m | 91 Gb | >23h47m |
| HOL-Light file | dump | size | steps | thms | lp | v | size | vo |
|------------------------------|-------|--------|-------|-------|-----|-----|-------|--------|
| hol.ml | 3m58s | 3 Gb | 3 M | 5687 | 40s | 37s | 1 Gb | 52m21s |
| Multivariate/make_complex.ml | 3h | 135 Gb | 85 M | 40728 | 50m | 31m | 91 Gb | 34h49m |

Translating HOL-Light proofs to Dedukti
---------------------------------------
Expand Down

0 comments on commit 8c5cf1a

Please sign in to comment.