## 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: Jan 31 2023 at 10:01 UTC