Stream: jsCoq

Topic: jsCoq helloworld fails


view this post on Zulip Jordan Winkler (Jul 03 2021 at 19:43):

I am new to JavaScript. So on a Debian install of Firefox, running the index in the Npm install of jsCoq I receive a "Failed to start jsCoq worker." Passing in "--allow-file-access-from-files" does not work on Firefox. Why?

On Chromium with this argument, it loads, but then fails in another way:

Package 'coq' is missing (file:///home/jordan/code/web_coq/node_modules/jscoq/coq-pkgs/coq.json: not found (0))

coq.json is definitely there.

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

Likely the documentation is out of date, recent browser versions have turned the --allow-file-access stuff into a no op

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

you could try serving your directory with for example npm's http-server

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

Using the file:// scheme is a bit broken in most browsers. Since the JS side is using fetch(), I suspect that depending on the browser implementation, it may not be willing to give you access to the file (the flag should in principle allow it, but :shrug:)


Last updated: Jan 31 2023 at 11:01 UTC