Zulip Chat Archive

Hello, we are organizing a school in december and I was wondering if js/wa coq is able to load Elpi and Hierarchy-Builder (and hence a preview of MathComp 2.0). https://coq.vercel.app/ shows an elpi package, but you get a Not_found when elpi is required.

Emilio Jesús Gallego Arias (Nov 03 2022 at 18:01):

Hi @Enrico Tassi , not sure about what the status is now, but for sure we can make it work, even if we need to hardcode elpi

Emilio Jesús Gallego Arias (Nov 03 2022 at 18:06):

Need to check what the status in v8.16 is tho, we have made a lot of changes including unifying the WebAssembly / js_of_ocaml backend

Enrico Tassi (Nov 03 2022 at 20:11):

I'm planning a release of coq-elpi in 2 week max, so it would help to know if I have to change something there.
For now From elpi Require Import elpi gives a Not_found on https://coq.vercel.app/ . How do you get a trace? I could not try the wa backed, is it online?

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:46):

@Enrico Tassi I think the ball is on our side, tho I'd help if we could fix https://github.com/coq/coq/issues/16571 (for the build setup) tho I'm unsure if that bug is actually not me messing up.

But indeed what is on vercel is quite off from the current status, so I'd recommend either getting the docker image (jsCoq SDK) or buidling it yourself.

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:51):

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:53):

Actually maybe just using the "legacy" syntax for the Declare ML Module may work

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:53):

Enrico Tassi (Nov 04 2022 at 06:56):

what is unclear is that in theory requiring elpi.vo needs no external file other than the cmxs.
Can we have maybe a short session where we debug this together? I've the feeling it would go much faster.

Enrico Tassi (Nov 04 2022 at 06:57):

Enrico Tassi (Nov 04 2022 at 07:56):

@Emilio Jesús Gallego Arias and/or @Shachar Itzhaky would you be available next week to tackle this together?

Emilio Jesús Gallego Arias (Nov 04 2022 at 11:25):

Yes, I'm unsure about my schedule next week due to some personal stuff but for sure I can find a slot

Emilio Jesús Gallego Arias (Nov 04 2022 at 11:26):

Enrico Tassi (Nov 04 2022 at 12:14):

Emilio Jesús Gallego Arias (Nov 04 2022 at 15:08):

Enrico Tassi (Nov 04 2022 at 16:38):

Emilio Jesús Gallego Arias (Nov 04 2022 at 19:57):

Is the version in npm for 8.15 too old for you ? If that one works, I think it'd be way easier for you to start with the 8.15 version, then we can upgrade more calmy to 8.16

Emilio Jesús Gallego Arias (Nov 04 2022 at 19:57):

Shachar Itzhaky (Nov 06 2022 at 11:07):

Hi Enrico! I am working on a PLDI submission this week but will be available afterwards (not sure if you meant 7/11 or 14/11; the latter should be fine)

Enrico Tassi (Nov 07 2022 at 10:32):

I'm building the whole thing myself for 8.15. I'm following the instructions for jscoq. Is there something similar for wacoq?
I've a new submodule for jscoq-addons for hierarchy-builder. How am I supposed to submit a pr? I mean, I have an entire repo, not a commit.

Shachar Itzhaky (Nov 07 2022 at 10:41):

actually I had hierarchy-builder in mathcom-extra, I think it was working ok for 8.15 but perhaps you have better patches?

Enrico Tassi (Nov 07 2022 at 10:53):

Shachar Itzhaky (Nov 07 2022 at 10:57):

Enrico Tassi (Nov 07 2022 at 12:00):

Enrico Tassi (Nov 07 2022 at 12:03):

In particular I'm doing

google-chrome --allow-file-access-from-files --js-flags="--harmony-tailcalls" --js-flags="--stack-size=65536" _build/jscoq+32bit

, so I guess I should put these files somewhere in _build

Shachar Itzhaky (Nov 07 2022 at 12:06):

you are right we did not explain well enough. This is meant for when you install your own version of jsCoq with NPM (in a third directory, i.e. on your website) and then you can also install this .tgz packages. Now if you want to test from your build dir, which is a very sensible and reasonable thing to do and we should explain that, then you should run npm i /path/to/package.tgz in the jsCoq source tree. After you have done that you should run dune build again so that it updates the packages in _build/jscoq+32bit as well.

Shachar Itzhaky (Nov 07 2022 at 12:08):

an alternative that's good for quick testing is to use the npm link feature. It is an NPM subcommand that creates a symlink to the source dir rather than installing the dist file, which means that if you rebuild the package you don't have to reinstall. The downside is that if you then run Dune in the jsCoq source tree, then Dune will delete your symlink and you will have to link it again.

Shachar Itzhaky (Nov 07 2022 at 12:08):

Enrico Tassi (Nov 07 2022 at 12:10):

Shachar Itzhaky (Nov 07 2022 at 12:11):

Enrico Tassi (Nov 07 2022 at 12:28):

gares@ollypat:~/work-area/2022-12-school-files/jscoq$ find . -name hierarchy-builder
./_build/jscoq+32bit/node_modules/@jscoq/hierarchy-builder
./node_modules/@jscoq/hierarchy-builder

       node coq-pkgs [jscoq+32bit]
wrote coq-pkgs/init.coq-pkg.
wrote coq-pkgs/coq-base.coq-pkg.
wrote coq-pkgs/coq-collections.coq-pkg.
wrote coq-pkgs/coq-arith.coq-pkg.
wrote coq-pkgs/coq-reals.coq-pkg.
wrote coq-pkgs/ltac2.coq-pkg.
wrote coq-pkgs/coq.json.
        make coq-pkgs [jscoq+32bit]

Shachar Itzhaky (Nov 07 2022 at 14:31):

this is just the command that makes the stdlib. did it not run npm i as well?
you should see a _build/jscoq+32bit/node_modules/@jscoq/hierarchy-builder.

Shachar Itzhaky (Nov 07 2022 at 14:35):

here is another suggestion, it is a bit messy at the moment but hopefully we will have a more streamlined solution soon after the refactor that @Emilio Jesús Gallego Arias has done and bugfixes to Dune:

Enrico Tassi (Nov 07 2022 at 14:58):

Shachar Itzhaky (Nov 07 2022 at 14:59):

