Karl Palmskog (Sep 07 2020 at 12:34): 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:
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/
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.
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?
Bas Spitters (Sep 07 2020 at 19:41):In fact, the graphics plugin should also work for coqoban.
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
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.
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?
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
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)
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
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)
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.
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
Shachar Itzhaky (Sep 08 2020 at 15:24):do you mean w.r.t. compatibility of .vo files?
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
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)
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:26):so it is pretty much up to date tho
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:26):maybe you can just add the date to the version number
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.
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:27):Indeed the rest of the packages do need an improved version number
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
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:27):or even they should be different packages?
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:27):@jscoq/mathcomp-1.10 , @jscoq@mathcom-1.11 etc...
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.
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
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:28):even tho there is still some nasty bug
Emilio Jesús Gallego Arias (Sep 08 2020 at 15:29):does npm allow to install two versions of a package simultaneously?
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.
Shachar Itzhaky (Sep 08 2020 at 18:39):Emilio Jesús Gallego Arias said:
@jscoq/mathcomp-1.10,@jscoq@mathcom-1.11etc...
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?
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...
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
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
Emilio Jesús Gallego Arias (Sep 08 2020 at 18:41):quickly
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
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.
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: Apr 16 2024 at 04:02 UTC