Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Scalable operations for Thm.instanti...


view this post on Zulip Email Gateway (Sep 22 2021 at 10:32):

From: Makarius <makarius@sketis.net>
* ML *

This refers to Isabelle/4974c3697fee.

Many years ago, I made measurements that showed that the naive association
lists were actually sufficient for most applications. Now I did change my mind
and made it more scalable: the impact is hardly measurable, apart from
https://isabelle.sketis.net/devel/build_status/macOS_11_Big_Sur_4_threads/index.html#session_HOL-Record_Benchmark
where there is a clear reduction of runtime.

That example also shows that more heap space is required: 2-3 trees require
more overhead than plain list.

Right now I am inclined to leave this new status-quo, unless someone comes
with concrete applications that require further tuning (e.g. a different
implementation behind the now abstract data types of Vars.table etc.)

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC