Return to Answer

I am going to propose the most obvious solution in order to see why you dislike it. Keep in mind that loading anything from the disk is an order of magnitude slower than performing actions in memory, so an additional pass through the loaded code will not be a bottleneck.

Let $M$ be the map taking an identifier name $x$ to its unique identity $M(x)$, presumed to be an integer. There is also a global counter $C$ whose value is larger than any identity so far.

Upon saving a unit $A$, you also have to save the accompanying map $M_A$, so that later on, when $A$ is loaded, other (non-compiled) units will be able to refer to entities in $A$ by their names.

Upon loading a unit $A$ and its accompanying map $M_A$, we perform a global shift: we change each $M(x)$ to $M(x) + C$, and we shift all identities in $A$ by adding $C$ to them. We also increment $C$ by the size of $M$. (If you want to "save integers" you can shift $M_A$ down to $0$ when saving the file.)

If your identities are not integers and you cannot use addition to shift them, then you can create a temporary remapping table $R$ which takes each $M_A(x)$ to a new fresh identity $R(M_A(x)) = M'_A(x)$. You then go through $A$ and apply $R$ throughout, and replace $M_A$ with $M_A'$.

You also need to merge $M_A$ with your global $M$, the details of which may depend on your naming scheme for compilation units.

The proposed solution is standard. The first sentence of the Wikipedia page on dynamic linking says (emphasis mine):

In computing, a dynamic linker is the part of an operating system that loads and links the shared libraries needed by an executable when it is executed (at "run time"), by copying the content of libraries from persistent storage to RAM, filling jump tables and relocating pointers.

Regarding storing data on the disk: this is known as code marshaling. Real programming languages have good support for it, Ocaml has the standard libary module Marshal. It's fast and it saves you a ton of trouble, but note that code marshalled with this module is going to be specific to the OCaml compiler, and thus not very portable, so you would still have to distribute source code. (Python is like that, nobody tries to distribute compiled Python.) However, you should only worry about portability after your proof assistant has more than 666 users, at which point one of them will volunteer to implement portable marshaling for you.

I am going to propose the most obvious solution in order to see why you dislike it. Keep in mind that loading anything from the disk is an order of magnitude slower than performing actions in memory, so an additional pass through the loaded code will not be a bottleneck.

Let $M$ be the map taking an identifier name $x$ to its unique identity $M(x)$, presumed to be an integer. There is also a global counter $C$ whose value is larger than any identity so far.

Upon saving a unit $A$, you also have to save the accompanying map $M_A$, so that later on, when $A$ is loaded, other (non-compiled) units will be able to refer to entities in $A$ by their names.

Upon loading a unit $A$ and its accompanying map $M_A$, we perform a global shift: we change each $M(x)$ to $M(x) + C$, and we shift all identities in $A$ by adding $C$ to them. We also increment $C$ by the size of $M$. (If you want to "save integers" you can shift $M_A$ down to $0$ when saving the file.)

If your identities are not integers and you cannot use addition to shift them, then you can create a temporary remapping table $R$ which takes each $M_A(x)$ to a new fresh identity $R(M_A(x)) = M'_A(x)$. You then go through $A$ and apply $R$ throughout, and replace $M_A$ with $M_A'$. This solution is more principled, and has a negligible additional cost.

You also need to merge $M_A$ with your global $M$, the details of which may depend on your naming scheme for compilation units.

The proposed solution is standard. The first sentence of the Wikipedia page on dynamic linking says (emphasis mine):

In computing, a dynamic linker is the part of an operating system that loads and links the shared libraries needed by an executable when it is executed (at "run time"), by copying the content of libraries from persistent storage to RAM, filling jump tables and relocating pointers.

Regarding storing data on the disk: this is known as code marshaling. Real programming languages have good support for it, Ocaml has the standard libary module Marshal. It's fast and it saves you a ton of trouble, but note that code marshalled with this module is going to be specific to the OCaml compiler, and thus not very portable, so you would still have to distribute source code. (Python is like that, nobody tries to distribute compiled Python.) However, you should only worry about portability after your proof assistant has more than 666 users, at which point one of them will volunteer to implement portable marshaling for you.

I am going to propose the most obvious solution in order to see why you dislike it. Keep in mind that loading anything from the disk is an order of magnitude slower than performing actions in memory, so an additional pass through the loaded code will not be a bottleneck.

Let $M$ be the map taking an identifier name x to its unique identity M(x), presumed to be an integer. There is also a global counter C whose value is larger than any identity so far.

Upon saving a unit A, you also have to save the accompanying map M, so that later on, when A is loaded, other (non-compiled) units will be able to refer to entities in A by their names.

Upon loading a unit A and its accompanying map M, we perform a global shift: we change each M(x) to M(x) + C, and we shift all identities in A by adding C to them. We also increment C by the size of M.

If your identities are not integers and you cannot use addition to shift them, then you can create a temporary remapping table R which takes each M(x) from A to a new fresh identity M'(x). You then go through A and apply R throughout, and replace M with M'.

The proposed solution is standard. The first sentence of the Wikipedia page on dynamic linking says (emphasis mine):

In computing, a dynamic linker is the part of an operating system that loads and links the shared libraries needed by an executable when it is executed (at "run time"), by copying the content of libraries from persistent storage to RAM, filling jump tables and relocating pointers.

Regarding storing data on the disk: this is known as code marshaling. Real programming languages have good support for it, Ocaml has the standard libary module Marshal. It's fast and it saves you a ton of trouble, but note that code marshalled with this module is going to be specific to the OCaml compiler, and thus not very portable, so you would still have to distribute source code. (Python is like that, nobody tries to distribute compiled Python.) However, you should only worry about portability after your proof assistant has more than 666 users, at which point one of them will volunteer to implement portable marshaling for you.

