"make" overwrites previous "make vos" progress

[RalfJung]

Description of the problem

When mixing "make vos" and "make" on the same checkout (which can easily happen accidentally), there are some bad interactions. Concretely, after a make vos finishes, when I type make and immediately Ctrl-C it, a subsequent make vos rebuilds everything. Somehow, building a vo file seems to destroy the corresponding vos file in a way that the next vos build needs to be re-done from scratch.

Coq Version

8.13.0

[SkySkimmer]

The old .vos must be destroyed as otherwise we would load outdated files, I don't see a way around it.

[RalfJung]

The .v files did not change, so the old .vos is still up-to-date with the code. Why would not destroying it lead to using outdated files?

[silene]

.vos files override .vo files, so if you do not erase them as .vo files are built, then there is no point on building .vo files in the first place.

[silene]

I suppose we could fix the issue by tampering with the modification date of the empty .vos file so that it matches the modification date of the erased .vos file. No idea if OCaml provides a suitable API for that low-level stuff.

[RalfJung]

.vos files override .vo files, so if you do not erase them as .vo files are built, then there is no point on building .vo files in the first place.

Are you saying when I build a .vo file and import another module, and both a .vo and .vos file exist for that other module, and the .vos file is older, Coq will still load the .vos file?

I would have expected .vo builds to never import .vos files.

[silene]

No, that is not what I am saying. When you are building a .vo file, .vos files are not considered. But, when you are building a .vos file, .vo files are taken into consideration, because they are more accurate universe-wise (but that is only if the corresponding .vos files are empty).

[RalfJung]

But then I don't understand why "there is no point on building .vo files in the first place". The point is to check universes. But .vos builds can keep using .vos files and all is fine -- or rather, all would be fine if .vo builds wouldn't delete the perfectly fine .vos files.

[silene]

Think about the interactive use of Coq. If you are doing Require, you want to see the universes from the .vo files if you have compiled them, not the broken ones from .vos files.

[ejgallego]

@RalfJung coqc will produce a 0-sized vos everytime a vo file is produced, because the build system cannot provide the information to coqc about what targets are stale and which ones are up to date.

[RalfJung]

Think about the interactive use of Coq. If you are doing Require, you want to see the universes from the .vo files if you have compiled them, not the broken ones from .vos files.

What currently happens in interactive use is that I have to wait until the .vo build completes (>30min), or re-do the .vos build (still ~5min). And that just because I accidentally did make followed by Ctrl-C. That's worse, IMO.^^

If I did make vos, I am totally fine with Require using broken universes. So I don't think what Coq does here is a good idea. If I wanted Coq to delete previous build results I'd do make clean, not make.

[RalfJung]

coqc will produce a 0-sized vos everytime a vo file is produced, because the build system cannot provide the information to coqc about what targets are stale and which ones are up to date.

The job of coqc is to produce one file and one file only, why would it even care with other files are stale or not?

Or does this go back to the old problem that on Require, Coq will prefer a .vos over a .vo even if the .vos file is many months old? But that can be fixed by simply checking the modification time and loading the newer file; no need to delete valid and up-to-date files.

[ejgallego]

The job of coqc is to produce one file and one file only, why would it even care with other files are stale or not?

It needs indeed to know which file to choose when both are present, so the current rules is pick the vos unless it is zero-sized.

Or does this go back to the old problem that on Require, Coq will prefer a .vos over a .vo even if the .vos file is many months old? But that can be fixed by simply checking the date and loading the newer file; no need to delete valid and up-to-date files.

Using a date is unreliable , even if a vos file is older it could still be valid.

[RalfJung]

Using a date is unreliable , even if a vos file is older it could still be valid.

How is using a date ever worse that always preferring the vos file? If both vos and vo exist, and the vo is newer, then most likely the vo is "at least as valid" as the vos. So we can handle the case @silene mentioned without ever deleting any files.

[ejgallego]

How is using a date ever worse that always preferring the vos file? If both vos and vo exist, and the vo is newer, then most likely the vo is "at least as valid" as the vos.

This case never happens as coqc won't always prefer the .vos file, if the .vos file 0-size, then it uses the .vo, and if the .vo is produced, coqc will ensure that the old .vos is zero-sized. So indeed, you cannot have "both vos and vo exists but vo is newer"

[RalfJung]

Yes but I am saying that the way you are ensuring this is bad.^^ Namely, you are deleting valid and up-to-date files. That's a bad idea, it destroys work that might have to be redone later.

My proposed scheme is intended to work without destroying valid data and forcing work to be re-done.

[ejgallego]

The date idea was discussed in the original PR, but likely had some problems, maybe because it is hard to add the conditional to the build rules? I don't recall to be honest. I think vio uses something like that and was also creating some trouble.

[RalfJung]

How do the build rules come in here? I imagined they'd be unchanged.

[RalfJung]

It just happened again that I accidentally killed 20min worth of building vos files by accidentally building a single vo file. :/

[Blaisorblade]

How do the build rules come in here? I imagined they'd be unchanged.

If B depends on A, what file does B.vos depend on? A.vos, or something complex?

Honestly I’d rather (have an option for) B.vos depend on A.vos, and stop Coq -vos from ever loading vo files.

That’d reject this idea:

Think about the interactive use of Coq. If you are doing Require, you want to see the universes from the .vo files if you have compiled them, not the broken ones from .vos files.

[RalfJung]

I just discovered another bad interaction...

• make the entire project (so we have all the .vo files)
• edit some file somewhere in the middle ofthe dependency chain
• make vos, then notice that this rebuilds everything from the root of the dependency chain and realize that you actually want a .vo, so Ctrl-C
• make -- but sadly now it again starts from the root of the dependency chain!

So, not only dos make delete previous make vos progress, the other way around also seems to be true: make vos, when there are things that need to be rebuild, will delete make progress that is earlier in the dependency chain than what had to be rebuilt.

Now I have to wait another 30min until this re-build is done...