Stream: jsCoq

Topic: Elpi and HB


view this post on Zulip Enrico Tassi (Nov 03 2022 at 15:06):

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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

The wa backend can be found at https://coq.vercel.app/wa/scratchpad.html , tho in the current 8.16 branch you just pass ?backend=wa to the URL.

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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2022 at 21:51):

The plugin loader is here https://github.com/jscoq/jscoq/blob/v8.16/backend/jsoo/jscoq_worker.ml#L127 , for the wasm backend is just nothing, it is just missing the filesystem files. Shachar will correct me if I'm wrong but we'd basically need to tar.gz the required files for elpi

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2022 at 21:53):

and be an easier patch

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 04 2022 at 06:57):

Also, is wacoq faster? if so I'd prefer that one since we do have perf problems

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2022 at 11:26):

yes doing a quick call would be much more efficient

view this post on Zulip Enrico Tassi (Nov 04 2022 at 12:14):

I'm quite free, I let you pick a time that fits

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2022 at 15:08):

@Enrico Tassi what versions do you need things to work?

view this post on Zulip Enrico Tassi (Nov 04 2022 at 16:38):

8.15 or 8.16, actually anything we use here https://github.com/math-comp/math-comp/pull/733/files#diff-a4e04df48252cabe60d40e7d9b7417d7c5f9259e81e4be5e86f18430a22d011a
preferably 8.16 + HB 1.4 (coq-elpi 1.16.x), but even 8.15 + HB 1.4 (coq-elpi 1.14.x) would do.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2022 at 19:57):

https://www.npmjs.com/package/@wacoq/elpi/v/0.15.1

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 07 2022 at 10:53):

Oh I see, I'll check that one then

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 10:57):

it's here, nothing to smart there https://github.com/jscoq/addon-mathcomp-extra/blob/v8.16/Makefile

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 10:57):

perhaps I can replace my build commands with yours

view this post on Zulip Enrico Tassi (Nov 07 2022 at 12:00):

Now I have the 3 tgz I need, but the build instructions are a bit terse:

This creates .tgz files for packages in _build/jscoq+32bit (or +64bit). You can then npm install them in your jsCoq distribution.

What should I do with the .tgz?

view this post on Zulip Enrico Tassi (Nov 07 2022 at 12:00):

(I'm not an npm expert)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 12:08):

(pls read about npm link for more info on how to use)

view this post on Zulip Enrico Tassi (Nov 07 2022 at 12:10):

from where should I run npm i ...tgz

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 12:11):

yeah sry I missed that bit in my msg, I have updated :)

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 12:11):

it should be in the jsCoq project root

view this post on Zulip Enrico Tassi (Nov 07 2022 at 12:28):

Hum, I think I still miss a step, since

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

but make jscoq says:

       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]

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Enrico Tassi (Nov 07 2022 at 14:58):

Shachar Itzhaky said:

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.

Yes, isn't it what find finds?

view this post on Zulip 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?

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 14:59):

though it should depend on package.json which has changed so it's weird

view this post on Zulip Enrico Tassi (Nov 07 2022 at 15:04):

So I confirm package.json was updated (I see the tgz as dependencies).
Then

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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 15:06):

does hierarchy-builder appear in package.json? send me the file :)

view this post on Zulip 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",

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Nov 07 2022 at 15:09):

ok, I'll try with absolute paths

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 15:09):

try the serve-from-source-dir path

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 15:09):

Enrico Tassi said:

ok, I'll try with absolute paths

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

view this post on Zulip Enrico Tassi (Nov 07 2022 at 15:10):

nope, did not help

view this post on Zulip Enrico Tassi (Nov 07 2022 at 15:12):

if I rm _build/.../coq-pkgs and make jscoq I still see

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Nov 07 2022 at 15:16):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2022 at 15:58):

for the ?backend=wa thing you need the bleeding edge branch

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 15:59):

