Stream: jsCoq

Topic: Some trouble with `a custom com`

Shachar Itzhaky (Jan 20 2021 at 19:51):

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 ??)

Shachar Itzhaky (Jan 20 2021 at 21:44):

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)

Emilio Jesús Gallego Arias (Jan 26 2021 at 10:09):

Ouch!!

Emilio Jesús Gallego Arias (Jan 26 2021 at 10:09):

That certainly deserves a patch I think.

Pierre-Marie Pédrot (Jan 26 2021 at 10:11):

We don't make any promise about vo files being the same in 32 and 64-bit though.

Pierre-Marie Pédrot (Jan 26 2021 at 10:11):

There are other sources of difference that can be exploited.

Emilio Jesús Gallego Arias (Jan 26 2021 at 10:58):

@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]

Emilio Jesús Gallego Arias (Jan 26 2021 at 10:58):

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

Emilio Jesús Gallego Arias (Jan 26 2021 at 10:59):

@Shachar Itzhaky so I guess we can patch this by taking max_int_32_bit instead, right?

Pierre-Marie Pédrot (Jan 26 2021 at 11:00):

Some hashes are not the same in 32 and 64 bit runs. You people are actively looking for trouble.

Shachar Itzhaky (Jan 26 2021 at 11:02):

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.

Shachar Itzhaky (Jan 26 2021 at 11:04):

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...

Pierre-Marie Pédrot (Jan 26 2021 at 11:04):

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 ?

Pierre-Marie Pédrot (Jan 26 2021 at 11:04):

Use 0x3FFFFFFF

Shachar Itzhaky (Jan 26 2021 at 11:05):

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.

Pierre-Marie Pédrot (Jan 26 2021 at 11:06):

Such a dev process will likely trigger eisenbugs due to different hash generation, so there should be a huge warning somewhere

Shachar Itzhaky (Jan 26 2021 at 11:10):

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.

Shachar Itzhaky (Jan 26 2021 at 11:11):

This is our current patch: https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/coerce-32bit.patch

Shachar Itzhaky (Jan 26 2021 at 11:13):

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.

Shachar Itzhaky (Jan 26 2021 at 11:40):

I added a warning about this in docs/build.md.

Emilio Jesús Gallego Arias (Jan 26 2021 at 12:46):

@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