yeah I mean after it has run npm i you should see that. but I guess it did not run it somehow. maybe delete _build/*/node_modules?

Shachar Itzhaky (Nov 07 2022 at 14:59):

Enrico Tassi (Nov 07 2022 at 15:04):

gares@ollypat:~/work-area/2022-12-school-files/jscoq$ rm -rf _build/*/node_modules
gares@ollypat:~/work-area/2022-12-school-files/jscoq$ ls node_modules/@jscoq/
elpi  hierarchy-builder  mathcomp
gares@ollypat:~/work-area/2022-12-school-files/jscoq$ make jscoq
eval `opam env --set-switch --switch jscoq+32bit` && dune build @jscoq
         npm node_modules [jscoq+32bit]     ...
         npm dist [jscoq+32bit]  ...
gares@ollypat:~/work-area/2022-12-school-files/jscoq$ ls _build/jscoq+32bit/coq-pkgs/
coq-arith.coq-pkg        coq-collections.symb.json  init.symb.json
coq-arith.symb.json      coq.json                   ltac2.coq-pkg
coq-base.coq-pkg         coq-reals.coq-pkg          ltac2.symb.json
coq-base.symb.json       coq-reals.symb.json
coq-collections.coq-pkg  init.coq-pkg

Enrico Tassi (Nov 07 2022 at 15:05):

I can also start from scratch and wipe _build, no problem... but I think I tried and it changed nothing

Shachar Itzhaky (Nov 07 2022 at 15:06):

Enrico Tassi (Nov 07 2022 at 15:07):

