Stream: jsCoq

Topic: windows vs WSL


view this post on Zulip Darij Grinberg (Jul 06 2021 at 19:05):

Hi! Is there a good way to connect from a browser running on Windows to a local jscoq install on WSL2? or should I install jscoq on Windows natively?

view this post on Zulip Darij Grinberg (Jul 06 2021 at 19:06):

When I open examples/scratchpad.html, I see:
Failed to start jsCoq worker.
(Serving from local file;
has --allow-file-access-from-files been set?)

view this post on Zulip Michael Soegtrop (Jul 07 2021 at 07:15):

You should ask this question in the jsCoq stream.

Btw.: can I move something to a different stream?

view this post on Zulip Notification Bot (Jul 07 2021 at 08:07):

This topic was moved here from #Coq users > windows vs WSL by Théo Zimmermann

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 09:38):

@Darij Grinberg I'm not very familiar with windows, but maybe installing npm's http-server would work?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 09:38):

that's what I use on linux

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 09:39):

it's a very simple web server

view this post on Zulip Darij Grinberg (Jul 07 2021 at 11:41):

@Emilio Jesús Gallego Arias any more details? I don't think I've ever successfully installed a server...

view this post on Zulip Janno (Jul 07 2021 at 12:19):

If you have python3 installed you can use python3 -m http.server (which will serve the current directory on port 8000 by default).

view this post on Zulip Darij Grinberg (Jul 07 2021 at 13:34):

ok, what do I do next?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 13:34):

how do I connect? and which directory should I run this in?

view this post on Zulip Janno (Jul 07 2021 at 14:37):

I don't know enough about the current jscoq setup to say. I suppose in the parent directory of examples but that's just a guess. With that setup you should be able to open http://localhost:8000/examples/scratchpad.html and hopefully it will find all the required files.

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:50):

hmm

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:50):

i don't think it's working

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:51):

it definitely connects to the files, but scratchpad.html is empty, and in the other examples files the coq forms are not interactive

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:51):

and on the linux console, i'm getting stuff like this:

127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /ui-js/jscoq-loader.js HTTP/1.1" 200 -
127.0.0.1 - - [07/Jul/2021 16:48:53] code 404, message File not found
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /codemirror/lib/codemirror.css HTTP/1.1" 404 -
127.0.0.1 - - [07/Jul/2021 16:48:53] code 404, message File not found
127.0.0.1 - - [07/Jul/2021 16:48:53] code 404, message File not found
127.0.0.1 - - [07/Jul/2021 16:48:53] code 404, message File not found
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /codemirror/theme/blackboard.css HTTP/1.1" 404 -
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /codemirror/addon/hint/show-hint.css HTTP/1.1" 404 -
127.0.0.1 - - [07/Jul/2021 16:48:53] code 404, message File not found
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /codemirror/theme/darcula.css HTTP/1.1" 404 -
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /codemirror/addon/dialog/dialog.css HTTP/1.1" 404 -
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /ui-css/coq-log.css HTTP/1.1" 200 -
127.0.0.1 - - [07/Jul/2021 16:48:53] code 404, message File not found
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /codemirror/lib/codemirror.js HTTP/1.1" 404 -
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /ui-css/coq-light.css HTTP/1.1" 200 -
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /ui-css/settings.css HTTP/1.1" 200 -
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /ui-css/coq-dark.css HTTP/1.1" 200 -
127.0.0.1 - - [07/Jul/2021 16:48:53] "GET /ui-css/coq-base.css HTTP/1.1" 200 -

view this post on Zulip Janno (Jul 07 2021 at 14:52):

I haven't used jscoq in years so I am out of my depth here. Do the files that yield 404 errors exist (relative to the parent directory of examples)?

view this post on Zulip Janno (Jul 07 2021 at 14:53):

Maybe there is some git submodule for codemirror that hasn't been initialized?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:53):

ah right

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:53):

there is no /codemirror at all

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:53):