(and also you need wasi-sdk in order to build it)

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 16:00):

Enrico Tassi said:

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

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.

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 07 2022 at 16:01):

oh actually it's 8.15 so there's no findlib issue

view this post on Zulip Enrico Tassi (Nov 08 2022 at 09:36):

One hint is that I also get:

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

Indeed coq-elpi setup:
https://github.com/LPCIC/coq-elpi/blob/afc9b5aebdd4c44be4891723934ed9435a92df85/src/coq_elpi_vernacular.ml#L251
calls Boot.Env.init
https://github.com/LPCIC/coq-elpi/blob/afc9b5aebdd4c44be4891723934ed9435a92df85/src/coq_elpi_vernacular.ml#L226
which may call exit
https://github.com/coq/coq/blob/a0a9a522a1b4bd880748502f13f324c0aa20d82e/boot/env.ml#L56
https://github.com/coq/coq/blob/a0a9a522a1b4bd880748502f13f324c0aa20d82e/boot/env.ml#L33

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 08 2022 at 10:19):

OK, I managed to load elpi by applying this diff
elpi-jscoq.diff

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 10:46):

nice!

view this post on Zulip 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?

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 10:56):

what are your config options? (in the call to JsCoq.start)

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 10:57):

Enrico Tassi said:

OK, I managed to load elpi by applying this diff
elpi-jscoq.diff

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

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 10:58):

lol https://github.com/jscoq/addon-elpi/blob/e124466146005acc7010706da66da411e83eb1d8/Makefile#L14

view this post on Zulip Enrico Tassi (Nov 08 2022 at 11:43):

I'm just opening index.html, I did add hierarchy-builder there.

view this post on Zulip 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...

view this post on Zulip 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'],

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 11:56):

yes, + is the default coq-pkgs dir.

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Nov 08 2022 at 12:22):

thanks, but how is it that elpi is found anyway?

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 12:23):

oh funny you should ask :)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 08 2022 at 12:55):

Other question: I do have many stack overflows. Does wacoq handle these better?

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 14:17):

great!

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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:

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 14:27):

(oops nice try me, it doesn't have it either)

view this post on Zulip Enrico Tassi (Nov 08 2022 at 14:27):

And what about stack overflows and WA?

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 08 2022 at 14:30):

for referencing other packages for the purpose of coqdep, see example in Iris:
https://github.com/jscoq/addon-iris/blob/iris-4.0.0-coq-8.16/dune

view this post on Zulip Enrico Tassi (Nov 09 2022 at 09:19):

OK thanks, I'm following the instructions for wacoq-bin

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 12:29):

yes we are going to get rid of the wacoqdoc

view this post on Zulip Enrico Tassi (Nov 09 2022 at 13:03):

is there a way around this I can apply myself?

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 13:18):

yeah don't run it :) do you need to create a coqdoc-style document?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 09 2022 at 13:20):

How am I supposed to build the addons for wacoq?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 13:23):

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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 09 2022 at 13:29):

npm link did the trick

view this post on Zulip Enrico Tassi (Nov 09 2022 at 13:29):

I'm really clueless... indeed I could not get how npx was finding any wacoq...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 13:39):

ok hmm

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 13:41):

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

view this post on Zulip 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...

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 13:42):

we should clean up this mess quickly and move on

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 09 2022 at 13:49):

rememeber I'm on v8.15

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 13:59):

yeah so add backend: 'wa' to your jscoq_options

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 14:13):

hmm perhaps I'm wrong? pretty sure this was available in 8.15 already

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 17:08):

are you now serving from source dir with make links? or still from bin dir?

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 17:08):

in fact for wacoq you don't even need the links