{
  "name": "jscoq",
  "version": "0.15.1",
  "description": "A port of Coq to JavaScript -- run Coq in your browser",
  "bin": {
    "jscoq": "./dist/cli.js",
    "jscoqdoc": "ui-js/jscoqdoc.js"
  },
  "dependencies": {
    "@jscoq/elpi": "file:../jscoq-addons/_build/jscoq+32bit/jscoq-elpi-0.14.1.tgz",
    "@jscoq/hierarchy-builder": "file:../jscoq-addons/_build/jscoq+32bit/jscoq-hierarchy-builder-1.4.0.tgz",
    "@jscoq/mathcomp": "file:../jscoq-addons/_build/jscoq+32bit/jscoq-mathcomp-0.16.0.tgz",
    "array-equal": "^1.0.0",
    "bootstrap": "^5.1.3",

Enrico Tassi (Nov 07 2022 at 15:08):

$ ls ../jscoq-addons/_build/jscoq+32bit/jscoq-mathcomp-0.16.0.tgz -lh
-rw-rw-r-- 1 gares gares 30M nov.   7 11:53 ../jscoq-addons/_build/jscoq+32bit/jscoq-mathcomp-0.16.0.tgz

Shachar Itzhaky (Nov 07 2022 at 15:08):

ok probably npm is having a hard time with the relative paths, but that also strikes me as weird because npm is very trigger-happy when it comes to throwing error messages at you, it won't just silently ignore a dep because it cannot find the archive...

Enrico Tassi (Nov 07 2022 at 15:09):

Shachar Itzhaky (Nov 07 2022 at 15:09):

it is actually possible that if you put in an absolute path npm will transform it to a relative one...

Enrico Tassi (Nov 07 2022 at 15:10):

Enrico Tassi (Nov 07 2022 at 15:12):

gares@ollypat:~/work-area/2022-12-school-files/jscoq$ make jscoq
eval `opam env --set-switch --switch jscoq+32bit` && dune build @jscoq
        node coq-pkgs [jscoq+32bit]
wrote coq-pkgs/init.coq-pkg.
wrote coq-pkgs/coq-base.coq-pkg.
wrote coq-pkgs/coq-collections.coq-pkg.
wrote coq-pkgs/coq-arith.coq-pkg.
wrote coq-pkgs/coq-reals.coq-pkg.
wrote coq-pkgs/ltac2.coq-pkg.
wrote coq-pkgs/coq.json.
        make coq-pkgs [jscoq+32bit]
...

Shachar Itzhaky (Nov 07 2022 at 15:12):

that print is not going to change because it is only building these files during the jsCoq build, if you have other files they come from npm packages

Shachar Itzhaky (Nov 07 2022 at 15:13):

and they're not going to show up in coq-pkgs (perhaps unfortunately), they're going to be in node_modules

Enrico Tassi (Nov 07 2022 at 15:16):

hum, I think I'm missing something. Anyway, now jscoq sees two out of 3 packages (not HB, but elpi and mathcomp). I did edit all_pkgs in index.html...

Enrico Tassi (Nov 07 2022 at 15:16):

Anyway, From elpi Require Import elpi fails saying that "exit" is not implemented.

Enrico Tassi (Nov 07 2022 at 15:18):

so, for some reasons HB is not found... but there is that other problem first. Can wacoq circumvent it? Should I patch elpi/coq-elpi?

Enrico Tassi (Nov 07 2022 at 15:21):

Also, adding ?backend=wa when browsing locally index.html does not seem to change anything (I did run make wacoq).

Emilio Jesús Gallego Arias (Nov 07 2022 at 15:58):

Shachar Itzhaky (Nov 07 2022 at 15:59):

oh yes that is still in development, we unified the backends in order for this flag to be available

Shachar Itzhaky (Nov 07 2022 at 15:59):

Shachar Itzhaky (Nov 07 2022 at 16:00):

That is a missing stub but the real reason is that it is trying to call exit in the first place. we should try to understand why it even calls exit.

Shachar Itzhaky (Nov 07 2022 at 16:00):

@Emilio Jesús Gallego Arias could this be related to a findlib error? previously it raised an anomaly

Shachar Itzhaky (Nov 07 2022 at 16:01):

Enrico Tassi (Nov 08 2022 at 09:36):

/lib/elpi/elpi_plugin.cma loading....
stderr: cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.

Enrico Tassi (Nov 08 2022 at 09:36):

Of course I can modify the initialization code for coq-elpi, but you have to tell me how

Enrico Tassi (Nov 08 2022 at 10:19):

Enrico Tassi (Nov 08 2022 at 10:20):

And run a tiny program, so I think we are good w.r.t. elpi.
Now I've to understand why HB does not show up in the list of packages, probably my pckage was wrong, I'll look into the one in mathcomp-extras

Shachar Itzhaky (Nov 08 2022 at 10:46):

Enrico Tassi (Nov 08 2022 at 10:50):

for some reasons it looks for hierarchy-builder.json in coq-pkgs/ and not in node-modules/ even if I did the very same thing for elpi, which is correctly found.
ideas?

Shachar Itzhaky (Nov 08 2022 at 10:56):

Shachar Itzhaky (Nov 08 2022 at 10:57):

Oh right I had to remove the coq dep myself even in the previous versions of the addon...

Shachar Itzhaky (Nov 08 2022 at 10:58):

Enrico Tassi (Nov 08 2022 at 11:43):

Enrico Tassi (Nov 08 2022 at 11:44):

I mean, all_pkgs already contains a bunch of stuff, I've added HB there. I guess I need to do something else then...

Enrico Tassi (Nov 08 2022 at 11:45):

all_pkgs:  {'+': ['coq', 'mathcomp', 'equations', 'elpi', 'hierarchy-builder',
                          'quickchick', 'software-foundations',
                          'hahn', 'paco', 'snu-sflib',
                          'fcsl-pcm', 'htt', 'pnp', 'stdpp', 'iris'],

Shachar Itzhaky (Nov 08 2022 at 11:56):

Shachar Itzhaky (Nov 08 2022 at 11:57):

you need to add:
'node_modules/hierarchy-builder/coq-pkgs': ['hierarchy-builder']
(assuming this is where your pkg is)

Enrico Tassi (Nov 08 2022 at 12:22):

Shachar Itzhaky (Nov 08 2022 at 12:23):

Shachar Itzhaky (Nov 08 2022 at 12:24):

there is a hard-coded list of "affiliated" packages, those are packages listed under the @jscoq namespace in the npm repo

Shachar Itzhaky (Nov 08 2022 at 12:24):

to make it easier for users, if you want to use one of those, it is enough to just add them to the list and CoqManager translates the path.

Enrico Tassi (Nov 08 2022 at 12:38):

Wow, I got HB to load. One question: it does not load elpi automatically, I have to load it by hand before. where should I specify this dependenecy?

Enrico Tassi (Nov 08 2022 at 12:55):

Shachar Itzhaky (Nov 08 2022 at 14:17):

Shachar Itzhaky (Nov 08 2022 at 14:18):

actually I believe that it should load automatically if you run From elpi Import elpi. but perhaps there is a bug

Enrico Tassi (Nov 08 2022 at 14:23):

What I meant is that: From HB Require Import structures. does not work, but From elpi Require Import elpi. From HB Require Import structures. does. The first one fails with error "elpi.elpi" not found...

Shachar Itzhaky (Nov 08 2022 at 14:25):

Oh ok yes that is understandable because when building elpi you haven't told jsCoq about hierarchy-builder. It would be nice for it to detect automatically, perhaps with the facilities that @Emilio Jesús Gallego Arias is implementing in Dune this would be possible. For now, use my old plugin as reference:

Shachar Itzhaky (Nov 08 2022 at 14:27):

Enrico Tassi (Nov 08 2022 at 14:27):

Shachar Itzhaky (Nov 08 2022 at 14:29):

yes using WA should eliminate most if not all of the stack overflows. To build waCoq (stable for 8.15) you need to install wasi-sdk (I recommend v12 because this is what we used) and you have to first clone and build wacoq-bin

Shachar Itzhaky (Nov 08 2022 at 14:30):

Enrico Tassi (Nov 09 2022 at 09:19):

Enrico Tassi (Nov 09 2022 at 12:23):

I think I have wacoq built and installed, now I'm trying to compile the addons with make world CONTEXT=wacoq but I'm getting

...
    ocamlopt elpi/workdir/src/elpi_plugin_lib.{a,cmxa} [wacoq]
    ocamlopt elpi/workdir/src/elpi_plugin_lib.cmxs [wacoq]
   ocamlfind elpi/workdir/src/elpi_plugin.cmxs [wacoq]
Entering directory '/home/gares/work-area/2022-12-school-files/jscoq-addons'
      coqdep elpi/workdir/theories/elpi.v.d [wacoq]
        coqc elpi/workdir/theories/.elpi.aux,elpi/workdir/theories/elpi.{glob,vo} [wacoq]
calling Boot.init
File "elpi/dune", line 2, characters 0-163:
2 | (rule
3 |  (targets coq-pkgs)
4 |  (deps
5 |   (package coq-elpi)
6 |   workdir/src/elpi_plugin.cma)
7 |  (action
8 |   (run npx %{env:pkgtool=jscoq} build --workspace %{dep:elpi.json})))
         npx elpi/coq-pkgs [wacoq] (exit 127)
sh: 1: wacoqdoc: not found

any ideas of why wacoqdoc is not there and why it is needed in the first place? I have a coqdoc in the wacoq switch, but no wacoq

Shachar Itzhaky (Nov 09 2022 at 12:29):

Enrico Tassi (Nov 09 2022 at 13:03):

Shachar Itzhaky (Nov 09 2022 at 13:18):

Enrico Tassi (Nov 09 2022 at 13:19):

no, but I'm not running it explicitly. I'm just typing make world CONTEXT=wacoq in jscoq-addons

Enrico Tassi (Nov 09 2022 at 13:20):

Shachar Itzhaky (Nov 09 2022 at 13:22):

yeah that's basically it but the jscoq-addons is just a root Makefile that runs the sub-makefiles... it's not running commands. It seems like maybe your elpi Makefile is setting envvar pkgtool to wacoqdoc?

Shachar Itzhaky (Nov 09 2022 at 13:23):

oh dune-workspace.wacoq is supposed to set it but it sets it to wacoq not wacoqdoc

Shachar Itzhaky (Nov 09 2022 at 13:23):

wacoq comes from wacoq-bin, to get that one run npm link in wacoq-bin.

Shachar Itzhaky (Nov 09 2022 at 13:24):

but it baffles me that it's trying to run wacoqdoc instead, that is so f-ing weird

Enrico Tassi (Nov 09 2022 at 13:29):

Shachar Itzhaky (Nov 09 2022 at 13:35):

npx is short for npm exec which looks for JS scripts in node_modules directories. it has some complicated scheme. npm link puts a link to it in /usr/local/lib/node_modules/.bin or smt.

Shachar Itzhaky (Nov 09 2022 at 13:36):

the error message is strange, I should try your use case of npx wacoq without npm link prior to that

Enrico Tassi (Nov 09 2022 at 13:36):

I tried npx wacoq and I got the same error (no wacoqdoc), while npc jscoq complains I did not give a thing to buil

Shachar Itzhaky (Nov 09 2022 at 13:39):

Shachar Itzhaky (Nov 09 2022 at 13:41):

huh you are right it is installing wacoq from npm and then complains about wacoqdoc

Shachar Itzhaky (Nov 09 2022 at 13:42):

ofc it's installing the latest wacoq which is 0.16 and which does not have wacoqdoc because we have merged those...

Shachar Itzhaky (Nov 09 2022 at 13:42):

Enrico Tassi (Nov 09 2022 at 13:49):

so, I got the tgz for my packages for @wacoq, I did npm install them inside jscoq
but now how do I change index.html to get the wa backend?

Enrico Tassi (Nov 09 2022 at 13:49):

Shachar Itzhaky (Nov 09 2022 at 13:59):

Shachar Itzhaky (Nov 09 2022 at 14:00):

btw really sorry for all the voodoo, it took us forever to get the backend integration into shape but hopefully with the next version it would be smoother

Enrico Tassi (Nov 09 2022 at 14:10):

    var jscoq_opts = {
        backend: 'wa',
        implicit_libs: false,
        focus: false,
        editor: { mode: { 'company-coq': true } },
        all_pkgs:  {'+': ['coq', 'mathcomp', 'equations', 'elpi',
                          'quickchick', 'software-foundations',
                          'hahn', 'paco', 'snu-sflib',
                          'fcsl-pcm', 'htt', 'pnp', 'stdpp', 'iris'],
                    'node_modules/@wacoq/hierarchy-builder/coq-pkgs': ['hierarchy-builder'],
                    './examples': ['examples']}
    };

it will prints jscoq everywhere and I still get the stack overflows. How can I test it is indeed the wa backend running

Shachar Itzhaky (Nov 09 2022 at 14:13):

Enrico Tassi (Nov 09 2022 at 15:14):

ok, so one problem is that "make wacoq" does not put stuff in _build/jscoq+32bit which I was still using, so I did run make jscoq and for the updated index.html, and indeed I see "WA" logo

Enrico Tassi (Nov 09 2022 at 15:15):

but now the problem is that it does not find wacoq. I see a package.wacoq, but I don't even know how to tell npm to use that.

Enrico Tassi (Nov 09 2022 at 15:21):

can you give some hints on how to get things going?
I tried jscoq$ npm install ../wacoq-bin/wacoq-bin-0.15.1.tar.gz followed by make jscoq/wacoq but still many not found in the console

Shachar Itzhaky (Nov 09 2022 at 17:06):

uhm right you should either install or link it and you should probably expect all the missing libs because you have to install each package separately, or remove them from the list of all_pkgs

Shachar Itzhaky (Nov 09 2022 at 17:07):

the errors about missing libs are not harmful. as long as it can find the lib that you want and it appears in the list of packages

Shachar Itzhaky (Nov 09 2022 at 17:08):

Enrico Tassi (Nov 09 2022 at 20:30):

What is see is "loading worker 100%..." but the "..." is still running. In the console the only meaningful error is

Uncaught (in promise) TypeError: Failed to execute 'fetch' on 'WorkerGlobalScope': Failed to parse URL from ../bin/icoq.bc
    at z._fetchSimple (93ead2eb-ac7a-45ff-a…d658677d7d:2:316836)
    at z._fetch (93ead2eb-ac7a-45ff-a…d658677d7d:2:316671)
    at $.upload (93ead2eb-ac7a-45ff-a…d658677d7d:2:314254)
    at $.boot (93ead2eb-ac7a-45ff-a…d658677d7d:2:314094)
    at J (93ead2eb-ac7a-45ff-a…d658677d7d:2:317409)
    at 93ead2eb-ac7a-45ff-a…d658677d7d:2:317456
    at 93ead2eb-ac7a-45ff-a…d658677d7d:2:317489
    at 93ead2eb-ac7a-45ff-a…d658677d7d:2:317493

Shachar Itzhaky (Nov 09 2022 at 21:08):

Shachar Itzhaky (Nov 09 2022 at 21:09):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:11):

Mmm, how come do you get so many stack overflows, is elpi very deeply recursive?

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:12):

Shachar Itzhaky (Nov 09 2022 at 21:12):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:15):

