search

rlepigre / pml

New version of the PML language and (classical) proof assistant
http://pml-lang.org
MIT License
20 stars 2 forks source link

Cost of logging and Chrono #27

Open craff opened 6 years ago

craff commented 6 years ago

In function which are very frequently called, log and chrono can cost a lot. If I uncomment the log in add_term and add_valu, the cost of log+chorno in Equiv and Compare is a factor between 2 and 3.

we should create a binary "main.native" where this log/chrono on small function are disabled (keeping still the main one like typing) and a main.debug with all log and chrono.

craff commented 6 years ago

This could be cleanly implemented having two functions per log and two functions Chrono.add_time, the new one being inactive in main.native and active in main.debug.

We must make sure these function doing nothing are inlined and eliminated by OCaml.