Stream: jsCoq

Topic: Making a HoTT addon

Matthieu Sozeau (Apr 07 2021 at 16:15):

I'm progressing making a HoTT addon for JSCoq, right now I just can't figure out how to pass --boot to the coqc command. I'm trying.

(rule
 (targets coq-pkgs)
 (deps
  (package hott)
  (:pkg-json hott-pkg.json))
 (action
  (run npx %{env:pkgtool=jscoq} build %{pkg-json} --noinit -indices-matter --nostdlib)))

(alias
 (name all)
 (deps package.json))

@Emilio Jesús Gallego Arias any idea?

Emilio Jesús Gallego Arias (Apr 07 2021 at 16:16):

Not sure this is supported, cc @Shachar Itzhaky

Matthieu Sozeau (Apr 07 2021 at 16:16):

Probably it should be in the dune-project for HoTT rather?

Matthieu Sozeau (Apr 07 2021 at 16:21):

Rather in the dune for theories, it compiles now!

Matthieu Sozeau (Apr 07 2021 at 16:59):

I don't understand what I'm supposed to do with the new jscoq-hott.tgz though. Come back to my jscoq instance and npm install it? Then what?

Matthieu Sozeau (Apr 07 2021 at 17:19):

I get very weird errors if I go back to jscoq/ and do npm install jscoq-hott.tgz. The npm runs fine, but the make jscoq fails

Emilio Jesús Gallego Arias (Apr 07 2021 at 17:20):

I'm afraid I don't know how the new addon system works, we need help from @Shachar Itzhaky

Matthieu Sozeau (Apr 07 2021 at 17:33):

Ok, I have it working now. I would just need to be able not to load the 'init' package

Matthieu Sozeau (Apr 07 2021 at 17:40):

Got it, with prelude = false, but still loading the init package, it works

Emilio Jesús Gallego Arias (Apr 07 2021 at 17:41):

For that you have a noinit option, see:

| `prelude`       | boolean         | `true`          | Load the Coq prelude (`Coq.Init.Prelude`) at startup. (If set, make sure that `init_pkgs` includes `'init'`.) |

Emilio Jesús Gallego Arias (Apr 07 2021 at 17:41):

Oh I see you figured it out while I was pasting the code :)

Emilio Jesús Gallego Arias (Apr 07 2021 at 17:41):

Glad to hear it worked, I'm a bit pressed this week to really help

Shachar Itzhaky (Apr 07 2021 at 17:55):

Wait what, I'm not sure I understand what happened. @Matthieu Sozeau was asking about a compile time flag, no? prelude: false is a runtime option... passing flags to coqc should be handled by the coq.theory in Dune, probablt?

Matthieu Sozeau (Apr 07 2021 at 17:55):

No, it's a runtime flag

Shachar Itzhaky (Apr 07 2021 at 17:56):

Oh, you wrote coqc, perhaps you just meant coqtop?

Matthieu Sozeau (Apr 07 2021 at 17:56):

The HoTT library is incompatible with Coq's prelude, but it needs the plugins from Coq.

Matthieu Sozeau (Apr 07 2021 at 17:56):

Ah right, you also need to pass it to coqc

Shachar Itzhaky (Apr 07 2021 at 17:57):

Yeah actually I assume the compile-time flags are already handled by HoTT's Dune files, otherwise it would not work even in native Coq.

Matthieu Sozeau (Apr 07 2021 at 17:57):

So indeed I used coq.theory's flags to handle that part

Matthieu Sozeau (Apr 07 2021 at 17:57):

HoTT had no dune file but that was easy :)

Matthieu Sozeau (Apr 07 2021 at 17:58):

I'm still lost as for the npm errors. In the end I just put my package and json file in coq-pkgs/

Shachar Itzhaky (Apr 07 2021 at 17:58):

Neat, yeah so prelude: false stops jsCoq from doing Require Init.Prelude. on startup. As for the init package, probably just a bug on our side -- perhaps some code there assumes that init_pkgs is never empty.

Shachar Itzhaky (Apr 07 2021 at 18:00):

Matthieu Sozeau said:

I'm still lost as for the npm errors. In the end I just put my package and json file in coq-pkgs/

Ok that's an excellent start! Packaging is something to think about but at least it already works so yay