this is an npm install IIRC, so i don't see any traces of git in the directory

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 14:54):

oh sorry, I thought you had installed jscoq from npm

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:54):

i have

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 14:54):

ah you did? it should be there, but then you need to serve the install directory

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 14:54):

I am not familiar with the npm setup a lot, ccing @Shachar Itzhaky

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:54):

i'm serving node_modules/jscoq; is that wrong?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:54):

was "npm install jscoq" too simple?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 14:55):

Should work fine, but indeed I'm not sure what the right directory to point the web server is

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:55):

hmm

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:56):

ah!

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:56):

the entire node_modules needs to be served

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:56):

thank you! that wasn't very intuitive though :)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 14:57):

Glad it worked, please if you think we can improve the documentation don't hesitate to submit a PR / issue

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:57):

so now it's missing all packages:
Package 'init' is missing (http://localhost:8000/jscoq/coq-pkgs/init.json: not found (404))
Package 'mathcomp' is missing (http://localhost:8000/@jscoq/mathcomp/coq-pkgs/mathcomp.json: not found (404))
Package 'dsp' is missing (http://localhost:8000/jscoq/coq-pkgs/dsp.json: not found (404))

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:57):

do i need to compile them first?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 14:58):

or should i just ditch npm and install it from the repo?

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 15:20):

Hi. This definitely should work, since our website is built using the package from npm.
Did you try https://github.com/jscoq/jscoq/blob/v8.13/docs/embedding.md? (Actually I have updated this file today, but only the parts related to coqdoc.)

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:08):

@Shachar Itzhaky Ah, so I should browse to /jscoq/index.html.That looks better. Is there a way to check that it correctly imports packages?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:08):

Some simple code snippet?

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:08):

Try e.g. Require Import Lia.

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:09):

ah seems to work

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:09):

or not

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:09):

Cannot find a physical path bound to logical path matching
suffix <>.

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:09):

You can also copy the npm-landing.html to the root of your project and try there.

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:10):

Looks like it did not find the package files (coq.json etc.) after all :(

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:10):

this works:
Compute
let n := 33 : nat in
let e := n+n+n in
e+e+e.

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:10):

= 297 : nat

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:10):

so the "core", whatever it is, seems to be in place

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:11):

Oh so it found init but not arith? hmm

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:11):

did you get any warnings in the message area, on startup?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:11):

it actually spent some time loading parts of ssreflects from your command

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:11):

For Lia? :-s

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:11):

yeah

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:11):

maybe the error message was spurious
what's a way to check if it was successful?

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:12):

ok wait that's super strange. I'm trying to reproduce.

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:13):

these errors are rarely spurious. But you can try running the rest of the snippet (copy from here: https://coq-next.vercel.app/ci/diagnostics.html)

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:14):

you're right, it's not spurious

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:14):

do you have a few minutes to zoom?

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:14):

wait let me try to run the exact same commands. Doing npm i jscoq now.

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:15):

are you on WSL?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:15):

that might be causing file access issues

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:16):

no, but that should not matter in principle since you are not building it. Are you using http-server to serve the files?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:17):

python3 -m http.server in my node-modulesdirectory

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:17):

python 3.7.3, node v10.24.0, jscoq freshly installed yesterday or so

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:22):

It seemed to work on Linux. Let me try WSL now.

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:22):

On my local machine npm i jscoq hangs right now... is my home internet sluggish atm? :D

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:38):

@Darij Grinberg apart from coq.json, what is the content of the node_modules/jscoq/coq-pkgs directory?

view this post on Zulip Darij Grinberg (Jul 07 2021 at 17:42):

