Ali Caglayan (Jun 06 2022 at 10:31): Ali Caglayan (Jun 06 2022 at 10:31):@Enrico Tassi You mentioned somewhere that you wanted to replace .aux files. What would you replace them with? Are they useful to have today?
Enrico Tassi (Jun 06 2022 at 20:11):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.
Ali Caglayan (Jun 06 2022 at 22:00):I suppose the second part can be thought of as a kind of "cache"?
Enrico Tassi (Jun 07 2022 at 06:28):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: Jun 09 2023 at 07:01 UTC