Stream: jsCoq

Topic: jscoq with mathcomp 1.13.0


view this post on Zulip Cyril Cohen (Dec 03 2021 at 10:37):

@Emilio Jesús Gallego Arias @Shachar Itzhaky @Enrico Tassi how do I get mathcomp 1.13.0 in jscoq ? (preferably through npm)

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:04):

Ah, we don't have a version ready but I guess I can compile one for you. I can post a .tar.gz that you can install through npm.

view this post on Zulip Enrico Tassi (Dec 03 2021 at 12:11):

Is there any doc on how to do that? I know @Cyril Cohen needs to add a few more mathcomp extras on top of it

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:13):

Hmm this has been a gap for some time; atm compiling libraries requires that you build your own jsCoq, because it needs the coqc that jsCoq uses in order for the binaries to be compatible.

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:14):

This is the location of the build doc: https://github.com/jscoq/jscoq/blob/v8.14/docs/build.md

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:17):

We did not find a satisfactory method for allowing user builds without it, although there are some hacks. E.g. in waCoq you can replace your coqc with npx wacoq coqc, provided that you have coqc globally installed with the same version as waCoq's.

view this post on Zulip Cyril Cohen (Dec 03 2021 at 12:20):

Shachar Itzhaky said:

Ah, we don't have a version ready but I guess I can compile one for you. I can post a .tar.gz that you can install through npm.

Please do that. I'm not sure I will manage to compile jscoq myself (I'm using nixos and I'm afraid there is a lot of setup to do to allow a custom compilation of jscoq)

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:21):

Actually all you need to have is installable through opam by running ./etc/toolchain-setup.sh. Haven't tried nix though. It will probably be some adventure.

view this post on Zulip Cyril Cohen (Dec 03 2021 at 12:28):

Could I have both a 8.13 and 8.14 version (I did not test 8.14 enough yet)...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:33):

Can't we just allow people to download the docker image?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:34):

@Cyril Cohen also you can use docker which IMO may be the best for people needing addons

view this post on Zulip Cyril Cohen (Dec 03 2021 at 12:34):

Emilio Jesús Gallego Arias said:

Cyril Cohen also you can use docker which IMO may be the best for people needing addons

I do not understand how to use it

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:36):

dockerfile is at etc/docker/Dockerfile

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:36):

I'm not expert at docker, but you can just do docker build

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:36):

then login into the build image

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:37):

but don't we push already a pre-built docker somewhere @Shachar Itzhaky ?

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:38):

AFAIR you have made some GitHub action that builds the docker but the publish stage was not complete.

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:38):

Can we perhaps pull the image from the build result somehow?

view this post on Zulip Cyril Cohen (Dec 03 2021 at 12:41):

:scream: you do manual installs https://github.com/jscoq/addon-mathcomp-extra/blob/v8.13/Makefile ?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:45):

Cyril Cohen said:

:scream: you do manual installs https://github.com/jscoq/addon-mathcomp-extra/blob/v8.13/Makefile ?

what do you mean? Yup, we have our packaging system :) It is pretty old actually

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:46):

The plan is that for Dune 3.0 we can however just clone and build with build and I wrote rules for Dune to call coq-pkg

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:46):

We do extra fancy stuff that OPAM / Nix can't do so far [maybe Nix, but last time I looked at the stuff was a bit overwhelmed]

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:47):

we generate a special package format that includes symbols, deps, etc... so we can do lazy loading in the browser, is also compressed

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:47):

Really cool stuff mostly the work of Shachar XD

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:48):

Dune helps us a lot as we can keep a local build and we don't need to mess with paths / install / etc... and have even mulitple context or cross compile without messy stuff

view this post on Zulip Cyril Cohen (Dec 03 2021 at 12:50):

That sounds awesome, I'm simply afraid I can't wrap my head around it anytime soon

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:50):

It's actually pretty easy, we just didn't polish it enough

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 12:51):

we will add the missing packages and upload them to npm you are all set

view this post on Zulip Cyril Cohen (Dec 03 2021 at 12:51):

Emilio Jesús Gallego Arias said:

we will add the missing packages and upload them to npm you are all set

That would be great!
I'm sure it's possible to figure out a simple thing using nix, it's even more compositional than Dune IMO.

view this post on Zulip Cyril Cohen (Dec 03 2021 at 12:52):

Cyril Cohen said:

Emilio Jesús Gallego Arias said:

we will add the missing packages and upload them to npm you are all set

That would be great!
I'm sure it's possible to figure out a simple thing using nix, it's even more compositional than Dune IMO.

(and it can be combined to Dune, and pre-patch sources to force Dune usage if you really need to)

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 12:59):

For the time being, I added the mathcomp 1.13.0 version to the jsCoq 0.14.0 release entry.
https://github.com/jscoq/jscoq/releases/tag/v0.14.0

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 13:00):

We don't really have a good discipline for how to distribute different versions of the same library... right now every release of jsCoq is tied to a particular version of each of the companion packages. We wanted to change this for like forever, because @Emilio Jesús Gallego Arias noted that one of the motivations for jsCoq was being able to quickly try out different versions of mathcomp.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 13:01):

Cyril Cohen said:

Emilio Jesús Gallego Arias said:

we will add the missing packages and upload them to npm you are all set

That would be great!
I'm sure it's possible to figure out a simple thing using nix, it's even more compositional than Dune IMO.

Dune replaces coq_makefile, is a different story ; the thing is that we need to patch Coq, so I'm unsure if a regular nix workflow would work so well

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 13:01):

Indeed @Shachar Itzhaky , actually it has been just a problem of manpower, I'm working hard trying to get some manpower here to help us

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 13:02):

because IMHO we know more or less what to do

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 13:02):

But myself I need to write lots of papers now as to have a chance to tenure in Inria

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 13:02):

so I'm left with little dev time for now

view this post on Zulip Emilio Jesús Gallego Arias (Dec 03 2021 at 13:02):

Pity because we are not far at from having a very streamlined workflow

view this post on Zulip Cyril Cohen (Dec 03 2021 at 13:05):

Emilio Jesús Gallego Arias said:

Cyril Cohen said:

Emilio Jesús Gallego Arias said:

we will add the missing packages and upload them to npm you are all set

That would be great!
I'm sure it's possible to figure out a simple thing using nix, it's even more compositional than Dune IMO.

Dune replaces coq_makefile, is a different story ; the thing is that we need to patch Coq, so I'm unsure if a regular nix workflow would work so well

Yes, nix is totally made for patching litterally anything on the fly.

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 14:51):

Good luck with that @Emilio Jesús Gallego Arias !!! :heart:

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 14:51):

I have tried working with nix before. I even still have a nix volume on my hard drive... but I never managed to learn it well enough.

view this post on Zulip Shachar Itzhaky (Dec 03 2021 at 17:47):

@Emilio Jesús Gallego Arias I have pushed this image to dockerhub:
https://hub.docker.com/repository/docker/poware/jscoq

But I was not able to do anything meaningful with it... in particular, I couldn't install OPAM and Dune because of some SSL certificate mumbo.


Last updated: Jan 30 2023 at 17:03 UTC