Karl Palmskog (Nov 03 2021 at 11:18): 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.
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
No idea @Karl Palmskog , yes we use jsoo and working fine here, tho we are in more recent compiler versions
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)
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
Shachar Itzhaky (Nov 12 2021 at 11:52):Yes, I do believe jsCoq requires at least 4.10 now. The default is 4.12.
Emilio Jesús Gallego Arias (Nov 12 2021 at 11:52):@Karl Palmskog is there a need for jsCoq + 4.07.1 ?
Karl Palmskog (Nov 12 2021 at 11:52):4.07.1 had a good run, it's been my favorite OCaml release ever
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
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
Emilio Jesús Gallego Arias (Nov 12 2021 at 11:53):for jsCoq we purposely support a very narrow set of stuff
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"
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
Emilio Jesús Gallego Arias (Nov 12 2021 at 11:54):so you don't really have a choice, but neither a problem
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
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