.vo files vary from build order

[bmwiedemann]

Description of the problem

While working on reproducible builds for openSUSE, I found that
In addition to #11227 , there are variations in .vo files
that go away when I build on a filesystem that has deterministic readdir order and build with make instead of make -j4 - so that the builds happen in deterministic order.

/usr/lib64/coq/theories/FSets/FSetList.vo differs at offset '9059' (data)
--- /tmp/tmp.KtRUkpybQT/old.yPM 2019-12-02 10:39:36.148042421 +0000
+++ /tmp/tmp.KtRUkpybQT/new.vUR 2019-12-02 10:39:36.148042421 +0000
@@ -1,11 +1,11 @@
 00002340  8b e6 08 d0 e1 81 57 ec  a0 a0 28 4d 53 65 74 4c  |......W...(MSetL|
 00002350  69 73 74 a0 25 4d 53 65  74 73 a0 23 43 6f 71 40  |ist.%MSets.#Coq@|
-00002360  90 30 35 20 c8 a4 e3 1b  b6 aa ca 98 d2 da c7 7f  |.05 ............|
-00002370  f0 c1 a0 a0 29 4f 72 64  65 72 73 41 6c 74 a0 2a  |....)OrdersAlt.*|
+00002360  90 30 b5 b2 78 25 9a ee  e4 62 59 2b 46 34 9c 6c  |.0..x%...bY+F4.l|
+00002370  48 e4 a0 a0 29 4f 72 64  65 72 73 41 6c 74 a0 2a  |H...)OrdersAlt.*|
 00002380  53 74 72 75 63 74 75 72  65 73 a0 23 43 6f 71 40  |Structures.#Coq@|
 00002390  90 30 5c 91 d4 af b1 94  2f 7a 6f 13 17 a2 75 69  |.0\...../zo...ui|
-000023a0  ed 79 b1 cf 42 6c ca 2c  09 6f 38 78 f9 cc b9 cc  |.y..Bl.,.o8x....|
-000023b0  d4 7a 00 02 af 1c 84 95  a6 be 00 02 8b 52 00 00  |.z...........R..|
+000023a0  ed 79 6e 87 f6 25 58 27  a4 20 92 36 b7 1c 3b 0e  |.yn..%X'. .6..;.|
+000023b0  f3 06 00 02 af 1c 84 95  a6 be 00 02 8b 52 00 00  |.............R..|

https://github.com/bmwiedemann/openSUSE/blob/master/packages/c/coq/coq.spec#L77 has the details of how we build.

Coq Version

8.9.1

[ejgallego]

Umm, that's bizarre and certainly a bug; while we try to debug, do you have access to the differing files?

You can use votour [a binary in checker/] which is a vo file explorer to see what's exactly the different bit.

[SkySkimmer]

Since it looks like a Require issue it may be worth trying with 8.11/master.

[ejgallego]

master sees the same problem, I was able to reproduce.

[ejgallego]

Looks a bit tricky to analyze, I guess having the ability for votour to produce a diff would help.

I need to take care of other stuff, I reproduced just doing two dune builds, one with -j 8 and the other with -j 3.

[ppedrot]

It might be due to the fact that hashconsing is not fully deterministic. Depending on the way the list of identifiers are processed we might get different in-memory representation.

[ejgallego]

It might be due to the fact that hashconsing is not fully deterministic. Depending on the way the list of identifiers are processed we might get different in-memory representation.

Indeed I was wondering if the difference would be in the hash-cons, but how can this happen? Not for terms at least; almost surely what's causing the difference here is that we are taking some has of the directory contents.

[SkySkimmer]

In add_vo_path the directory names are put through Id.of_string which hconses in some arbitrary order. Maybe we should order the result of all_subdirs somehow.
(around https://github.com/coq/coq/blob/de91f71b2e25e66ba4dd1f1db6582f5fea205591/vernac/loadpath.ml#L246-L266)

[ejgallego]

Maybe we should order the result of all_subdirs somehow.

I don't understand how this affects the hashconsing, tho even ordering would not yield the same results as for example some directories may not be present between two runs I think.

[bmwiedemann]

I could not find votour in openSUSE, so I uploaded 2 versions of one affected .vo file to https://rb.zq1.de/other/coq/ so that you can analyze it more closely.

[ppedrot]

@bmwiedemann the Coq version you used to generate these two files is still 8.9.1, right?

There is more than a change of representation, it seems that the provided files are different just because the vo files they are depending on are already different. Indeed, vo files store a digest of their dependencies and it happens in your example that it's essentially what is changing.

[ppedrot]

Forgot to mention, but the single offending file in your example is Coq.MSets.MSetList. For the file 1, it has digest b5b278259aeee462592b46349c6c48e4 and for the other 3520c8a4e31bb6aaca98d2dac77ff0c1.