Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Yes, I already keep track of what's been loaded since even when loading everything from source I don't want to load things multiple times. To tell which unit something comes from, my current idea is that each "identity" is actually a pair of integers, one labeling the unit it came from and one counting the definitions in that unit. Then the compiled file and the loading process both store a correspondence between loaded absolute file paths and numbers, and combining them we obtain a function from numbers to numbers that we apply to the first components of identities as we walk the terms.
Thanks, I look forward to it. Having now written out the problem carefully, I think I can imagine a solution a bit better. Each compiled unit maintains a list of all the other units it imported, the identity offsets for each of them, and the range of identities that came from that unit. Then when loading it, whenever we encounter an identity in a stored term, we look it up to find what unit it came from, subtract the stored offset for that unit, and then add the corresponding offset for that same unit in the current run. Is that sufficient?
As I said, I could write some code that tries to do this, but it's starting to feel about as complicated as manually munging De Bruijn indices when weakening under binders, and hence as easy to get wrong. So I was hoping that someone else had written out instructions or sample code that I could just copy and be more confident of not making a mistake.
But now at the point that $A$ is loaded, maybe we've already loaded $B$ and shifted its $M_B$ by a different constant $C_B'$. So when we pass through the $A$ terms, we don't just have to rename all the $A$ identities by adding one constant $C_A$, we have to rename all the $B$ identities by subtracting $C_B$ and adding $C_B'$. So that means that when we encounter an identity while traversing the $A$ terms, we have to be able to tell which unit it came from originally, and have stored enough information to know what to add to it.
Yes, this is indeed the first thing I thought of also. Thanks for writing it out clearly with justification. The complication that I was not sure what to do about is that the unit $A$ could itself import another unit $B$, which might already have been compiled at the time $A$ was compiled. So there is an $M_B$ from when $B$ was compiled, and then when $A$ is compiled it had to shift $M_B$ by adding a constant $C_B$ and those are the identities of the $B$ constants appearing in the saved $A$ terms.
Thanks! Equality checking is what I really wanted to know about, so I hope an actual expert shows up. I'm not sure why you're so exercised about my asking what actual proof assistants do currently; it seems to me like a perfectly reasonable thing to want to know. I didn't say I was planning to copy them. I've read plenty about the "right" or "future" way to do things; is it so ridiculous to want to be able to compare that in an informed way with what people have done in the past?
After I read through the elaboration zoo, will I know what is done in Agda and in Coq? If not, I don't regard it as an answer. I want to avoid digging through their source code myself; I assumed that there was someone in the world who's already familiar with that source code and would be able to tell me what it does.
I don't think spartan type theory and the elaboration zoo are "real-world" proof assistants in the sense I meant. I want to know what implementation techniques have actually been proven scalable.