darij@moria:/mnt/d/dev/node_modules/jscoq/coq-pkgs$ ll
total 28068
drwxrwxrwx 1 darij darij 4096 Jul 6 20:58 .
drwxrwxrwx 1 darij darij 4096 Jul 6 20:58 ..
-rwxrwxrwx 1 darij darij 10528757 May 21 18:45 coq-arith.coq-pkg
-rwxrwxrwx 1 darij darij 2224820 May 21 18:45 coq-base.coq-pkg
-rwxrwxrwx 1 darij darij 9772640 May 21 18:45 coq-collections.coq-pkg
-rwxrwxrwx 1 darij darij 124012 May 21 18:45 coq.json
-rwxrwxrwx 1 darij darij 4963250 May 21 18:45 coq-reals.coq-pkg
-rwxrwxrwx 1 darij darij 1114758 May 21 18:44 init.coq-pkg

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 17:54):

that seems to be it.
Sorry I find that I am unable to offer useful information since I am trying for 20 minutes to complete a npm i jscoq and it just won't finish up.

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 18:01):

weirdly enough npm i wacoq does work :face_palm:

view this post on Zulip Darij Grinberg (Jul 07 2021 at 18:07):

that seems to be it.
meaning the installer has failed to download all files?

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 18:08):

No, I meant that these are the files that should be there.

view this post on Zulip Darij Grinberg (Jul 07 2021 at 18:08):

ah

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 18:08):

I have no idea what's going on. I am running wget 'https://registry.npmjs.org/jscoq/-/jscoq-0.13.0.tgz' and it just stalls forever after downloading 25MB. Is NPM blacklisting me for having installed too many packages today?

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 18:37):

Oh ok I have misled you. In the index.html you actually have to run:

From Coq Require Import Lia.

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 18:37):

Sorry! :worried:

view this post on Zulip Shachar Itzhaky (Jul 07 2021 at 18:46):

I will set implicit_libs: true in these examples for future versions. It is admittedly confusing to newcomers.

view this post on Zulip Darij Grinberg (Jul 07 2021 at 19:00):

@Shachar Itzhaky Thank you! This works

view this post on Zulip Darij Grinberg (Jul 07 2021 at 19:01):

my next question would be how to install packages (specifically, the dependencies of https://github.com/hivert/Coq-Combi ) and then how to work on a multi-file project

view this post on Zulip Shachar Itzhaky (Jul 08 2021 at 12:24):

mathcomp is already available; npm i @jscoq/mathcomp, then you can add 'mathcomp' to all_pkgs in the config.

view this post on Zulip Shachar Itzhaky (Jul 08 2021 at 12:25):

Compiling packages unfortunately still requires that you build jsCoq locally (so that you have a compatible coqc). We are working on a Docker image that will allow to circumvent this need... but it's not ready yet.

view this post on Zulip Shachar Itzhaky (Jul 08 2021 at 12:29):

follow https://github.com/jscoq/jscoq/blob/v8.13/docs/build.md. It used to work on WSL; I have not tested it for some time (there is no WSL image in GitHub CI). Notice that you probably need to do a 64-bit build on WSL. Let me know if this works for you.

view this post on Zulip Darij Grinberg (Jul 08 2021 at 18:42):

thanks -- I've now gotten coqide to work, so this has fallen to low priority for me (much as I love the idea of running coq in my browser)

view this post on Zulip Shachar Itzhaky (Jul 09 2021 at 16:48):

Ok! BTW you can also try VSCoq (Visual Studio Code plugin).
I think that for multi-file project the support in jsCoq may be a bit too bleeding-edge.
Regardless, I have compiled mathcomp.multinomials so probably will be included in future releases.

view this post on Zulip Darij Grinberg (Jul 09 2021 at 16:51):

yeah, I've tried vscoq too, couldn't really get it to work either for a different reason :)

view this post on Zulip Darij Grinberg (Jul 09 2021 at 16:52):

great news about multinomials

view this post on Zulip Shachar Itzhaky (Jul 09 2021 at 16:53):

I found that there are many other packages under the mathcomp org. I wonder if there is an easy way to make them all available to our users without having to go over them one by one.


Last updated: Jan 30 2023 at 17:03 UTC