Actually it shouldn't be too hard to have the findlib stuff working for 8.16, there are two paths:

Shachar Itzhaky (Nov 09 2022 at 21:18):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:23):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:24):

Shachar Itzhaky (Nov 09 2022 at 21:25):

oh yeah that's a good thing to try then. @Enrico Tassi I assume you are using -linkall otherwise the 8.15 version would not have worked at all?

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:25):

since 4.08, OCaml refuses to load modules twice, so now using a loader, modules are not doubly loaded

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:25):

Yes, 8.15 is using linkall otherwise it would have to declare all the deps manually in the .v file

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:25):

which is also an option but more fragile, as using -linkall does query ocamlfind so it uses the up to date library list

Shachar Itzhaky (Nov 09 2022 at 21:26):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:27):

no because the list used by coq makefile is actually a bit hacky, so coq and a few other things are excluded

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:27):

it does something like ocamlfind ocamlopt -packages elpi,pkg1,pkg2 -linkall elpi_plugin ...

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:28):

Shachar Itzhaky (Nov 09 2022 at 21:28):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:28):

Shachar Itzhaky (Nov 09 2022 at 21:28):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:28):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:29):

Shachar Itzhaky (Nov 09 2022 at 21:29):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:30):

it is great to build it with dune, but if we go in linkall business it is more painful

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:30):

it is great to build it with dune, but if we go in linkall business it is more painful

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:30):

tho newer dune can build elpi for the findlib just fine, but we need to fix coqdep

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:31):

it is great to build it with dune, but if we go in linkall business it is more painful

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:31):

tho newer dune can build elpi for the findlib just fine, but we need to fix coqdep

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:31):

Shachar Itzhaky (Nov 09 2022 at 21:31):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:31):

If we add the findlib.conf file + a tar.gz with the needed files, that should be fine now

Shachar Itzhaky (Nov 09 2022 at 21:32):

yes, I was working on a script using the hints you gave me but then I had to work on PLDI so it's not done

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:32):

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:33):

Shachar Itzhaky (Nov 09 2022 at 21:33):

Shachar Itzhaky (Nov 09 2022 at 21:36):

