Stream: Coq devs & plugin devs

Topic: Auxiliary files


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Jun 06 2022 at 22:00):

I suppose the second part can be thought of as a kind of "cache"?

view this post on Zulip 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: Feb 06 2023 at 00:03 UTC