Stream: jsCoq

Topic: Yet another SF preview


view this post on Zulip Shachar Itzhaky (Jan 09 2021 at 10:32):

Hi guys!

I have put up another version of SF (LF+PLF) at https://jscoq.github.io/ext/sf, this time base on waCoq because the JS version was throwing "Stack overflow"s for some big nat values. You are most welcome to try it!

It is the Aug 2020 version, once the 2021 edits have stabilized I will update it to reflect the most recent edition.
(Right now waCoq does not work on Safari due to some partial implementation of WebAssembly, will have to find a workaround.)

view this post on Zulip Pierre Courtieu (Feb 12 2021 at 08:06):

works very well.
Does it produce the grades :-)?

view this post on Zulip Shachar Itzhaky (Mar 03 2021 at 19:29):

Hi! Sorry for going missing, I definitely had plans to also run the grader in the browser -- it requires some porting because it uses Unix features, but definitely looks doable!

view this post on Zulip grianneau (Jul 18 2023 at 07:40):

Hei, how can I modify this project to serve a modified version? (and also offer to use the page offline)
I'm asking, because I follow SF with SSReflect tactics.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2023 at 09:44):

Hi @grianneau , the regular build instructions are in https://github.com/jscoq/jscoq/blob/v8.17/docs/build.md

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2023 at 09:46):

Tho it is a good idea to have a look at what the CI system does

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2023 at 09:46):

If you only need to serve updated .v / .vo files you can use the jsCoq SDK from npm https://github.com/jscoq/jscoq/blob/v8.17/docs/authoring.md

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2023 at 09:46):

Let us know of any problem

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2023 at 09:52):

Shachar and I are working on the documentation, hopefully we can improve it a bit.

view this post on Zulip grianneau (Jul 24 2023 at 13:28):

Thank you for the link to the version 8.17, I was using the 8.16 one. I can hardly see a difference now tho.
I can successfully run the commands ./etc/toolchain-setup.sh or ./etc/toolchain-setup.sh --64 and then make coq.
However, make jscoq seems to fail on my machine for both 32bit and 64bit. In both case the index.html has the three dots (on the right of the Coq logo) loading forever. With 64bit I get the error: missing primitives ml_z_extract_small.
I have no clue yet about:

view this post on Zulip grianneau (Aug 10 2023 at 08:39):

Emilio Jesús Gallego Arias said:

Tho it is a good idea to have a look at what the CI system does

I see this:
Screenshot-from-2023-08-10-10-33-24.png
I'm at the right place to look at the jsCoq CI status, amn't I?

view this post on Zulip Emilio Jesús Gallego Arias (Aug 10 2023 at 10:07):

That's a great question @grianneau , we mean to look at the CI file that builds jsCoq in the CI.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 10 2023 at 10:09):

We should amend the Readme

view this post on Zulip Shachar Itzhaky (Aug 10 2023 at 12:16):

@grianneau I believe that Emilio was suggesting that you look at the definition of the CI action.
In Github, the actions are configured via YAML files in .github/workflows.
https://github.com/jscoq/jscoq/blob/v8.17%2Blsp/.github/workflows/ci.yml

view this post on Zulip grianneau (Aug 14 2023 at 07:10):

Thank you for your answers. It is nice to have this reference working build from the CI! Locally, I get versions of opam dependencies that are different from the CI. By forcing the same versions, it removes some errors when building jsCoq. However I'm still stuck with this error:

SyntaxError: Unexpected token '?'
    at wrapSafe (internal/modules/cjs/loader.js:915:16)
    at Module._compile (internal/modules/cjs/loader.js:963:27)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:1027:10)
    at Module.load (internal/modules/cjs/loader.js:863:32)
    at Function.Module._load (internal/modules/cjs/loader.js:708:14)
    at Function.executeUserEntryPoint [as runMain] (internal/modules/run_main.js:60:12)
    at internal/main/run_main_module.js:17:47
make: *** [Makefile:86: jscoq] Error 1