the only problem is I think findlib.conf should be there before the worker starts executing, so it's a bit delicate; need to make add it to init_libs maybe

Shachar Itzhaky (Nov 09 2022 at 21:37):

and I'm pretty sure I did "something" to make it look for findlib.conf in /lib; except I can't find it in the source

Emilio Jesús Gallego Arias (Nov 09 2022 at 21:39):

Enrico Tassi (Nov 10 2022 at 08:59):

I don't think 8.16 will make any difference w.r.t. stack overflows, so I'd rather focus on making the wa backend work

Enrico Tassi (Nov 10 2022 at 09:10):

class IcoqPod extends EventEmitter {

    core: OCamlExecutable
    intr: WorkerInterrupts

    binDir: string
    io: IO

    constructor(binDir?: string) {
        super();
        binDir = binDir || (typeof fetch === 'undefined'
                            || process.env.NODE_NOW ? './bin' : '../bin');

I don't see anyone passing an argument to the constructor of IcoqPodCLI (which inherits from this one) so I guess we go in the || branches

Enrico Tassi (Nov 10 2022 at 09:11):

Shachar Itzhaky (Nov 10 2022 at 09:33):

oh wait does the error come from the CLI? I thought this stack trace was in the browser

Shachar Itzhaky (Nov 10 2022 at 09:36):

I see now that this version is using typeof fetch == 'undefined' to determine whether fetch is available. This turned out to be wrong in the long term because newer versions of Node have fetch. So in fact 8.15 CLI is practically broken, this needs a patch.

Shachar Itzhaky (Nov 10 2022 at 09:37):

Enrico Tassi (Nov 10 2022 at 10:02):

Ah ok, I did hardcode 'file:///home/gares/work-area/2022-12-school-files/jscoq/_build/jscoq+32bit/node_modules/wacoq-bin/bin' and now it loads, but then it does not run, and I have no error on the console

Enrico Tassi (Nov 10 2022 at 10:03):

Enrico Tassi (Nov 10 2022 at 10:09):

the file '/lib/icoq.bc' has not the right magic number: expected Caml1999X029 got  Caml1999X027

Enrico Tassi (Nov 10 2022 at 10:09):

Enrico Tassi (Nov 10 2022 at 10:13):

ok, so I have jscoq+32bit and wacoq switches, and I guess one is 4.12 and the other 4.10

Enrico Tassi (Nov 10 2022 at 10:14):

Enrico Tassi (Nov 10 2022 at 10:15):

Enrico Tassi (Nov 10 2022 at 10:16):

Enrico Tassi (Nov 10 2022 at 10:47):

Shachar Itzhaky (Nov 10 2022 at 10:51):

Emilio Jesús Gallego Arias (Nov 10 2022 at 14:36):

Enrico Tassi (Nov 10 2022 at 15:13):

Compiled library elpi.elpi (in file /lib/elpi/elpi.vo) makes inconsistent assumptions over library Coq.Init.Notations

so I don't get how I got things desynchronized, since I've only used a single switch

Shachar Itzhaky (Nov 10 2022 at 15:15):

if you have recompiled wacoq after installing 4.12 then you have to make install again and only then recompile elpi.

Enrico Tassi (Nov 10 2022 at 15:18):

I did so, I guess I got something wrong
I also have a problem that HB is not showing up, even if I add

                    'node_modules/@wacoq/hierarchy-builder/coq-pkgs': ['hierarchy-builder']}

Enrico Tassi (Nov 10 2022 at 15:20):

make wacoq && make dist-npm-wacoq && npm install ./wacoq-0.15.1.tgz && google-chrome --allow-file-access-from-files --js-flags="--harmony-tailcalls" --js-flags="--stack-size=65536" node_modules/wacoq

Shachar Itzhaky (Nov 10 2022 at 15:20):

Enrico Tassi (Nov 10 2022 at 15:22):

sure, the opam switch was empty.
one thing that stinks is that the UI shows OCaml 4.10.2 (wasi-sdk-12), even if I'm sure I've 4.12 everywhere

Enrico Tassi (Nov 10 2022 at 15:22):

Emilio Jesús Gallego Arias (Nov 10 2022 at 16:02):

Enrico Tassi (Nov 10 2022 at 16:05):

are you saying the version string is hardcoded rather than detected at compile time?

Emilio Jesús Gallego Arias (Nov 10 2022 at 16:09):

In 8.15 you need to pull the wacoq-bin which may indeed pull a different version?

Emilio Jesús Gallego Arias (Nov 10 2022 at 16:09):

As in 8.15 the build involves 3 repos + the WASI SDK it is a bit hard to keep track of stuff

Emilio Jesús Gallego Arias (Nov 10 2022 at 16:10):

It seems to me still that the quickest path would be one of the two I pointed out above

Emilio Jesús Gallego Arias (Nov 10 2022 at 16:11):

Emilio Jesús Gallego Arias (Nov 10 2022 at 16:12):

tho it'd be still good to understand what is going on in the jsoo version, at least to report a bug with the stack overflow, browser version, and reproduction example

Enrico Tassi (Nov 10 2022 at 16:17):

Enrico Tassi (Nov 10 2022 at 16:18):

if the string is hardcoded... ok, but if it is detected then my build setup is borked

Shachar Itzhaky (Nov 10 2022 at 16:28):

Shachar Itzhaky (Nov 10 2022 at 16:29):

but then how is it even able to load the files if it has been compiled with ocaml 4.10

Enrico Tassi (Nov 14 2022 at 15:21):

So, the good news is that I managed to build and deploy all I want, here: https://www-sop.inria.fr/teams/marelle/MC-2022/
One thing which is annoying is that the packages don't load automatically, e.g. one has to download them first by clocking in the box bottom right. Actually it works for elpi, but not HB. Could you point me to the code where the magic happens?

Emilio Jesús Gallego Arias (Nov 14 2022 at 15:24):

Emilio Jesús Gallego Arias (Nov 14 2022 at 15:27):

That is found inside the hb.coq-pkg file, the json file contains this metadata

Emilio Jesús Gallego Arias (Nov 14 2022 at 15:28):

Enrico Tassi (Nov 14 2022 at 15:29):

Enrico Tassi (Nov 14 2022 at 15:33):

Next question is: is there a way to get the output printed without killing \n?
I don't have the time to make elpi code return the Pp.t (instead of printing the resulting string), which would be the nice solution

Emilio Jesús Gallego Arias (Nov 14 2022 at 15:36):

Shachar Itzhaky (Nov 14 2022 at 16:25):

Hi @Enrico Tassi , that's excellent! Even though the road was harsh at least it proves that jsCoq is workable (and even waCoq).

Shachar Itzhaky (Nov 14 2022 at 16:26):

Hmm it is possible that the HTML pretty-printer is placing the text in a regular div in the hope that Pp.t stuff has already taken care of all the line breaks. But that could be a good patch to add to that.

Enrico Tassi (Nov 14 2022 at 20:02):

Enrico Tassi (Nov 14 2022 at 20:03):

Enrico Tassi (Nov 14 2022 at 20:04):

HB.about builds a Pp.t, but I don't have an API like Feedback, I only have coq.say which takes a string.
I could make it take a Pp.t and make a feedback out of it, but I can't fix this in the little time I have left.

Emilio Jesús Gallego Arias (Nov 14 2022 at 20:15):

Emilio Jesús Gallego Arias (Nov 14 2022 at 20:16):

so I guess you can just add the style in the css so the text is white-space: pre-line

Emilio Jesús Gallego Arias (Nov 14 2022 at 20:18):

Shachar Itzhaky (Nov 14 2022 at 22:57):

probably we should add special treatment for that in FormatPrettyPrint, or perhaps it would just make sense to enable this pre-line style for ppboxes as well.

Emilio Jesús Gallego Arias (Nov 15 2022 at 15:16):

Enrico Tassi (Nov 16 2022 at 10:54):

I'm working on some scripts to ease the deployment of the entire stack.
I'm wondering why some parts of Coq are not compiled, like binary integers (which then force me to remove some stuff from mathcomp, etc).
Would it be possible to have the entire Coq stdlib built as a package?

Enrico Tassi (Nov 16 2022 at 12:20):

Shachar Itzhaky (Nov 16 2022 at 12:33):

oh interesting, this looks like a bug. I mean there have been some patches for the 64-bit mode but we have not knowingly removed modules. I know for sure that Bin is there; or at least has been (:wink:) -- which one is missing?

Enrico Tassi (Nov 16 2022 at 12:45):

maybe they are compiled but not packaged?
I'm talking about BinNat, PrimFloat... stuff I have to comment out of mathcomp and elpi in order to have the code loaded

Enrico Tassi (Nov 16 2022 at 12:46):

Shachar Itzhaky (Nov 16 2022 at 12:47):

Enrico Tassi (Nov 16 2022 at 12:50):

Emilio Jesús Gallego Arias (Nov 16 2022 at 16:28):

so it loads much faster, as these packages are basically only used in a few lines, and they add 100 MiB to the download or something like that

Emilio Jesús Gallego Arias (Nov 16 2022 at 16:28):

Emilio Jesús Gallego Arias (Nov 16 2022 at 16:29):

Enrico Tassi (Nov 17 2022 at 22:11):

Shachar Itzhaky (Nov 18 2022 at 11:26):

Oh interesting. I guess Sys.os_type would say "Unix" in WA; I don't know what it would say in jsoo

Emilio Jesús Gallego Arias (Nov 18 2022 at 13:01):

Enrico Tassi (Nov 18 2022 at 13:03):

Hum, is there a non hackish way? I mean, a standard file to look at in the WA filesystem? like /etc/debian-version

Emilio Jesús Gallego Arias (Nov 18 2022 at 13:03):

Emilio Jesús Gallego Arias (Nov 18 2022 at 13:04):

unless you want to patch the system, then you can add other file if you would like, still would be a hack until ocaml-wasm stabilizes tho

Enrico Tassi (Nov 18 2022 at 13:06):

I know that the file is, I just don't want the test to depend on the file name or location jscoq chooses

Emilio Jesús Gallego Arias (Nov 18 2022 at 13:08):

Enrico Tassi (Nov 18 2022 at 13:09):

Emilio Jesús Gallego Arias (Nov 18 2022 at 13:23):

Emilio Jesús Gallego Arias (Nov 18 2022 at 13:24):

Enrico Tassi (Nov 18 2022 at 13:50):

It is fine to get a None, but apparently Boot does an exit 1 in that mode.

Shachar Itzhaky (Nov 18 2022 at 14:33):

I thought this was solved after removing coq from the opam deps. Why is Boot called from a plugin? sounds a bit weird

Emilio Jesús Gallego Arias (Nov 18 2022 at 14:52):

That's still to be solved upstream, guess_coqlib has been doing that since a long time :(

Enrico Tassi (Nov 18 2022 at 14:56):

Elpi wants to know where user-contribs is. I don't think it is still necessary these days, since it can address files using Coq's resolver, but the code calls Boot in order to get the path (that is the API).

Shachar Itzhaky (Nov 18 2022 at 16:22):

hmm is this a new thing in elpi? I am surprised that I have not encountered the issue myself in the past.

Enrico Tassi (Nov 18 2022 at 17:29):

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:28):

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:32):

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:33):