view this post on Zulip 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-ad658677d7d:2:316836)
    at z._fetch (93ead2eb-ac7a-45ff-ad658677d7d:2:316671)
    at $.upload (93ead2eb-ac7a-45ff-ad658677d7d:2:314254)
    at $.boot (93ead2eb-ac7a-45ff-ad658677d7d:2:314094)
    at J (93ead2eb-ac7a-45ff-ad658677d7d:2:317409)
    at 93ead2eb-ac7a-45ff-ad658677d7d:2:317456
    at 93ead2eb-ac7a-45ff-ad658677d7d:2:317489
    at 93ead2eb-ac7a-45ff-ad658677d7d:2:317493

does this ring a bell?

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:08):

hmm

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:09):

well the url looks wrong but why is it using this ../bin/icoq.bc

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:09):

it should be using an absolute url

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:12):

What browser you are using?

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:12):

ah no actually t's using a relative url but this used to work for sure

view this post on Zulip 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:

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:18):

should it though? because now elpi is not linked with -linkall

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:18):

I mean -linkall wouldn't work with 8.16 right?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:23):

Yes, it would work when using the legacy loading

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:24):

The problem with linkall was due to diamonds

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:26):

umm but then would it not link Coq as well..?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:27):

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:28):

so the list is manual I think

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:28):

yeah so I used to have this crazy hack: https://github.com/jscoq/addon-elpi/blob/30c74a194ef58c1dcf605b17f319499145c7860d/dune-files/src/dune#L35

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:28):

what I meant is that the deps of elpi for example, will be up to date

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:28):

I think if we do -linkall + wacoq, it would be needed still

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:28):

this is exactly what coq_makefile already does

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:29):

I think

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:29):

[didn't check the details]

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:29):

ah so the only problem was my insistence on building it with dune

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:31):

tho in 8.16 wacoq, what's the problem in making findlib work?

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:31):

ah now it would work, this was only needed for the -linkall route.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:32):

we can do the tar.gz for now with find + tar

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:32):

I see

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:33):

For Enrico's needs we could just do the tar.gz "manually" for now

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:33):

it'd be nice of course to do more granular stuff

view this post on Zulip Shachar Itzhaky (Nov 09 2022 at 21:33):

pkg-elpi.js
here is the script :) no warranty

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:39):

maybe it is on the fleche branch?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2022 at 21:39):

I think I saw it too

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 10 2022 at 09:10):

It looks like the ../bin/icoq.bc comes from core.ts in wacoq-bin

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

view this post on Zulip Enrico Tassi (Nov 10 2022 at 09:11):

@Shachar Itzhaky ideas?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 09:37):

compare with the master version of core.ts in wacoq-bin

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:03):

let me see the diff, not sure I'm good enough to do the port myself...

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:09):

here the error, I missed it:

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

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:09):

I think I mixed and matched two ocaml switches

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:14):

and the wacoq one is 64 bits

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:15):

which is the best way to compile "jscoq" using the wacoq switch?

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:15):

I think I have wacoq-bin and the packages built using the wacoq switch

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:16):

so I just need to build jscoq, I guess

view this post on Zulip Enrico Tassi (Nov 10 2022 at 10:47):

I see, this ocaml-wasm thing comes with 4.12

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 10:51):

64-bit is fine but the wacoq switch has to be 4.12 yes

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 14:36):

8.16 has unified the backends so if you need to make wacoq run I find it easier

view this post on Zulip Enrico Tassi (Nov 10 2022 at 15:13):

I recompiled everything but I still get an error which is weird:

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

view this post on Zulip 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.

view this post on Zulip 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']}

so something is still off

view this post on Zulip Enrico Tassi (Nov 10 2022 at 15:20):

this time I'm just doing

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

I hope it is fine (and I edited the index.html in there)

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 15:20):

yes but did you run make install in wacoq-bin?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 10 2022 at 15:22):

where does this come from?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:02):

likely from 8.15 , if you are still in that version

view this post on Zulip Enrico Tassi (Nov 10 2022 at 16:05):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:11):

Can you try quick to see if you can build wacoq in 8.16 ?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 10 2022 at 16:12):