Matthieu Sozeau (Apr 07 2021 at 18:01):

I think we need init as it contains the ml plugins that are still needed by the hott package

Shachar Itzhaky (Apr 07 2021 at 18:01):

Ah, makes sense... Did you make a .coq-pkg file?

Matthieu Sozeau (Apr 07 2021 at 18:05):

Yep

Shachar Itzhaky (Apr 07 2021 at 18:05):

Matthieu Sozeau said:

I get very weird errors if I go back to jscoq/ and do npm install jscoq-hott.tgz. The npm runs fine, but the make jscoq fails

Running make jscoq after compiling addons is no longer required. It shouldn't error though, it should just do nothing. There is an annoying issue in Dune that I haven't been able to work around that still happens if you run npm install.

Matthieu Sozeau (Apr 07 2021 at 18:05):

Then I tried the make pack thing

Matthieu Sozeau (Apr 07 2021 at 18:05):

Exactly npm install gets very confused

Shachar Itzhaky (Apr 07 2021 at 18:06):

What happens is, npm creates the node_modules directory, but that conflicts with a Dune target with the same name.

Matthieu Sozeau (Apr 07 2021 at 18:06):

The problem is that I wanted to make jscoq to update the html files in _build from the sources

Matthieu Sozeau (Apr 07 2021 at 18:06):

I see

Shachar Itzhaky (Apr 07 2021 at 18:07):

So the way I do it is this... (ugly) npm i whatever.tgz, then rm -rf node_modules, then make jscoq (it will run npm i again this time in the _build directory) :sad: :sad:

Matthieu Sozeau (Apr 07 2021 at 18:07):

Alright

Shachar Itzhaky (Apr 07 2021 at 18:08):

A more stable approach is to not install in the jsCoq source tree at all. Instead, create a third project that depends on jsCoq and your package.

Shachar Itzhaky (Apr 07 2021 at 18:08):

the website is built that way.

Shachar Itzhaky (Apr 07 2021 at 18:09):

With the help of npm link, development can be quick because you don't have to npm i anything, only after everything works you package the lot and then install properly.

Emilio Jesús Gallego Arias (Apr 07 2021 at 18:14):

Does (mode promote) for the node_modules target help?

Emilio Jesús Gallego Arias (Apr 07 2021 at 18:15):

If that's broken for dirs, it should be possible to fix upstream

Matthieu Sozeau (Apr 07 2021 at 18:20):

Hmm. Am I doing something wrong if my distribution is 200MB large ?

Emilio Jesús Gallego Arias (Apr 07 2021 at 18:26):

Seems entirely possible to me that HoTT has this size.

Emilio Jesús Gallego Arias (Apr 07 2021 at 18:28):

The build for 8.10 that I have around was 120MiB of .vo files

Emilio Jesús Gallego Arias (Apr 07 2021 at 18:29):

Yes, browser developers have fun with us preloading GiB of vo files sometimes :)

Shachar Itzhaky (Apr 07 2021 at 18:34):

Yep, I am lucky to have an internet connection with a particularly low upstream bandwidth, when I have to deploy the website I usually do it at night otherwise my wife can't use the Internet at all :grimacing:

Shachar Itzhaky (Apr 07 2021 at 18:36):

Emilio Jesús Gallego Arias said:

If that's broken for dirs, it should be possible to fix upstream

It was definitely broken some time ago and there was even a ticket, but I haven't tried again in a while.

Emilio Jesús Gallego Arias (Apr 07 2021 at 18:52):

We should really use github actions to upload the releases, I have no cycles for that sadly...

Matthieu Sozeau (Apr 07 2021 at 18:57):

Yep, sounds like a useful setup to have

Matthieu Sozeau (Apr 07 2021 at 18:57):

Is there any more tricks needed to get the node_modules files loaded than adding the .nojekyll file?

Shachar Itzhaky (Apr 07 2021 at 19:02):

You mean to get the GitHub Pages server to serve them..? I think that's about it. But there are definitely other gotchas in GitHub Pages that I don't recall off the top of my head.

Emilio Jesús Gallego Arias (Apr 07 2021 at 19:05):

Now that we are at it @Matthieu Sozeau , we have a plan to actually allow any library author to publish their own lib for jsCoq in a distributed way, basically adding a CI setup that does:

