Stream: jsCoq

Topic: How to make an interactive website from scratch?

Cyril Cohen (Dec 01 2021 at 23:33):

Hi, I've spent the last half day trying to setup a website such as https://coq-next.now.sh. I managed to do a seemingly npm install, and successfull ran npx jscoqdoc, but the generated html contains <script src="./ui-js/jscoq-loader.js"></script> (and not ./node_modules/jscoq/ui-js/jscoq-loaders.js and it seems that the path to codemirror is also wrong, but I don't know where or how yet).
Could someone point me to the sources of a generated webpage, together with a script (nix, docker or action, preferably some reproducible thing) that builds everything from scratch?
Also I wish to use mathcomp 1.13.0 but I can't seem to find where or how to select versions of packages...

Cyril Cohen (Dec 01 2021 at 23:36):

update: by copying node_modules/* at the root of the website I managed to run codemirror, now mathcomp is not found, although my package.json contains the following:

  "dependencies": {
    "express": "^4.17.1",
    "jscoq": "^0.13.3",
    "@jscoq/mathcomp": "^0.13.3"
  },

Cyril Cohen (Dec 01 2021 at 23:39):

(also if I want to customize the headers, for example adding some tex-like-based rendering (e.g. using mathjax), what is the best practice to do that?)

Emilio Jesús Gallego Arias (Dec 02 2021 at 02:59):

@Shachar Itzhaky knows a bit more about how this is done, it is been a while I don't generate .v.html files

For mathjax I was able to just use it succesfully , but by hand.

In general we need to streamline the workflow quite a lot, but we lack manpower

Enrico Tassi (Dec 02 2021 at 07:06):

do you have the same header/footer we use here?
https://github.com/math-comp/mcb/tree/master/coq

Enrico Tassi (Dec 02 2021 at 07:07):

also it seems you can point inside the noxe modules dir, rather than copying out

Shachar Itzhaky (Dec 03 2021 at 12:18):

Hmm yes the use case of jscoqdoc seems a bit broken. The scripts generates wrong paths... sry it has undergone zero qa.

Shachar Itzhaky (Dec 03 2021 at 16:47):

Oh I just discovered that there is an environment variable JSCOQ_URL. If you set it before running jscoqdoc it will determine the prefix used. So you can set it to e.g. ./node_modules/jscoq.

Ofc the default should not be . and also this var should be documented.

Cyril Cohen (Dec 03 2021 at 18:15):

Another problem with jscoqdoc is that it does not seem to accept the arguments to option --with-footer and --with-header (it looks like to discards them before calling coqdoc...)

Cyril Cohen (Dec 03 2021 at 18:15):

I'm sturggling to put enclosing <div> around chunks of code & comments, is it possible?

Cyril Cohen (Dec 03 2021 at 18:17):

Also it seems that jscoq will only transform coqdoc to textareas if it is caught by #main > div.code, so if I have extra divs inbetween, it does not work... setting up jscoq_ids = ['div.code']; does not seem to help :sad:

Shachar Itzhaky (Dec 03 2021 at 22:31):

Ahhh that's a nasty presumption on my part... I was assuming that any .html files on the jscoqdoc command line are meant to be processed by jscoqdoc proper instead of being passed on to coqdoc. I completely overlooked --with-{header,footer}.

So, hack: either rename your header and footer to not end in .html (sorry). Or, run coqdoc yourself however you like, and then run jscoqdoc on the resulting HTMLs.

Shachar Itzhaky (Dec 03 2021 at 22:32):

As for jscoq_ids... yeah overriding it should have worked. Perhaps double-check by putting a breakpoint in jscoq-agent.js at the point where it tries to initialize jsCoq?

Cyril Cohen (Dec 04 2021 at 00:21):

Shachar Itzhaky said:

As for jscoq_ids... yeah overriding it should have worked. Perhaps double-check by putting a breakpoint in jscoq-agent.js at the point where it tries to initialize jsCoq?

I'm using jscoq-loader.js rather than jscoq-agent.js, what's the difference?

Cyril Cohen (Dec 04 2021 at 00:33):

Shachar Itzhaky said:

As for jscoq_ids... yeah overriding it should have worked. Perhaps double-check by putting a breakpoint in jscoq-agent.js at the point where it tries to initialize jsCoq?

My mistake (in a Makefile), the change to my .js file was not propagated correctly, it does work to edit jscoq_ids

Last updated: Jun 01 2023 at 12:01 UTC