I wonder whether someone encountered a similar problem. Before arriving there, I manually set the COQBUILDDIR_REL variable in the dune file, from the value ???? to _vendor+v8.16+32bit/coq.

Edit: maybe I'm using a wrong version of node.

view this post on Zulip grianneau (Aug 14 2023 at 08:49):

It looks like all my local versions are the same as in the working CI, however I get this npm error:

error path /home/grianneau/Documents/repositories/jscoq32/_build/.sandbox/43c78b1bf4063419a56f67fabcda7ab2/jscoq+32bit/node_modules/@koush/wrtc
error command failed
error command sh -c node scripts/download-prebuilt-or-build-from-source.js

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 11:00):

Oh awkward, this package is really only needed for the p2p addon, I am not sure why it should fail to install on your machine though. There are platform specific binaries there, possibly they are not available for your platform and node version?

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 11:01):

is there an error in addition to command failed? Perhaps try npm i in the project root to get a better report

view this post on Zulip grianneau (Aug 14 2023 at 11:16):

Thank you for your message. I don't see any other error.
I can run npm install -g node-pre-gyp but npm install wrtc fails with:

npm ERR! code 1
npm ERR! path /home/grianneau/Documents/repositories/jscoq32/node_modules/@koush/wrtc
npm ERR! command failed
npm ERR! command sh -c -- node scripts/download-prebuilt-or-build-from-source.js

npm ERR! A complete log of this run can be found in:
npm ERR!     /home/grianneau/.npm/_logs/2023-08-14T11_11_26_971Z-debug-0.log

I don't know whether it's related to my starting issue.

The command npm i results in:

npm WARN deprecated uuid@3.4.0: Please upgrade  to version 7 or higher.  Older versions may use Math.random() in certain circumstances, which is known to be problematic.  See https://v8.dev/blog/math-random for details.
npm WARN deprecated vue-context@6.0.0: No longer maintained
npm ERR! code 1
npm ERR! path /home/grianneau/Documents/repositories/jscoq32/node_modules/@koush/wrtc
npm ERR! command failed
npm ERR! command sh -c -- node scripts/download-prebuilt-or-build-from-source.js

npm ERR! A complete log of this run can be found in:
npm ERR!     /home/grianneau/.npm/_logs/2023-08-14T11_11_26_971Z-debug-0.log

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 11:41):

Umm perhaps you can cd node_modules/@koush/wrtc ; node scripts/download-prebuilt-or-build-from-source.js?

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 11:43):

anyway try removing ronin-p2p from package.json. The collab plugin may fail to build, but you will at least have the worker.

view this post on Zulip grianneau (Aug 14 2023 at 12:12):

I realise I have no node_modules directory...

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 12:15):

oh it is probably in _build/jscoq+32bit sorry

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 12:15):

you can run npm i if you want it in your source dir as well

view this post on Zulip grianneau (Aug 14 2023 at 12:19):

I'm not sure what the source directory is. I runned npm i in the project directory jscoq32. There is no node_modules in this project.

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 12:20):

wait what
but jscoq32 does contain package.json? this is definitely where npm is supposed to place it... also the path from the error message indicates so

view this post on Zulip grianneau (Aug 14 2023 at 12:22):

Yes I have package.json and I could find ronin-p2p in it.

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 12:23):

ok try to remove it. there would be some errors later on but let's see that it works up to that point.

view this post on Zulip grianneau (Aug 14 2023 at 12:24):

I think I understand why. I forgot to run the command ./etc/toolchain-setup.sh (this time). When I run it it forces changes in the opam dependencies...

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 12:24):

hmm interesting although I see no connection between the opam dependencies and the npm ones

view this post on Zulip grianneau (Aug 14 2023 at 12:26):

Once I run ./etc/toolchain-setup.sh and setup opam dependencies, I don't need to rerun it after make clean, right?

view this post on Zulip grianneau (Aug 14 2023 at 12:28):

Well I see only opam installations in the script ./etc/toolchain-setup.sh.

view this post on Zulip Shachar Itzhaky (Aug 14 2023 at 12:47):