then we can just add the linkall to elpi

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 10 2022 at 16:17):

I did compile it, from the right branch, using a switch with 4.12

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Nov 10 2022 at 16:28):

no, the string is definitely not hardcoded

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 15:24):

That's the function you may want to look at first https://github.com/jscoq/jscoq/blob/v8.15/ui-js/coq-manager.js#L671

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 15:24):

likely for HB you are missing the file that contains the metadata

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 15:28):

you can just inspect the map in coq-packages.js

view this post on Zulip Enrico Tassi (Nov 14 2022 at 15:29):

anyway, I managed to make all packages load at init time, so the issue is gone

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 15:36):

I'm unsure what's killing \n

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 15:36):

Do you have an example to see?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 14 2022 at 20:02):

Can you tell me where it is?

view this post on Zulip Enrico Tassi (Nov 14 2022 at 20:03):

Emilio Jesús Gallego Arias said:

Do you have an example to see?

Take https://www-sop.inria.fr/teams/marelle/MC-2022/ and add HB.about Equality.type.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 20:15):

@Enrico Tassi nothing special is done by jsCoq

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 20:16):

the text (with the \n) is put inside a div

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 20:18):

in what class I'm unsure, maybe #query-panel .Notice

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2022 at 15:16):

Maybe, I'm unsure if Pp is too limited for us to actually guess that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 15 2022 at 15:16):

For Boxmodel we should indeed have a kind of pre tag

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 16 2022 at 12:20):

Are there known problems?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Nov 16 2022 at 12:46):

Boh, no, I think I'm lost... they are there... I'm puzzled

view this post on Zulip Shachar Itzhaky (Nov 16 2022 at 12:47):

hmm what happened that failed loading before you commented them

view this post on Zulip Enrico Tassi (Nov 16 2022 at 12:50):

dunno, I'm trying again to recompile everything

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 16:28):

@Enrico Tassi what is happening is that we build a patched math-comp

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 16:28):

You can just import them explicitly, or drop the patch

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 16:29):

https://github.com/ejgallego/math-comp/tree/fast-load

view this post on Zulip Emilio Jesús Gallego Arias (Nov 16 2022 at 16:29):

We should push this to upstream math-comp IMHO

view this post on Zulip Enrico Tassi (Nov 17 2022 at 22:11):

@Shachar Itzhaky is there a way to detect wacoq from ocaml? I could do this for jscoq https://github.com/LPCIC/coq-elpi/commit/aa3f4b47841e752292e4961cc742511035822ae4 but it does not work when coq is compiled to wa. Is there a way?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:01):

You can use a hack such as checking if the file /bin/icoq.bc exists

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:03):

The file is the bytecode runner indeed

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:08):

Unfortunately there is no other way that I know except this hack

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:08):

if you don't want to modify ocaml-wasm

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:08):

yeah depending on that is not good

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:08):

maybe there are some stub that you could use, but I'm not sure

view this post on Zulip Enrico Tassi (Nov 18 2022 at 13:09):

Another option would be to name the Boot module work there

view this post on Zulip Enrico Tassi (Nov 18 2022 at 13:09):

Actualy I don't get why it complains about not finding coqlib and then exit 1

view this post on Zulip Enrico Tassi (Nov 18 2022 at 13:09):

in both wa and js

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:23):

Oh, Boot is giving you trouble

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:23):

likely we are not setting coqlib properly

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:24):

actually jsCoq works in -noinit mode, which IMHO the right setting for that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 13:24):

but yeah for plugins using guess_coqlib that a pita

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 14:52):

Enrico Tassi said:

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

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

view this post on Zulip Enrico Tassi (Nov 18 2022 at 14:56):

Shachar Itzhaky said:

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

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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 18 2022 at 17:29):

Actually, it's code by Emilio https://github.com/LPCIC/coq-elpi/commit/ef79008a340392ec1b5e4a211b4db50755b04553

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 19:28):

