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?
Not sure this is supported, cc @Shachar Itzhaky
Probably it should be in the dune-project
for HoTT rather?
Rather in the dune
for theories
, it compiles now!
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?
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
I'm afraid I don't know how the new addon system works, we need help from @Shachar Itzhaky
Ok, I have it working now. I would just need to be able not to load the 'init' package
Got it, with prelude = false, but still loading the init package, it works
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'`.) |
Oh I see you figured it out while I was pasting the code :)
Glad to hear it worked, I'm a bit pressed this week to really help
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?
No, it's a runtime flag
Oh, you wrote coqc
, perhaps you just meant coqtop
?
The HoTT library is incompatible with Coq's prelude, but it needs the plugins from Coq.
Ah right, you also need to pass it to coqc
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.
So indeed I used coq.theory
's flags
to handle that part
HoTT had no dune file but that was easy :)
I'm still lost as for the npm errors. In the end I just put my package and json file in coq-pkgs/
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.
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
I think we need init
as it contains the ml plugins that are still needed by the hott package
Ah, makes sense... Did you make a .coq-pkg
file?
Yep
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
.
Then I tried the make pack
thing
Exactly npm install
gets very confused
What happens is, npm creates the node_modules
directory, but that conflicts with a Dune target with the same name.
The problem is that I wanted to make jscoq
to update the html files in _build
from the sources
I see
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:
Alright
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.
the website is built that way.
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.
Does (mode promote)
for the node_modules target help?
If that's broken for dirs, it should be possible to fix upstream
Hmm. Am I doing something wrong if my distribution is 200MB large ?
Seems entirely possible to me that HoTT has this size.
The build for 8.10 that I have around was 120MiB of .vo files
Yes, browser developers have fun with us preloading GiB of vo files sometimes :)
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:
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.
We should really use github actions to upload the releases, I have no cycles for that sadly...
Yep, sounds like a useful setup to have
Is there any more tricks needed to get the node_modules files loaded than adding the .nojekyll
file?
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.
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.
Steps 2/3 should be automatic if the library is using Dune
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
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:
.vo
s are incompatible with jsCoq's..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.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-cli
package [which is mostly general I understand]
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.
Safer is to have a hash for the SDK and indeed embed it in the packages as to provide a nice error message.
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.
Shachar Itzhaky said:
Yeah, the packager is available as soon as you
npm i jscoq
, asnpx jscoq
; a dev may opt to install globally (though discouraged by npm officials)npm i -g jscoq
and then use it as justjscoq
.
So a jsCoq image in DockerHub, perhaps with an accompanying script that redirectscoqc
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
@Matthieu Sozeau Where is the current version of your HoTT addon? I would like to try building it :)
Here's the files I used, IIRC hott.tgz
But you can start afresh I think, it's now a fairly regular package.
Indeed, HoTT build now is just a regular build but passing -noinit
, ideally we would pass -boot
too but that's not working yet.
ok thx -- will try
Last updated: Jun 01 2023 at 12:01 UTC