I am going to propose the most obvious solution in order to see why you dislike it. Keep in mind that loading anything from the disk is an order of magnitude slower than performing actions in memory, so an additional pass through the loaded code will not be a bottleneck.

Let $M$ be the map taking an identifier name $x$ to its unique identity $M(x)$, presumed to be an integer. There is also a global counter $C$ whose value is larger than any identity so far.

Upon saving a unit $A$, you also have to save the accompanying map $M_A$, so that later on, when $A$ is loaded, other (non-compiled) units will be able to refer to entities in $A$ by their names.

Upon loading a unit $A$ and its accompanying map $M_A$, we perform a global shift: we change each $M(x)$ to $M(x) + C$, and we shift all identities in $A$ by adding $C$ to them. We also increment $C$ by the size of $M$. (If you want to "save integers" you can shift $M_A$ down to $0$ when saving the file.)

If your identities are not integers and you cannot use addition to shift them, then you can create a temporary remapping table $R$ which takes each $M_A(x)$ to a new fresh identity $R(M_A(x)) = M'_A(x)$. You then go through $A$ and apply $R$ throughout, and replace $M_A$ with $M_A'$.

You also need to merge $M_A$ with your global $M$, the details of which may depend on your naming scheme for compilation units.

The proposed solution is standard. The first sentence of the Wikipedia page on dynamic linking says (emphasis mine):

In computing, a dynamic linker is the part of an operating system that loads and links the shared libraries needed by an executable when it is executed (at "run time"), by copying the content of libraries from persistent storage to RAM, filling jump tables and relocating pointers.

Regarding storing data on the disk: this is known as code marshaling. Real programming languages have good support for it, Ocaml has the standard libary module Marshal. It's fast and it saves you a ton of trouble, but note that code marshalled with this module is going to be specific to the OCaml compiler, and thus not very portable, so you would still have to distribute source code. (Python is like that, nobody tries to distribute compiled Python.) However, you should only worry about portability after your proof assistant has more than 666 users, at which point one of them will volunteer to implement portable marshaling for you.

I am going to propose the most obvious solution in order to see why you dislike it. Keep in mind that loading anything from the disk is an order of magnitude slower than performing actions in memory, so an additional pass through the loaded code will not be a bottleneck.

Let $M$ be the map taking an identifier name x to its unique identity M(x), presumed to be an integer. There is also a global counter C whose value is larger than any identity so far.

Upon saving a unit A, you also have to save the accompanying map M, so that later on, when A is loaded, other (non-compiled) units will be able to refer to entities in A by their names.

Upon loading a unit A and its accompanying map M, we perform a global shift: we change each M(x) to M(x) + C, and we shift all identities in A by adding C to them. We also increment C by the size of M.

If your identities are not integers and you cannot use addition to shift them, then you can create a temporary remapping table R which takes each M(x) from A to a new fresh identity M'(x). You then go through A and apply R throughout, and replace M with M'.

The proposed solution is standard. The first sentence of the Wikipedia page on dynamic linking says (emphasis mine):

In computing, a dynamic linker is the part of an operating system that loads and links the shared libraries needed by an executable when it is executed (at "run time"), by copying the content of libraries from persistent storage to RAM, filling jump tables and relocating pointers.

Regarding storing data on the disk: this is known as code marshaling. Real programming languages have good support for it, Ocaml has the standard libary module Marshal. It's fast and it saves you a ton of trouble, but note that code marshalled with this module is going to be specific to the OCaml compiler, and thus not very portable, so you would still have to distribute source code. (Python is like that, nobody tries to distribute compiled Python.) However, you should only worry about portability after your proof assistant has more than a 666 users, at which point one of them will volunteer to implement portable marshaling for you.

I am going to propose the most obvious solution in order to see why you dislike it. Keep in mind that loading anything from the disk is an order of magnitude slower than performing actions in memory, so an additional pass through the loaded code will not be a bottleneck.

Let $M$ be the map taking an identifier name x to its unique identity M(x), presumed to be an integer. There is also a global counter C whose value is larger than any identity so far.

Upon saving a unit A, you also have to save the accompanying map M, so that later on, when A is loaded, other (non-compiled) units will be able to refer to entities in A by their names.

Upon loading a unit A and its accompanying map M, we perform a global shift: we change each M(x) to M(x) + C, and we shift all identities in A by adding C to them. We also increment C by the size of M.

If your identities are not integers and you cannot use addition to shift them, then you can create a temporary remapping table R which takes each M(x) from A to a new fresh identity M'(x). You then go through A and apply R throughout, and replace M with M'.

The proposed solution is standard. The first sentence of the Wikipedia page on dynamic linking says (emphasis mine):

In computing, a dynamic linker is the part of an operating system that loads and links the shared libraries needed by an executable when it is executed (at "run time"), by copying the content of libraries from persistent storage to RAM, filling jump tables and relocating pointers.

Regarding storing data on the disk: this is known as code marshaling. Real programming languages have good support for it, Ocaml has the standard libary module Marshal. It's fast and it saves you a ton of trouble, but note that code marshalled with this module is going to be specific to the OCaml compiler, and thus not very portable, so you would still have to distribute source code. (Python is like that, nobody tries to distribute compiled Python.) However, you should only worry about portability after your proof assistant has more than 666 users, at which point one of them will volunteer to implement portable marshaling for you.