right

view this post on Zulip grianneau (Aug 15 2023 at 07:37):

Shachar Itzhaky said:

anyway try removing ronin-p2p from package.json. The collab plugin may fail to build, but you will at least have the worker.

I tried this, it seems the worker is built despite build errors, but in the webpage the worker loads forever. I get error messages after opening the served page:

[2023-08-15T07:25:46.978Z]  "GET /examples/examples.symb.json" Error (404): "Not found"
...
[2023-08-15T07:25:47.000Z]  "GET /coq-pkgs/coq.json" Error (404): "Not found"
[2023-08-15T07:25:47.000Z]  "GET /node_modules/@jscoq/mathcomp/coq-pkgs/mathcomp.json" Error (404): "Not found"
[2023-08-15T07:25:47.000Z]  "GET /node_modules/@jscoq/equations/coq-pkgs/equations.json" Error (404): "Not found"
[2023-08-15T07:25:47.000Z]  "GET /node_modules/@jscoq/elpi/coq-pkgs/elpi.json" Error (404): "Not found"
[2023-08-15T07:25:47.000Z]  "GET /node_modules/@jscoq/quickchick/coq-pkgs/quickchick.json" Error (404): "Not found"
...
[2023-08-15T07:25:47.008Z]  "GET /node_modules/@jscoq/software-foundations/coq-pkgs/software-foundations.json" Error (404): "Not found"
[2023-08-15T07:25:47.010Z]  "GET /node_modules/@jscoq/hahn/coq-pkgs/hahn.json" Error (404): "Not found"
[2023-08-15T07:25:47.010Z]  "GET /node_modules/@jscoq/paco/coq-pkgs/paco.json" Error (404): "Not found"
[2023-08-15T07:25:47.011Z]  "GET /node_modules/@jscoq/snu-sflib/coq-pkgs/snu-sflib.json" Error (404): "Not found"
[2023-08-15T07:25:47.012Z]  "GET /node_modules/@jscoq/fcsl-pcm/coq-pkgs/fcsl-pcm.json" Error (404): "Not found"
...
[2023-08-15T07:25:47.031Z]  "GET /node_modules/@jscoq/htt/coq-pkgs/htt.json" Error (404): "Not found"
[2023-08-15T07:25:47.032Z]  "GET /node_modules/@jscoq/pnp/coq-pkgs/pnp.json" Error (404): "Not found"
[2023-08-15T07:25:47.032Z]  "GET /node_modules/@jscoq/stdpp/coq-pkgs/stdpp.json" Error (404): "Not found"
[2023-08-15T07:25:47.032Z]  "GET /node_modules/@jscoq/iris/coq-pkgs/iris.json" Error (404): "Not found"
[2023-08-15T07:25:47.032Z]  "GET /examples/examples.json" Error (404): "Not found"
...
[2023-08-15T07:25:47.040Z]  "GET /coq-pkgs//init.symb.json" Error (404): "Not found"
[2023-08-15T07:25:47.040Z]  "GET /coq-pkgs//coq-base.symb.json" Error (404): "Not found"
...
[2023-08-15T07:25:47.042Z]  "GET /coq-pkgs//coq-collections.symb.json" Error (404): "Not found"
[2023-08-15T07:25:47.042Z]  "GET /coq-pkgs//coq-arith.symb.json" Error (404): "Not found"
[2023-08-15T07:25:47.043Z]  "GET /coq-pkgs//coq-reals.symb.json" Error (404): "Not found"

view this post on Zulip grianneau (Aug 15 2023 at 08:04):

I use node version 16.20.1 and npm version 8.19.4 as in the CI.

view this post on Zulip grianneau (Aug 15 2023 at 08:25):

npm does not create the folder node_modules. I don't get more information with the verbose option.

view this post on Zulip grianneau (Aug 15 2023 at 08:32):

npm i passes with no error without the package ronin-p2p, so it is the culprit.

view this post on Zulip grianneau (Aug 15 2023 at 08:42):

