Cyril Cohen (Dec 03 2021 at 10:37): 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)
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.
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
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.
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
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.
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.gzthat 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)
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.
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)...
Emilio Jesús Gallego Arias (Dec 03 2021 at 12:33):Can't we just allow people to download the docker image?
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
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
Emilio Jesús Gallego Arias (Dec 03 2021 at 12:36):dockerfile is at etc/docker/Dockerfile
Emilio Jesús Gallego Arias (Dec 03 2021 at 12:36):I'm not expert at docker, but you can just do docker build
Emilio Jesús Gallego Arias (Dec 03 2021 at 12:36):then login into the build image
Emilio Jesús Gallego Arias (Dec 03 2021 at 12:37):but don't we push already a pre-built docker somewhere @Shachar Itzhaky ?
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.
Shachar Itzhaky (Dec 03 2021 at 12:38):Can we perhaps pull the image from the build result somehow?
Cyril Cohen (Dec 03 2021 at 12:41)::scream: you do manual installs https://github.com/jscoq/addon-mathcomp-extra/blob/v8.13/Makefile ?
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
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
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]
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
Emilio Jesús Gallego Arias (Dec 03 2021 at 12:47):Really cool stuff mostly the work of Shachar XD
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
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
Emilio Jesús Gallego Arias (Dec 03 2021 at 12:50):It's actually pretty easy, we just didn't polish it enough
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
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.
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)
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
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.
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
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
Emilio Jesús Gallego Arias (Dec 03 2021 at 13:02):because IMHO we know more or less what to do
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
Emilio Jesús Gallego Arias (Dec 03 2021 at 13:02):so I'm left with little dev time for now
Emilio Jesús Gallego Arias (Dec 03 2021 at 13:02):Pity because we are not far at from having a very streamlined workflow
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.
Shachar Itzhaky (Dec 03 2021 at 14:51):Good luck with that @Emilio Jesús Gallego Arias !!! :heart:
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.
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: Oct 01 2023 at 18:01 UTC