So there were uses like let path = Envars.coqlib () / "path" which were turned into /path , which IMHO looks pretty dangerous

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:33):

So indeed I forbade that case; but the api for Boot.Env.init could allow the client to fail better for sure

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:34):

The thing is that Boot.Env.init also replaced Envars.guess_coqlib which had that pretty bad exit 1 semantics

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:35):

It just due to lack of time the API wasn't fixed in Coq, that PR was very painful to get even in that state

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:35):

Whether the previous situation, getting a non-sense path was better than the current one, I don't know, could be both ways

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:37):

Emilio Jesús Gallego Arias (Nov 18 2022 at 19:39):

Shachar Itzhaky (Nov 18 2022 at 19:41):

Enrico Tassi (Nov 18 2022 at 20:33):

setting it to anything would make the exisinting code not exit 1, so that would just work.

Shachar Itzhaky (Nov 18 2022 at 20:52):

Enrico Tassi (Nov 23 2022 at 15:28):

I tried to port my setup on 8.16 (using the legacy loading for elpi).
The good news is that the file:/// issue is gone, I can test locally.
The bad news is that it fails with

Anomaly "Uncaught exception (Failure
"Config file not found - neither /home/gares/COQ/WACOQ/opam/wacoq/lib/findlib.conf nor the directory /home/gares/COQ/WACOQ/opam/wacoq/lib/findlib.conf.d")." Please report at http://coq.inria.fr/bugs/.