• download a particular docker image with jscoq toolchain installed
• build the addon with the right coqc in the docker image
• pack the addon
• publish it as an artifact

Then, you could just do in jsCoq pkg.push(url_of_artifact) and get it running.

Emilio Jesús Gallego Arias (Apr 07 2021 at 19:05):

Steps 2/3 should be automatic if the library is using Dune

Emilio Jesús Gallego Arias (Apr 07 2021 at 19:06):

I think that just pushing the docker image to the registry would make life much easier, and allow people to use the npm package verbatim

Shachar Itzhaky (Apr 07 2021 at 19:40):

We have the basic infrastructure for this already. I have experimented with creating a "jsCoq-sdk" in Docker (https://github.com/jscoq/jscoq/blob/2b3f67abe02a9d350a9d93f82336411ef6f60c8a/etc/docker/Dockerfile#L91) though it is now commented out because it wasn't too robust.
I also did a very nasty (but awesome!) hack in SF: I install Coq on the jscoq switch but then only use the installed coqc, taking all the libraries (.vo files) from the .coq-pkg files instead. Works quite well but also a not entirely satisfactory for two main reasons:

• You still need a 32-bit Coq with jsCoq patches applied. Otherwise generated .vos are incompatible with jsCoq's.
• The .coq-pkg bundles contain neither native plugin libraries (.cmxs) nor bytecode (.cmxa), instead they contain JS files generated with js_of_ocaml. So again I have to fall back to system-installed libraries. Bundling cmxs would ofc not be portable. Bundling cmxa would in theory be portable if we use waCoq (which provides a consistent runtime on top of WebAssembly), but compiling with waCoq would be extremely slow in most cases; even compiling with a bytecode version of coqc running on a native OCaml interpreter can be painful.

Emilio Jesús Gallego Arias (Apr 07 2021 at 20:36):

Thanks for the summary of your efforts Shachar!

Indeed I think we could have the sdk to be just the Coq from our vendoring , isn't that what you are doing anyways? That should be fine, tho we'd need to install also the jscoq-clipackage [which is mostly general I understand]

Emilio Jesús Gallego Arias (Apr 07 2021 at 20:37):

For the 2nd point, IIUC, I think we could just require consistency in the SDK , by indeed forcing all compilation calls to go via Docker.

Emilio Jesús Gallego Arias (Apr 07 2021 at 20:37):

Safer is to have a hash for the SDK and indeed embed it in the packages as to provide a nice error message.

Shachar Itzhaky (Apr 08 2021 at 12:29):

Yeah, the packager is available as soon as you npm i jscoq, as npx jscoq; a dev may opt to install globally (though discouraged by npm officials) npm i -g jscoq and then use it as just jscoq.
So a jsCoq image in DockerHub, perhaps with an accompanying script that redirects coqc to run in the container, should work. The CLI does not have to run in Docker.

Emilio Jesús Gallego Arias (Apr 08 2021 at 14:02):

Shachar Itzhaky said:

Yeah, the packager is available as soon as you npm i jscoq, as npx jscoq; a dev may opt to install globally (though discouraged by npm officials) npm i -g jscoq and then use it as just jscoq.
So a jsCoq image in DockerHub, perhaps with an accompanying script that redirects coqc to run in the container, should work. The CLI does not have to run in Docker.

Yup, the idea of the SDK I had in mind is that you build the addon inside the container, so the script you add to your addons CI is something that builds the run using the jsCoq published Docker image, then pushes the artifact

Shachar Itzhaky (Apr 23 2021 at 10:13):

@Matthieu Sozeau Where is the current version of your HoTT addon? I would like to try building it :)

Matthieu Sozeau (Apr 23 2021 at 10:38):

Here's the files I used, IIRC hott.tgz

Matthieu Sozeau (Apr 23 2021 at 10:38):

But you can start afresh I think, it's now a fairly regular package.

Emilio Jesús Gallego Arias (Apr 23 2021 at 12:16):

Indeed, HoTT build now is just a regular build but passing -noinit , ideally we would pass -boot too but that's not working yet.

Shachar Itzhaky (Apr 24 2021 at 15:31):

ok thx -- will try

Last updated: Jun 01 2023 at 12:01 UTC