Stream: jsCoq

Topic: Making a HoTT addon


view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 16:16):

Not sure this is supported, cc @Shachar Itzhaky

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 16:16):

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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 16:21):

Rather in the dune for theories, it compiles now!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:40):

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

view this post on Zulip 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'`.) |

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 17:41):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:55):

No, it's a runtime flag

view this post on Zulip Shachar Itzhaky (Apr 07 2021 at 17:56):

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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:56):

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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:56):

Ah right, you also need to pass it to coqc

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:57):

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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 17:57):

HoTT had no dune file but that was easy :)

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Apr 07 2021 at 18:01):

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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 18:05):

Yep

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 18:05):

Then I tried the make pack thing

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 18:05):

Exactly npm install gets very confused

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 18:06):

I see

view this post on Zulip 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:

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 18:07):

Alright

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Apr 07 2021 at 18:08):

the website is built that way.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 18:14):

Does (mode promote) for the node_modules target help?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 18:15):

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

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 18:20):

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 18:26):

Seems entirely possible to me that HoTT has this size.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 18:29):

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Matthieu Sozeau (Apr 07 2021 at 18:57):

Yep, sounds like a useful setup to have

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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:

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2021 at 19:05):

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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip Matthieu Sozeau (Apr 23 2021 at 10:38):

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

view this post on Zulip Matthieu Sozeau (Apr 23 2021 at 10:38):

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

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Apr 24 2021 at 15:31):

ok thx -- will try


Last updated: Jan 31 2023 at 10:01 UTC