From 0844871a4106f93ed92fdd7a44b39b181ca21088 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 13 Oct 2023 19:42:22 +0200 Subject: [PATCH] update README and NOTES --- NOTES.md | 2 ++ README.md | 12 ++++++------ 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/NOTES.md b/NOTES.md index ec57b6e..a6c60c3 100644 --- a/NOTES.md +++ b/NOTES.md @@ -1,6 +1,8 @@ NOTES ----- +- instrumenting BETA_CONV reduces the number of proof steps of `hol.ml` by 0.1% only + - instrumenting SYM reduces the number of proof steps of `hol.ml` by 4% - replacing ALPHA by REFL reduces the number of proof steps of `hol_upto_arith` from 405621 to 324391 (-20%)! diff --git a/README.md b/README.md index b693984..2d4fb6a 100644 --- a/README.md +++ b/README.md @@ -299,14 +299,14 @@ Multi-threaded translation to Dedukti with `mk 1000` and `-j 7`: * dkcheck is unable to check the generated dk file on my laptop for lack of memory (I have only 32 Go RAM and the process is stopped after 11m16s) Results for `hol.ml` up to `arith.ml` with `mk 7` and `-j 7` (by commenting from `loads "wf.ml"` to the end): - * proof dumping time: 11.7s 82 Mo - * number of proof steps: 324 K - * dk file generation: 6.6s 82 Mo - * checking time with dk check: 13.6s - * lp file generation: 3.7s 56 Mo + * proof dumping time: 12s 77 Mo + * number of proof steps: 302 K + * dk file generation: 6s 76 Mo + * checking time with dk check: 13s + * lp file generation: 4s 52 Mo * checking time with lambdapi: 1m22s (1m30s with `-c`) * translation to Coq: 2.8s 52 Mo - * checking time for Coq 8.17.1: 3m59s + * checking time for Coq 8.18.0: 4m34s Exporting pure Q0 proofs ------------------------