Enrico Tassi (Nov 23 2022 at 15:29):

@Shachar Itzhaky you said you had a patch, but I cannot find (as a branch in jscoq or wacoq-bin)

Shachar Itzhaky (Nov 23 2022 at 16:15):

Shachar Itzhaky (Nov 23 2022 at 16:22):

Shachar Itzhaky (Nov 23 2022 at 16:24):

the call to this.findlibStartup is currently commented out because you need to prepare a zip with all the required libs and METAs. So I started creating this here script pkg-elpi.js specifically to package ELPI's dependencies (since it is currently the only affiliated non-legacy plugin).

Shachar Itzhaky (Nov 23 2022 at 16:26):

Enrico Tassi (Nov 23 2022 at 18:00):

Im using the legacy loading for elpi, so nothing special there. Is that commit part of the v8.16 branch? cause coq needs findlib.conf even if no plugin is loaded, it is during initialization that you need it.

Shachar Itzhaky (Nov 23 2022 at 18:58):

wait what
but this is commented out in WASM atm and still the 0.16.x's work fine. So how can this be.

Enrico Tassi (Nov 23 2022 at 21:20):

Enrico Tassi (Nov 23 2022 at 21:21):

Enrico Tassi (Nov 24 2022 at 10:49):

I'm trying to build the v8.16 branch of jscoq, which I understand includes what used to be wacoq-bin.
I'm doing:

make coq && make jscoq && make wacoq && make jscoq_worker && make wacoq_worker && make coq-pks && make dist-npm && make dist-npm-wacoq

make[1]: Entering directory '/home/gares/COQ/WACOQ/jscoq'
eval `opam env --set-switch --switch jscoq+32bit` && dune build @jscoq --no-buffer
wrote coq-pkgs/init.coq-pkg in 8941 ms.1)
wrote coq-pkgs/coq-base.coq-pkg in 4086 ms.
wrote coq-pkgs/coq-collections.coq-pkg in 2432 ms.
wrote coq-pkgs/coq-arith.coq-pkg in 3015 ms.
wrote coq-pkgs/coq-reals.coq-pkg in 4644 ms.
wrote coq-pkgs/ltac2.coq-pkg in 2391 ms.)
wrote coq-pkgs/coq.json.1 left) (jobs: 1)
Done: 99% (11852/11853, 1 left) (jobs: 1)make[2]: Entering directory '/home/gares/COQ/WACOQ/jscoq/_build/jscoq+32bit'
        node coq-pkgs [jscoq+32bit]
Done: 99% (11852/11853, 1 left) (jobs: 1)[Exception] Anomaly ""Assert_failure _vendor+v8.16+32bit/coq/lib/objFile.ml:107:11"." Please report at http://coq.inria.fr/bugs/.
Aborted.
Done: 99% (11852/11853, 1 left) (jobs: 1)make[2]: *** [Makefile:120: coq-pkgs/coq-arith.symb.json] Error 1
make[2]: Leaving directory '/home/gares/COQ/WACOQ/jscoq/_build/jscoq+32bit'
File "dune", line 5, characters 0-405:
 5 | (rule
 6 |  (targets coq-pkgs)
 7 |  (deps
....
15 |              --rootdir %{env:COQBUILDDIR_REL=????} --nostdlib)
16 |    ; building symbols using Make because Dune has no pattern rules T.T
17 |    (run make libs-symb))))
        make coq-pkgs [jscoq+32bit] (exit 2)

Shachar Itzhaky (Nov 24 2022 at 11:24):

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

perhaps try 64-bit? (run ./etc/toolchain-setup.sh --64 before building and notice that the switch will be jscoq+64bit)

Also which of the makes failed? (jscoq or wacoq?)
Also the worker is included in the jscoq/wacoq targets so you should not have to build it separately, these targets are for quick builds without rebuilding the coq-pkgs.

I think it is time to coordinate with Emilio to have a joint hands-on session. Unfortunately he is in Equatorial Guinea right now. We should put some eyes on it when he gets back.

Shachar Itzhaky (Nov 24 2022 at 11:39):

Yep. Got the error on a clean build at 32-bit. I wonder how this regression did not appear in our CI.

Shachar Itzhaky (Nov 24 2022 at 11:41):

you can freely comment out run make libs-symb because this is related to autocomplete (which will soon be handled by coq-lsp anyway)

Enrico Tassi (Nov 24 2022 at 12:53):

Shachar Itzhaky (Nov 24 2022 at 14:47):

Shachar Itzhaky (Nov 24 2022 at 14:53):

nope, same error in the 64-bit version. so weird! I don't remember ever seeing this but now it happens consistently. Perhaps a regression in jsoo...

Shachar Itzhaky (Nov 24 2022 at 14:56):

Shachar Itzhaky (Nov 24 2022 at 14:57):

we need to investigate the cause and send a fix. The Marshal may have gotten borked

Enrico Tassi (Nov 24 2022 at 14:58):

Enrico Tassi (Nov 24 2022 at 20:36):

Yes, I could compile it, but the npm package is lacking the WA backend.
Which make target should I invoke to get a jscoq.tgz with wa backend inside?

Shachar Itzhaky (Nov 24 2022 at 21:15):

did you run make wacoq? then I think make dist-npm should create a package with both

Enrico Tassi (Nov 25 2022 at 22:14):

Thanks for all your hints, I managed to get 8.16 run. This is how I made the lib.zip file:

