How deterministic is lean4export?

Stream: lean4

[James E Hanson]

I have been playing around with lean4export and I noticed that in larger environments, the order in which declarations are exported is sensitive to seemingly irrelevant changes to the original .lean file. I'm assuming that this is either the result of concurrent processing or hashing or both, but what exactly is going on?

[Julian Berman]

lean4export's implementation is pretty simple, it's basically one file: https://github.com/leanprover/lean4export/blob/master/Export.lean plus the main which basically just loads the environment -- there's no concurrency, so it'll likely have to do with the HashMaps there

[Chris Bailey]

I did consider adding some kind of up-front sort (I think it would be like a lexical sort on the declarations in the loaded modules), but It's also possible for changes that seem irrelevant in the vernacular to result in changes in the kernel representation or the olean file. Can you give some examples of the changes you're talking about?