@Enrico Tassi You mentioned somewhere that you wanted to replace .aux files. What would you replace them with? Are they useful to have today?
They serve two purposes. In one case they carry data for other tools, they should be inside the .vo. In another case they can be used when the same file is recompiled, they tell the stm if a proof is big and also which context part is used. In this case they can't be in the .vo since make clean;make would kill them. I don't know where to put them for the second use case.
I suppose the second part can be thought of as a kind of "cache"?
kind of, but that cache has a syntax in form of proof using for the context, while there is no syntax for the timing info.
Last updated: Feb 22 2024 at 03:02 UTC