Stream: jsCoq

Topic: Ideas for jsCoq bundling


view this post on Zulip Karl Palmskog (Sep 07 2020 at 12:34):

Before I forget, let me add some ideas for projects that would be cool to run via a browser:

view this post on Zulip Karl Palmskog (Sep 07 2020 at 12:39):

with some gamification on top we could "compete" with all those Lean games: https://github.com/ImperialCollegeLondon/natural_number_game http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

view this post on Zulip Bas Spitters (Sep 07 2020 at 13:05):

Also fun: we can use our certified graphical calculator again. Now integrated the stdlib reals.
https://github.com/coq-community/corn/issues/123
@Vincent Semeria fixed it.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 14:27):

@Shachar Itzhaky could you comment on how easy or hard any of these would be to package using jsCoq? Could Bas or I help out to make it happen?

view this post on Zulip Bas Spitters (Sep 07 2020 at 19:41):

In fact, the graphics plugin should also work for coqoban.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 20:01):

since the following not only has a solver but also a checker, it could work as well: https://github.com/coq-contribs/sudoku

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 10:47):

@Karl Palmskog @Bas Spitters Hi there! Creating jsCoq bundles should be simplified with jsCoq 0.12.0. You still need to build jsCoq yourself because you need to compile the .vo files with jsCoq's own Coq, but then you can build packages easily with Dune. Documentation is a bit sparse on the matter but you can see some recent examples here: https://github.com/jscoq/addons

The recommended way is to run make install after you build jsCoq; this will install Coq binaries into the jscoq+32bit OPAM switch so that it would not clash with any "official" version of Coq installed in your system.

view this post on Zulip Bas Spitters (Sep 08 2020 at 11:28):

@Shachar Itzhaky Thanks. However, I understand that SF is already included. Will it also be included in collacoq?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:15):

I'd be happy to include it in collacoq, however SF is not in npm right @Shachar Itzhaky ?

I tried to build myself but unfortunately I didn't manage to use the addons build system when doing a local build so I need to solve any of these 2 issues before I can update collacoq's jscoq

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 15:20):

Hi, I'm happy to help with addon building stuff. You can consult our Dockerfile to see how I built the addons for this release. (https://github.com/jscoq/jscoq/blob/v8.12/etc/docker/Dockerfile)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:23):

For SF you are using a private repos so that's the main blocker I think

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 15:23):

I did not upload SF but that was a completely arbitrary decision. I can definitely publish the compiled .vos as a package too. (CI does not compile them because it has to check out from DeepSpec/sfdev right now and it is a private repo)

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 15:23):

Emilio Jesús Gallego Arias said:

For SF you are using a private repos so that's the main blocker I think

I still have it only it's in a separate Dockerfile.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:24):

I see, I guess publishing the package would be fine, tho we ought to be careful with the versioning

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 15:24):

do you mean w.r.t. compatibility of .vo files?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:25):

Versioning of the SF suite itself, if we publish the vo files they will likely be out of sync with the official published version of SF

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:25):

which is as of now Version 5.8 (2020-08-24 16:38, Coq 8.12)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:26):

so it is pretty much up to date tho

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:26):

maybe you can just add the date to the version number

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 15:27):

I did rebase the jscoq branch of SF so it pretty much matches the latest release. Hopefully Pierce will be open to merging the branch into the main repo.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:27):

Indeed the rest of the packages do need an improved version number

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:27):

for exapmle mathcom should be something such as 0.12.0+1.11.0

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:27):

or even they should be different packages?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:27):

@jscoq/mathcomp-1.10 , @jscoq@mathcom-1.11 etc...

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 15:28):

Versioning is always confusing, I put the version in the description of the package, since NPM follows semver and it is not very expressive for multi-dependency stuff.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:28):

For now regarding SF anything will do so @Bas Spitters can try to use collacoq

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:28):

even tho there is still some nasty bug

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 15:29):

does npm allow to install two versions of a package simultaneously?

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 15:31):

Emilio Jesús Gallego Arias said:

does npm allow to install two versions of a package simultaneously?

I believe the simple answer is no. The long answer is that they can be installed if they are dependencies of two different packages, but then they will be nested inside the packages that depend on them and isolated from the rest of the packages.

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 18:39):

Emilio Jesús Gallego Arias said:

@jscoq/mathcomp-1.10 , @jscoq@mathcom-1.11 etc...

Is there a real use case for having multiple versions of packages per a single release of jsCoq? I assume some users might have developments that e.g. work on mathcomp 1.10 but not on 1.11, is that common enough though?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 18:40):

For math-comp indeed it is, I wonder for other systems such as compcert etc...

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 18:40):

but certainly jsCoq should enable users to bootstrap with a concrete set of packages

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 18:41):

For example, a nice use case is to test bugs in different coq versions

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 18:41):

quickly

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 18:41):

so yeah I'd say that supporting multiple versions of packages was a goal from the start, how to implement that, it is open

view this post on Zulip Shachar Itzhaky (Sep 08 2020 at 18:43):

The annoying part is the cartesian product of jsCoq version x package version. This can get really confusing really fast.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 08 2020 at 18:54):

Yeah there are several approaches to do this; I guess the build file for the full distribution should specify which version of each addon are wanted


Last updated: Jan 30 2023 at 18:04 UTC