[BUG] Marshalling problems in > 4.0.0 (jsCoq / coq-lsp)

[ejgallego]

Dear JSOO devs,

we are seeing some issues with JSOO > 4.0.0 in jsCoq, in particular when trying to read back a marshalled .vo file.

The error we get is "File "_vendor+v8.20+32bit/coq/lib/objFile.ml", line 110, characters 11-17: Assertion failed."

This assertion fails:

 let () = assert (Int64.equal (LargeFile.pos_in ch) (Int64.add s.pos s.len)) in

So maybe the regression is not in Marshall. Note that the files read are small in size.

git bisect points to:

Runtime: update io.js, fix md5.js: 78ba544fb3dbcdb3437feafd43a8bdf6cba0d954

which makes sense given the Coq code above.

This on OCaml 4.12, 32bit.

Thanks for all your help.

[ejgallego]

Here is a trace with a good and bad JSOO version:

Good:

segment: summary | s.pos: 16 | s.len: 406 | pos_in: 422 

Bad:

segment: summary | s.pos: 16 | s.len: 406 | pos_in: 828

[ejgallego]

Seems like Marshall double-counted the number of bytes read, as in bad we have: 828 = 16 + 406 * 2

[hhugo]

Seems like Marshall double-counted the number of bytes read, as in bad we have: 828 = 16 + 406 * 2

Yes, it was double counting.