Stream: jsCoq

Topic: broken js_of_ocaml on 4.07.1


view this post on Zulip Karl Palmskog (Nov 03 2021 at 11:18):

is jsCoq still using js_of_ocaml these days? Because a bunch of js_of_ocaml packages are now seemingly broken on OCaml 4.07.1 (won't compile). Just wanted to check.

view this post on Zulip Karl Palmskog (Nov 03 2021 at 12:15):

if anyone is hooked up to upstream, here is a failing build: https://github.com/coq-community/sudoku/runs/4091274840?check_suite_focus=true

and this is the error message:

  #=== ERROR while compiling js_of_ocaml-compiler.3.10.0 ========================#
  # context              2.0.9 | linux/x86_64 | ocaml-variants.4.07.1+flambda | https://opam.ocaml.org#e0262986
  # path                 ~/.opam/4.07.1+flambda/.opam-switch/build/js_of_ocaml-compiler.3.10.0
  # command              ~/.opam/4.07.1+flambda/bin/dune build -p js_of_ocaml-compiler -j 2 @install
  # exit-code            1
  # env-file             ~/.opam/log/js_of_ocaml-compiler-411-a33be6.env
  # output-file          ~/.opam/log/js_of_ocaml-compiler-411-a33be6.out
  ### output ###
  # Error: This definition has type
  # [...]
  #     ocamlopt compiler/lib/.js_of_ocaml_compiler.objs/native/js_of_ocaml_compiler__Annot_parser.{cmx,o} (exit 2)
  # (cd _build/default && /home/coq/.opam/4.07.1+flambda/bin/ocamlopt.opt -w -40 -w -7-37 -safe-string -g -I compiler/lib/.js_of_ocaml_compiler.objs/byte -I compiler/lib/.js_of_ocaml_compiler.objs/native -I /home/coq/.opam/4.07.1+flambda/lib/biniou -I /home/coq/.opam/4.07.1+flambda/lib/bytes -I /home/coq/.opam/4.07.1+flambda/lib/easy-format -I /home/coq/.opam/4.07.1+flambda/lib/menhirLib -I /home[...]
  # File "annot_parser.ml", line 74, characters 2-1980:
  # Error: This definition has type
  #          'ttv_tail.
  #            _menhir_env ->
  #            'ttv_tail -> _menhir_state -> 'tv_arg_annot list -> 'freshtv208
  #        which is less general than
  #          'ttv_tail 'ttv_return.
  #            _menhir_env ->
  #            'ttv_tail -> _menhir_state -> 'tv_arg_annot list -> 'ttv_return

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2021 at 14:08):

No idea @Karl Palmskog , yes we use jsoo and working fine here, tho we are in more recent compiler versions

view this post on Zulip Karl Palmskog (Nov 03 2021 at 14:09):

this build error occurs both on 3.10.0 and 3.11.0 (on OCaml 4.07.1, but not 4.11.2 which I switched to in the end)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2021 at 14:26):

I'd submit a bug report to the main opam repos, seems indeed like an issue; in jsCoq we use 4.12 to better support M1 users

view this post on Zulip Shachar Itzhaky (Nov 12 2021 at 11:52):

Yes, I do believe jsCoq requires at least 4.10 now. The default is 4.12.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 11:52):

@Karl Palmskog is there a need for jsCoq + 4.07.1 ?

view this post on Zulip Karl Palmskog (Nov 12 2021 at 11:52):

4.07.1 had a good run, it's been my favorite OCaml release ever

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 11:53):

Yes I agree, it was a nice release, 4.12 is looking pretty good too

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 11:53):

or 4.11, indeed I'm always in 4.07 or 4.11 these days

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 11:53):

for jsCoq we purposely support a very narrow set of stuff

view this post on Zulip Karl Palmskog (Nov 12 2021 at 11:53):

no I don't currently run jsCoq anywhere, so no complaints other than, "I have to remember to use 4.12"

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 11:54):

the whole toolchain for jsCoq is vendored, including the ocaml runtime in the case of wacoq

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 11:54):

so you don't really have a choice, but neither a problem

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 11:54):

as a user you just download the build artifacts for the browser, you don't care about OCaml

view this post on Zulip Karl Palmskog (Nov 12 2021 at 11:55):

yeah I wish that were the case across all the Frankenstein projects I use Coq in


Last updated: Sep 26 2023 at 12:02 UTC