cd $OPAM_SWITCH_PREFIX/lib
(for p in `ocamlfind query elpi -r -format '%+m %+a' -predicates byte`; do echo ${p##$OPAM_SWITCH_PREFIX/lib/}; done) | xargs zip ../../../lib.zip
echo coq-elpi/META coq-elpi/elpi_plugin.cma | xargs zip ../../../lib.zip
echo coq-core/META coq-core/plugins/*/*.cma | xargs zip ../../../lib.zip
echo findlib/META findlib/*.cma | xargs zip ../../../lib.zip
echo zarith/META zarith/*.cma | xargs zip ../../../lib.zip
sed -i.bak '/directory/d' threads/META str/META dynlink/META
cp ocaml/threads/threads.cma threads
cp ocaml/dynlink.cma dynlink
cp ocaml/str.cma str
echo seq/META | xargs zip ../../../lib.zip
echo threads/META threads/*.cma | xargs zip ../../../lib.zip
echo str/META str/*.cma | xargs zip ../../../lib.zip
echo dynlink/META dynlink/*.cma | xargs zip ../../../lib.zip
cd -

There is a clear packaging problem, this lib.zip is orthogonal to packages (two packages may need the same lib) so one should really build it given the list of packages one wants. This is not unlike platform installers, where the files in the opam root are cherry picked.
I won't have time to base my script on just opam before next year, in the meanwhile: https://github.com/gares/wacoq-setup

Shachar Itzhaky (Nov 25 2022 at 22:20):

cool! I wonder why so many things are needed that are not returned by opam query. Or perhaps these are required by the plugin, not the lib?

Enrico Tassi (Nov 25 2022 at 22:23):

Enrico Tassi (Nov 25 2022 at 22:24):

Shachar Itzhaky (Nov 25 2022 at 22:53):

ok I see that for Coq I only needed the META files, same for str, threads, unix, zarith (which are Coq deps). My guess is when the module has already been loaded by Coq, findlib will not look for the cma.

Shachar Itzhaky (Nov 25 2022 at 22:59):

 ocamlfind query coq-elpi.elpi -r -predicates byte -format '%+m %+a'

and package all the META files but whitelist cma files that are linked to the wacoq executable.

Stream: jsCoq

Topic: Elpi and HB

Enrico Tassi (Nov 03 2022 at 15:06):

Emilio Jesús Gallego Arias (Nov 03 2022 at 18:01):

Emilio Jesús Gallego Arias (Nov 03 2022 at 18:06):

Enrico Tassi (Nov 03 2022 at 20:11):

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:46):

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:51):

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:53):

Emilio Jesús Gallego Arias (Nov 03 2022 at 21:53):

Enrico Tassi (Nov 04 2022 at 06:56):

Enrico Tassi (Nov 04 2022 at 06:57):

Enrico Tassi (Nov 04 2022 at 07:56):

Emilio Jesús Gallego Arias (Nov 04 2022 at 11:25):

Emilio Jesús Gallego Arias (Nov 04 2022 at 11:26):

Enrico Tassi (Nov 04 2022 at 12:14):

Emilio Jesús Gallego Arias (Nov 04 2022 at 15:08):

Enrico Tassi (Nov 04 2022 at 16:38):

Emilio Jesús Gallego Arias (Nov 04 2022 at 19:57):

Emilio Jesús Gallego Arias (Nov 04 2022 at 19:57):

Shachar Itzhaky (Nov 06 2022 at 11:07):

Enrico Tassi (Nov 07 2022 at 10:32):

Shachar Itzhaky (Nov 07 2022 at 10:41):

Enrico Tassi (Nov 07 2022 at 10:53):

Shachar Itzhaky (Nov 07 2022 at 10:57):

Shachar Itzhaky (Nov 07 2022 at 10:57):

Enrico Tassi (Nov 07 2022 at 12:00):

Enrico Tassi (Nov 07 2022 at 12:00):

Enrico Tassi (Nov 07 2022 at 12:03):

Shachar Itzhaky (Nov 07 2022 at 12:06):

Shachar Itzhaky (Nov 07 2022 at 12:08):

Shachar Itzhaky (Nov 07 2022 at 12:08):

Enrico Tassi (Nov 07 2022 at 12:10):

Shachar Itzhaky (Nov 07 2022 at 12:11):

Shachar Itzhaky (Nov 07 2022 at 12:11):

Enrico Tassi (Nov 07 2022 at 12:28):

Shachar Itzhaky (Nov 07 2022 at 14:31):

Shachar Itzhaky (Nov 07 2022 at 14:35):

Enrico Tassi (Nov 07 2022 at 14:58):

Shachar Itzhaky (Nov 07 2022 at 14:59):

Shachar Itzhaky (Nov 07 2022 at 14:59):

Enrico Tassi (Nov 07 2022 at 15:04):

Enrico Tassi (Nov 07 2022 at 15:05):

Shachar Itzhaky (Nov 07 2022 at 15:06):

Enrico Tassi (Nov 07 2022 at 15:07):

Enrico Tassi (Nov 07 2022 at 15:08):

Shachar Itzhaky (Nov 07 2022 at 15:08):

Enrico Tassi (Nov 07 2022 at 15:09):

Shachar Itzhaky (Nov 07 2022 at 15:09):

Shachar Itzhaky (Nov 07 2022 at 15:09):

Enrico Tassi (Nov 07 2022 at 15:10):

Enrico Tassi (Nov 07 2022 at 15:12):

Shachar Itzhaky (Nov 07 2022 at 15:12):

Shachar Itzhaky (Nov 07 2022 at 15:13):

Enrico Tassi (Nov 07 2022 at 15:16):

Enrico Tassi (Nov 07 2022 at 15:16):

Enrico Tassi (Nov 07 2022 at 15:18):

Enrico Tassi (Nov 07 2022 at 15:21):

Emilio Jesús Gallego Arias (Nov 07 2022 at 15:58):

Shachar Itzhaky (Nov 07 2022 at 15:59):

Shachar Itzhaky (Nov 07 2022 at 15:59):

Shachar Itzhaky (Nov 07 2022 at 16:00):

Shachar Itzhaky (Nov 07 2022 at 16:00):

Shachar Itzhaky (Nov 07 2022 at 16:01):

Enrico Tassi (Nov 08 2022 at 09:36):

Enrico Tassi (Nov 08 2022 at 09:36):

Enrico Tassi (Nov 08 2022 at 10:19):

Enrico Tassi (Nov 08 2022 at 10:20):

Shachar Itzhaky (Nov 08 2022 at 10:46):

Enrico Tassi (Nov 08 2022 at 10:50):

Shachar Itzhaky (Nov 08 2022 at 10:56):

Shachar Itzhaky (Nov 08 2022 at 10:57):

Shachar Itzhaky (Nov 08 2022 at 10:58):

Enrico Tassi (Nov 08 2022 at 11:43):

Enrico Tassi (Nov 08 2022 at 11:44):

Enrico Tassi (Nov 08 2022 at 11:45):

Shachar Itzhaky (Nov 08 2022 at 11:56):

Shachar Itzhaky (Nov 08 2022 at 11:57):

Enrico Tassi (Nov 08 2022 at 12:22):

Shachar Itzhaky (Nov 08 2022 at 12:23):