Darij Grinberg (Jul 06 2021 at 19:05): 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?
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?)
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?
Notification Bot (Jul 07 2021 at 08:07):This topic was moved here from #Coq users > windows vs WSL by Théo Zimmermann
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?
Emilio Jesús Gallego Arias (Jul 07 2021 at 09:38):that's what I use on linux
Emilio Jesús Gallego Arias (Jul 07 2021 at 09:39):it's a very simple web server
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...
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).
Darij Grinberg (Jul 07 2021 at 13:34):ok, what do I do next?
Darij Grinberg (Jul 07 2021 at 13:34):how do I connect? and which directory should I run this in?
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.
Darij Grinberg (Jul 07 2021 at 14:50):hmm
Darij Grinberg (Jul 07 2021 at 14:50):i don't think it's working
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
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 -
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)?
Janno (Jul 07 2021 at 14:53):Maybe there is some git submodule for codemirror that hasn't been initialized?
Darij Grinberg (Jul 07 2021 at 14:53):ah right
Darij Grinberg (Jul 07 2021 at 14:53):there is no /codemirror at all
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
Emilio Jesús Gallego Arias (Jul 07 2021 at 14:54):oh sorry, I thought you had installed jscoq from npm
Darij Grinberg (Jul 07 2021 at 14:54):i have
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
Emilio Jesús Gallego Arias (Jul 07 2021 at 14:54):I am not familiar with the npm setup a lot, ccing @Shachar Itzhaky
Darij Grinberg (Jul 07 2021 at 14:54):i'm serving node_modules/jscoq; is that wrong?
Darij Grinberg (Jul 07 2021 at 14:54):was "npm install jscoq" too simple?
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
Darij Grinberg (Jul 07 2021 at 14:55):hmm
Darij Grinberg (Jul 07 2021 at 14:56):ah!
Darij Grinberg (Jul 07 2021 at 14:56):the entire node_modules needs to be served
Darij Grinberg (Jul 07 2021 at 14:56):thank you! that wasn't very intuitive though :)
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
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))
Darij Grinberg (Jul 07 2021 at 14:57):do i need to compile them first?
Darij Grinberg (Jul 07 2021 at 14:58):or should i just ditch npm and install it from the repo?
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.)
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?
Darij Grinberg (Jul 07 2021 at 17:08):Some simple code snippet?
Shachar Itzhaky (Jul 07 2021 at 17:08):Try e.g. Require Import Lia.
Darij Grinberg (Jul 07 2021 at 17:09):ah seems to work
Darij Grinberg (Jul 07 2021 at 17:09):or not
Darij Grinberg (Jul 07 2021 at 17:09):Cannot find a physical path bound to logical path matching
suffix <>.
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.
Shachar Itzhaky (Jul 07 2021 at 17:10):Looks like it did not find the package files (coq.json etc.) after all :(
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.
Darij Grinberg (Jul 07 2021 at 17:10):= 297 : nat
Darij Grinberg (Jul 07 2021 at 17:10):so the "core", whatever it is, seems to be in place
Shachar Itzhaky (Jul 07 2021 at 17:11):Oh so it found init but not arith? hmm
Shachar Itzhaky (Jul 07 2021 at 17:11):did you get any warnings in the message area, on startup?
Darij Grinberg (Jul 07 2021 at 17:11):it actually spent some time loading parts of ssreflects from your command
Shachar Itzhaky (Jul 07 2021 at 17:11):For Lia? :-s
Darij Grinberg (Jul 07 2021 at 17:11):yeah
Darij Grinberg (Jul 07 2021 at 17:11):maybe the error message was spurious
what's a way to check if it was successful?
Shachar Itzhaky (Jul 07 2021 at 17:12):ok wait that's super strange. I'm trying to reproduce.
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)
Darij Grinberg (Jul 07 2021 at 17:14):you're right, it's not spurious
Darij Grinberg (Jul 07 2021 at 17:14):do you have a few minutes to zoom?
Shachar Itzhaky (Jul 07 2021 at 17:14):wait let me try to run the exact same commands. Doing npm i jscoq now.
Darij Grinberg (Jul 07 2021 at 17:15):are you on WSL?
Darij Grinberg (Jul 07 2021 at 17:15):that might be causing file access issues
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?
Darij Grinberg (Jul 07 2021 at 17:17):python3 -m http.server in my node-modulesdirectory
Darij Grinberg (Jul 07 2021 at 17:17):python 3.7.3, node v10.24.0, jscoq freshly installed yesterday or so
Shachar Itzhaky (Jul 07 2021 at 17:22):It seemed to work on Linux. Let me try WSL now.
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
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?
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
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.
Shachar Itzhaky (Jul 07 2021 at 18:01):weirdly enough npm i wacoq does work :face_palm:
Darij Grinberg (Jul 07 2021 at 18:07):that seems to be it.
meaning the installer has failed to download all files?
Shachar Itzhaky (Jul 07 2021 at 18:08):No, I meant that these are the files that should be there.
Darij Grinberg (Jul 07 2021 at 18:08):ah
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?
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.
Sorry! :worried:
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.
Darij Grinberg (Jul 07 2021 at 19:00):@Shachar Itzhaky Thank you! This works
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
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.
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.
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.
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)
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.
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 :)
Darij Grinberg (Jul 09 2021 at 16:52):great news about multinomials
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: May 31 2023 at 02:31 UTC