This notation causes me some trouble in jsCoq/waCoq (from PLF):
Notation "P [ X |-> a ]" := (assn_sub X a P)
(at level 10, X at next level, a custom com).
It leads to some serialization issue, which only seems to occur when a custom com
is used.
What is a custom com
and what is it doing here? Is anyone familiar with how it is represented in Coq's internals? The issue is some inconsistency between how the obj file is stored in 64-bit vs. 32-bit arch. (@Emilio Jesús Gallego Arias ??)
Oh :face_palm:
| ETConstr (InCustomEntry s,_,x) ->
let n = match fst (precedence_of_position_and_level from_level x) with
| LevelLt n -> n-1
| LevelLe n -> n
| LevelSome -> max_int in
InCustomEntryLevel (s,n)
Ouch!!
That certainly deserves a patch I think.
We don't make any promise about vo files being the same in 32 and 64-bit though.
There are other sources of difference that can be exploited.
@Pierre-Marie Pédrot actually what @Shachar Itzhaky did is to generate files using a 64-bit OCaml that do still run fine in a 32-bit runtime, he only had to use Marshall.Compat_32
and wrap the hashcons , so it is not about compatibility, but more about using a 64-bit OCaml to generate the .vo files that are then used in JSOO [which doens't have 64-bit integers]
This is a pain and I advised against it, however OSX users have the little problem that 32-bit binaries are not supported anymore :S
@Shachar Itzhaky so I guess we can patch this by taking max_int_32_bit
instead, right?
Some hashes are not the same in 32 and 64 bit runs. You people are actively looking for trouble.
Exactly. I would rather not rely on this brittle hack, but unfortunately Apple has dropped support for 32-bit programs altogether, and in the new arm64 architecture they are virtually nonexistent. I could not find a way to compile a 32-bit version of OCaml as a 64-bit executable (although, in theory, this could be done). I am happy to hear other suggestions. Anyway we are building our releases using Docker on Linux, so we can use the 32-bit OCaml there.
Emilio Jesús Gallego Arias said:
Shachar Itzhaky so I guess we can patch this by taking
max_int_32_bit
instead, right?
Not really since OCaml int is 31 bit :very_angry: I had to use (1 lsl 30) - 1
...
I am not sure what's your exact problem, but vo files are (should?) be platform independent, despite being architecture dependent. Why don't you generate the vo files on a machine with proper 32 bit support ?
Use 0x3FFFFFFF
Pierre-Marie Pédrot said:
I am not sure what's your exact problem, but vo files are (should?) be platform independent, despite being architecture dependent. Why don't you generate the vo files on a machine with proper 32 bit support ?
Yes that's what I was saying about the release builds. We can use 32 bit there. For development, having to run the build on a different machine is a bit cumbersome and may be a blocker for some macOS users who want to hack on jsCoq. So we allow both kinds of build. 32-bit is the default, 64-bit is only used on macOS.
Such a dev process will likely trigger eisenbugs due to different hash generation, so there should be a huge warning somewhere
If there is such a deviation in hash generation then we might be in trouble even with a 32-bit build since the .vo
files are built using native coqc
on top of native OCaml, but are read in the browser environment using js_of_ocaml / WebAssembly build of ocamlrun. So if you have any pointers to where hash generation can deviate despite being clipped to fit in a 31-bit int, I am very interested in hunting down and plugging those instances.
This is our current patch: https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/coerce-32bit.patch
Also, this is just one more reason to have extensive testing using different libraries and I'm looking forward to integrating @Enrico Tassi's suggestion based on Coq smoke tests.
I added a warning about this in docs/build.md
.
@Pierre-Marie Pédrot hash generation is patched so hashes are 31 bits even when using a 64-bit OCaml , so that's ok so far. Indeed that's not ideal but see the dire situation for developing on 32 bit on OSX
Last updated: Jun 10 2023 at 06:31 UTC