It is just a renaming, Envars.coqlib behaved similarly, IIRC.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 19:32):

Oh, actually you are right, the change made the API stricter

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 19:32):

Before, if coqlib was not set, Envars.coqlib () returned ""

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 19:37):

There are still quite a few things wrong on how Boot.Env behaves

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 19:37):

and how it does try to locate the stdlib

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 19:39):

But it is fishy that this fails in jsCoq tho

view this post on Zulip Emilio Jesús Gallego Arias (Nov 18 2022 at 19:39):

well, not sure

view this post on Zulip Shachar Itzhaky (Nov 18 2022 at 19:41):

Well I guess checking for env var "COQLIB" explicitly would not be so bad?

view this post on Zulip Shachar Itzhaky (Nov 18 2022 at 19:41):

we can also set it to /lib in jsCoq

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Nov 18 2022 at 20:52):

actually looks like 8.16 is already doing that https://github.com/jscoq/jscoq/blob/2a60fd083b6b09cbe19f750f31a877740d140ea2/backend/wasm/ocaml_exec.ts#L40

view this post on Zulip Shachar Itzhaky (Nov 18 2022 at 20:52):

you can try to backport

view this post on Zulip 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/.

view this post on Zulip 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)

view this post on Zulip Shachar Itzhaky (Nov 23 2022 at 16:15):

oh yes let me diggitup

view this post on Zulip Shachar Itzhaky (Nov 23 2022 at 16:22):

Look here: https://github.com/jscoq/jscoq/blob/2a60fd083b6b09cbe19f750f31a877740d140ea2/backend/wasm/core.ts#L35

view this post on Zulip 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).

view this post on Zulip Shachar Itzhaky (Nov 23 2022 at 16:26):

ah also this envvar needs to be set https://github.com/jscoq/jscoq/blob/2a60fd083b6b09cbe19f750f31a877740d140ea2/backend/wasm/ocaml_exec.ts#L40
probably we should put the functionality either in IcoqPod or OCamlExecutable instead of this weird split.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 23 2022 at 21:20):

I'm using this fork of wacoq-bin, only one extra commit (you can take I guess): https://github.com/gares/wacoq-bin

view this post on Zulip Enrico Tassi (Nov 23 2022 at 21:21):

and for jscoq, I'm here https://github.com/gares/jscoq/tree/v8.16 which is 1 commit ahead of the tag for 8.16

view this post on Zulip 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

but I get:

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)

does this ring a bell? Am I calling the right targets to get an npm package?

view this post on Zulip Shachar Itzhaky (Nov 24 2022 at 11:24):

Assertion failure! something to do with marshal...

  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.

I will try 32-bit again. On Mac I am only using 64 because 32 is dead.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Nov 24 2022 at 12:53):

do you confirm that if I do a 64 build the problem will go away?

view this post on Zulip Shachar Itzhaky (Nov 24 2022 at 14:47):

I started a build from scratch earlier but did not finish, lemme see

view this post on Zulip 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...

view this post on Zulip Shachar Itzhaky (Nov 24 2022 at 14:56):

yup... it passes if you use js_of_ocaml.4.0.0 (instead of 4.1.0).

view this post on Zulip Shachar Itzhaky (Nov 24 2022 at 14:57):

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

view this post on Zulip Enrico Tassi (Nov 24 2022 at 14:58):

thanks, I'll try

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 25 2022 at 22:23):

Because it is not the plugin you should query
You should query also Coq

view this post on Zulip Enrico Tassi (Nov 25 2022 at 22:23):

Here I did things by hand, I should have used ocamlfind more

view this post on Zulip Enrico Tassi (Nov 25 2022 at 22:24):

But the query "roots" are coq plus all its plugins

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Nov 25 2022 at 22:59):

I suggest we use this command:

 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.


Last updated: Jan 31 2023 at 10:01 UTC