UniMath
Kernel Term Sharing
In several files, either the command Set Kernel Term Sharing. or Unset Kernel Term Sharing. is used (https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:flag.Kernel-Term-Sharing). I have a couple of questions:
- What does this command do and why it is useful?
- Could it be useful in other files as well?
That option was discussed more frequently many years ago, e.g., in https://github.com/UniMath/UniMath/issues/625#issuecomment-284799214.
Back then, it seemed unpredictable whether (un)setting this option improved or worsened things. I have not understood the workings or effects of this option in the meantime.
There is some slow code in several parts of the repository. Would it be worth to experiment whether using that setting at several could help improving the compilation time?
There is some slow code in several parts of the repository. Would it be worth to experiment whether using that setting at several could help improving the compilation time?
From the documentation (https://github.com/SkySkimmer/coq/commit/581e34c649b0d36b3d4f4f0fa80fcd0d4efa861b) it seems that sharing is activated by default.
I think before investing a lot of time in experiments it would be worth asking the Coq devs what the status of this option is, for instance, on the Coq Zulip.
I was interested to see whether it could change the compilation time in some files in Bicategories, because small changes like that might affect it. I was not planning to do a lot of experimentation with it.
Ah, I see. That's a great idea. I seem to remember that there was a way to show the compilation times of all files, in decreasing order. That could be useful for this undertaking. But probably you know well which files take a long time.
I think kernel term sharing means that every term is cached in a hash table, so that each term appears in memory only once.