There is something strange (maybe) when I do npm view package versions: there is only 0.1.0 for ronin-p2p while there are plenty of versions for other packages.

view this post on Zulip grianneau (Aug 15 2023 at 11:54):

I've tried to build the version 8.17 and I get the error: Error: Library "coq-lsp.fleche" not found (and then the same npm error as before).

view this post on Zulip grianneau (Aug 16 2023 at 12:00):

I can reproduce this build error on another machine, for both branches 8.17+lsp (the default branch) and 8.17:

File "backend/common/dune", line 10, characters 3-17:
10 |    coq-lsp.fleche))
        ^^^^^^^^^^^^^^
Error: Library "coq-lsp.fleche" not found.
-> required by library "jscoq_core" in _build/jscoq+32bit/backend/common
-> required by executable jscoq_worker in backend/jsoo/dune:2
-> required by _build/jscoq+32bit/backend/jsoo/jscoq_worker.bc.js
-> required by alias jscoq (context jscoq+32bit) in dune:41
Done: 27% (1866/6846, 4980 left, 1 failed) (jobs: 1)debug2: channel 0: window 999401 sent adjust 49175
Done: 30% (2909/9594, 6685 left, 1 failed) (jobs: 1)npm WARN deprecated uuid@3.4.0: Please upgrade  to version 7 or higher.  Older versions may use Math.random() in certain circumstances, which is known to be problematic.  See https://v8.dev/blog/math-random for details.
Done: 30% (2909/9594, 6685 left, 1 failed) (jobs: 1)npm WARN deprecated vue-context@6.0.0: No longer maintained
Done: 33% (3472/10509, 7037 left, 1 failed) (jobs: 1)debug2: channel 0: window 1998732 sent adjust 98420
Done: 33% (3472/10509, 7037 left, 1 failed) (jobs: 1)npm ERR! code 1
npm ERR! path /home/ubuntu/test_jsCoq_build/jscoq/_build/jscoq+32bit/node_modules/@koush/wrtc
Done: 33% (3472/10509, 7037 left, 1 failed) (jobs: 1)npm ERR! command failed
npm ERR! command sh -c node scripts/download-prebuilt-or-build-from-source.js

npm ERR! A complete log of this run can be found in: /home/ubuntu/.npm/_logs/2023-08-16T11_42_58_781Z-debug-0.log

I can see that the CI (github workflow) passes for these branches. What should I pay attention to when trying to imitate a successful build that happens on the CI?

view this post on Zulip Shachar Itzhaky (Aug 18 2023 at 13:13):

I think what happened to you above is that the worker was indeed built but the packages were not, because the packages depend on the CLI and there was some error with building the CLI - even though the CLI should not depend on ronin-p2p.

view this post on Zulip Shachar Itzhaky (Aug 18 2023 at 13:14):

it is very hard to figure out what went wrong without somehow catching the error from download-prebuilt. can you somehow find it in your build tree and run it in the terminal?

view this post on Zulip grianneau (Aug 21 2023 at 13:53):

Shachar Itzhaky said:

I think what happened to you above is that the worker was indeed built but the packages were not, because the packages depend on the CLI and there was some error with building the CLI - even though the CLI should not depend on ronin-p2p.

I'm sorry but I don't understand this message and the next one about download-prebuilt. I feel like I encounter a problem that is related to node and maybe not to the build of jscoq, right?

view this post on Zulip Shachar Itzhaky (Aug 21 2023 at 13:56):

you are correct in general. The problem is this unmaintained package @koush/wrtc, which for some reason fails to install on your build machine. That aside, this dependency is only needed for the "collab" addon (collaborative editing), so the fact that a build of a separate component (jsCoq CLI) fails indicates some dependency mayhem in jsCoq's source code.

view this post on Zulip grianneau (Aug 21 2023 at 14:20):

After removing ronin-p2p from the file package.json, I see no error with the command make jscoq. However the jsCoq worker fails to start (inside the webpage).


Last updated: Oct 01 2023 at 19:01 UTC