8.14 · jsCoq · Zulip Chat Archive

hmm yes I agree there are definitely some pros and cons. For now, the state is not too much to be a hassle. It is mostly the state of the UI -- plus a queue of sentences that need to be added. I could not find a way to avoid the latter, because I have to wait until a sentence is added before adding the next.

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:01):

I did some progress, still need to tweak the init stuff, and the patches

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:01):

but hopefully I get to it today

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:01):

one thing is that we should document the node version we require

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:01):

we can't do that in the packages.json file, right?

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:01):

I was seeing some trouble, I think because of ubuntu having an old node

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:15):

Shachar, actually you are right and the new code for the state init is worse, and it is not fixed in master.

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:15):

Dunno what to do, anyways Stm.new_doc was a lie

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:16):

I mean, it couldn't be called twice; but I guess for now we will have to inverse-refactor

Shachar Itzhaky (Sep 16 2021 at 13:29):

Thanks!

I think Node 12.x is the minimum now because of some ES2017 stuff. I don't think there is a standard field in package.json for that. We should just write it in the README.

Shachar Itzhaky (Sep 16 2021 at 13:30):

Emilio Jesús Gallego Arias said:

I mean, it couldn't be called twice; but I guess for now we will have to inverse-refactor

I was actually able to call it twice. It is only that the load path reverts to what it was during init. Legit in some scenarios, I guess.

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:42):

Umm, actually if you call new_doc twice, it will overwrite the previous document

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:42):

the document is global inside the stm implementation, so yeah, maybe it works in terms of "reset", but that's dangeorus stuff

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:43):

Ok i was able to make SerAPI 8.14 work

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:43):

jsCoq should arrive soon

Shachar Itzhaky (Sep 16 2021 at 13:50):

Cool! I thought SerAPI worked already

Shachar Itzhaky (Sep 16 2021 at 13:50):

Emilio Jesús Gallego Arias said:

the document is global inside the stm implementation, so yeah, maybe it works in terms of "reset", but that's dangeorus stuff

I live on the edge of danger

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:53):

I know XD

Emilio Jesús Gallego Arias (Sep 16 2021 at 13:54):

For SerAPI only serlib was working, the toplevel stuff was quite broken due to a lot of upstream changes, now fixed

Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

Umm, I lost a lot of time getting some weird errors, it seems that my chromium version didn't like 8.14

Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

but in chrome dev, it works

Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

I dunno

Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

@Shachar Itzhaky anyways you can try the branch, seems to work here

Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

gonna have to do more cleanu

Shachar Itzhaky (Sep 16 2021 at 15:11):

Ok I will try to build on my Mac and on Docker

Shachar Itzhaky (Sep 16 2021 at 15:22):

oh the patches are commented out

Shachar Itzhaky (Sep 16 2021 at 15:22):

I have some partial porting of them in wacoq-bin. Will bring them over.

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:23):

Yup, I didn't do the patches, feel free to push over them

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:23):

Also I disabled some stuff, because I was getting this super weird bug in my main Chromium browser

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:24):

Lost 2 hours with than, then to have the idea to try a different browser version

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:24):

was scary

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:24):

Now that I think, it could well been just a limitation on the size of the .js file

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:24):

But we need to keep an eye on that

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:24):

I'm done for today, tomorrow will do another pass an clean the patch up

Emilio Jesús Gallego Arias (Sep 16 2021 at 16:25):

Maybe we can release 0.14.0 tomorrow :D

Shachar Itzhaky (Sep 16 2021 at 16:49):

lol ok :D I have ported most of the patches. Will push.

Emilio Jesús Gallego Arias (Sep 17 2021 at 11:49):

Great, thanks! I guess we can release?

Karl Palmskog (Sep 17 2021 at 12:00):

don't you want to wait until 8.14+rc1 is out? This will be the target of nearly everyone in the platform for tags/releases.

Emilio Jesús Gallego Arias (Sep 17 2021 at 12:12):

For me the state of the branch is good for a 0.14.0 release

Théo Zimmermann (Sep 17 2021 at 12:40):

That's it. The V8.14+rc1 tag is set.

Shachar Itzhaky (Sep 20 2021 at 18:08):

So. What would be the right way to install Coq 8.14? The docs say dune -p P && dune install P for P ∈ {coq-core, coq-stdlib}. This works ok but installs the theories in /lib/coq and native libraries (plugins) in /lib/coq-core. Is that intended?

Théo Zimmermann (Sep 21 2021 at 06:41):

You can also use the legacy configure + Makefile procedure. But yes, I think that it is intended that some stuff will be installed in coq-core.

Shachar Itzhaky (Sep 21 2021 at 11:22):

Hmm if I compile Coq v8.14 without running ./configure first, it does in fact build with dune build, but the version that is reported is 8.13.2. Possibly the version update can be in the Dune files as well to avoid confusion?

Théo Zimmermann (Sep 21 2021 at 11:24):

You probably didn't do this on a clean state, did you?

Théo Zimmermann (Sep 21 2021 at 11:24):

dune build is supposed to call configure by itself if you don't do it

Théo Zimmermann (Sep 21 2021 at 11:25):

The fact that it reports 8.13.2 lets me think that you did run configure yourself earlier on (on another branch) and that Dune is still using this.

Shachar Itzhaky (Sep 21 2021 at 11:26):

hmm yes that's possible! I was going to do a clean checkout but probably forgot lol

Shachar Itzhaky (Sep 21 2021 at 11:27):

too many subdirs, that's what happens

Shachar Itzhaky (Sep 21 2021 at 11:29):

tho I suppose if someone does pull and rebuild, they would expect the version number to be reflected as well.

Théo Zimmermann (Sep 21 2021 at 11:36):

Yeah, but from the point that you have manually run configure before, you have to re-run it every time you update.

Shachar Itzhaky (Sep 21 2021 at 11:36):

Oh ok but if I hadn't run configure, then ran dune build, then git pull, then dune build again -- it would update?

Shachar Itzhaky (Sep 21 2021 at 11:37):

that's acceptable.

Emilio Jesús Gallego Arias (Sep 21 2021 at 11:43):

Dune will re-run configure for example when the version has changed, tho you are correct, it should also re-run it in your case, a dependency may be missing in the promote rule for coq_config.ml

Théo Zimmermann (Sep 21 2021 at 11:49):

It the tree is not clean (configure output is there), will it really re-run configure?

Théo Zimmermann (Sep 21 2021 at 11:49):

I thought it was a fallback rule.

Emilio Jesús Gallego Arias (Sep 21 2021 at 11:52):

Indeed it will not, but maybe it should if configure.exe has changed?

Emilio Jesús Gallego Arias (Sep 21 2021 at 11:52):

Oh, but the problem is that Dune can't track the hash of the manual generation hash :/

Emilio Jesús Gallego Arias (Sep 21 2021 at 11:52):

Obviously

Emilio Jesús Gallego Arias (Sep 21 2021 at 13:42):

@Shachar Itzhaky , something still seems going on with the error handling; console gets an uncaught in promise for any error. At least, whatever it is going on, the error seems not to affect usability.

IMHO 8.14 branch is ready [modulo the possible problem with errors yet?] , so let me know when you cut 0.13.3 and we rebase and set 8.14 as default

Shachar Itzhaky (Sep 21 2021 at 13:43):

I have not been able to compile addons with 8.14. Ones with ML plugins don't compile, obviously, so I have disabled then; but one is just hanging forever (Hahn).

Emilio Jesús Gallego Arias (Sep 21 2021 at 13:47):

Umm, most addons should already have an 8.14 branch

Emilio Jesús Gallego Arias (Sep 21 2021 at 13:48):

Hanging in coqc? That seems like an interesting bug, you can actually run coqc under gdb and get a backtrace to see where's stuck

Shachar Itzhaky (Sep 21 2021 at 13:50):

Screen-Shot-2021-09-21-at-16.49.52.png
were you referring to this?

Emilio Jesús Gallego Arias (Sep 21 2021 at 14:02):

Yup!

Emilio Jesús Gallego Arias (Sep 21 2021 at 14:02):

Thanks for the screen shot

Shachar Itzhaky (Sep 21 2021 at 14:03):

That's always been there. It happens because CoqManager does not cleanup promises; can probably fix it at some point...

Shachar Itzhaky (Sep 21 2021 at 14:03):

A cancelled sid is essentially a rejected promise.

Shachar Itzhaky (Sep 21 2021 at 14:04):

Ok it hangs at rewrite !(Nat.add_mod k) here: https://github.com/vafeiadis/hahn/blob/22815da96d6db4287555ea3762d2d02fb670fdf7/HahnMinPath.v#L31

Emilio Jesús Gallego Arias (Sep 21 2021 at 14:08):

Thanks for the explanation; we are good then. Let me know if you need help with the addons; for hahn it seems like the rewrite ! is not terminating, which indeed can happen, the problem could come from many fronts, it'd be good if hahn would be added to Coq's CI so we don't have to deal with this.

Emilio Jesús Gallego Arias (Sep 21 2021 at 14:09):

I guess for now we'll have to disable it until we understand if that's a Coq problem or their bug in the first place

Shachar Itzhaky (Sep 21 2021 at 14:09):

it is in fact in the Docker CI.

Shachar Itzhaky (Sep 21 2021 at 14:09):

it's part of the affiliated addons build.

Emilio Jesús Gallego Arias (Sep 21 2021 at 18:04):

I did complete a rebase and some testing, looks pretty good IMHO; all that remains is the force push to v8.14 and setting the default branch, as not to have git issues I'll wait on your green light

Shachar Itzhaky (Sep 21 2021 at 18:44):

Ok, I will finish up 0.13.3 first. I have discovered an issue in SF; it is probably an issue with my build and not jsCoq (as it really hasn't changed much from 0.13.2), but I'm going to debug it first to make sure.

Shachar Itzhaky (Sep 21 2021 at 19:26):

ok looking good! Will make the release tomorrow and then I'll look at the v8.14 branch.

Shachar Itzhaky (Sep 23 2021 at 20:19):

You can go ahead and force-push your rebased branch.

Emilio Jesús Gallego Arias (Sep 24 2021 at 17:43):

Thanks @Shachar Itzhaky , just pushed the final rebase [I hope]

Emilio Jesús Gallego Arias (Sep 24 2021 at 17:43):

doing a bit more testing, and will setup the branch as default

Shachar Itzhaky (Sep 24 2021 at 17:43):

ok nice. I have a small patch to push as well, was waiting for the rebase (it's really tiny)

Emilio Jesús Gallego Arias (Sep 24 2021 at 17:45):

feel free to push atop of the branch already if you want

Shachar Itzhaky (Sep 24 2021 at 18:04):

actually it was two tiny things :)

Emilio Jesús Gallego Arias (Sep 24 2021 at 18:05):

Nice! default branch updated

Shachar Itzhaky (Sep 24 2021 at 18:17):

testing the docker now

Shachar Itzhaky (Sep 24 2021 at 18:19):

BTW did you notice I added the package mathcomp-extra? It's for libraries that are not included in the main mathcomp repo. Currently it is pretty small. What do you think we should put there? There are tons of packages in the GitHub org.

Emilio Jesús Gallego Arias (Sep 24 2021 at 18:19):

I'm not sure, I guess mathcom-analysis is pretty interesting these days, but should be it's own library maybe?

Shachar Itzhaky (Sep 24 2021 at 18:33):

hmm yeah maybe

Shachar Itzhaky (Sep 25 2021 at 14:36):

Oops. mathcomp-analysis seems to depend on hierarchy-builder, which depends on elpi...

Shachar Itzhaky (Sep 25 2021 at 14:39):

looks like Enrico did push some changes to coq-elpi yesterday about Coq 8.14

Enrico Tassi (Sep 25 2021 at 14:44):

Yes, on 8.14 you need coq-elpi 1.11.2, see also: https://github.com/coq/opam-coq-archive/pull/1827

Shachar Itzhaky (Sep 25 2021 at 17:57):

Great, it works! At least it builds lol :clown:

Shachar Itzhaky (Sep 27 2021 at 18:34):

Alright guys time for 0.14.0 alpha. https://coq-p-wr.vercel.app/
I'll add elpi back soon, and then try to add mathcomp-analysis as well.
Quickchick and equations still don't have 8.14-compatible branches.

Karl Palmskog (Sep 27 2021 at 18:37):

@Shachar Itzhaky Equations has been packaged for 8.14 based on a release: https://github.com/coq/opam-coq-archive/blob/f56f39bd23ced18945df79c101c1fc14c2e7b58c/extra-dev/packages/coq-equations/coq-equations.1.3%2B8.14/opam

Shachar Itzhaky (Sep 27 2021 at 18:38):

oh hmm ok let me try again with that branch then

Karl Palmskog (Sep 27 2021 at 18:38):

there is no associated branch to my knowledge, just a tag

Emilio Jesús Gallego Arias (Sep 27 2021 at 18:38):

Nice Shachar; note that some of the browsers we have around have trouble loading the .js file; they basically crash with

/node_modules/jscoq/…scoq_worker.bc.js:1   Uncaught RangeError: Maximum call stack size exceeded

Shachar Itzhaky (Sep 27 2021 at 18:38):

yeah, tag whatever :)

Shachar Itzhaky (Sep 27 2021 at 18:39):

Is this Chromium?

Karl Palmskog (Sep 27 2021 at 18:39):

same for Quickchick, it was released for 8.14 but there is no branch: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-quickchick/coq-quickchick.1.5.1/opam

Emilio Jesús Gallego Arias (Sep 27 2021 at 18:39):

Chromium indeed, so let's keep an eye, could be well that my version is just bugged

Emilio Jesús Gallego Arias (Sep 27 2021 at 18:40):

that's my main browser so it is quite "restricted"

Emilio Jesús Gallego Arias (Sep 27 2021 at 18:40):

Chromium
Versión 93.0.4577.82 (Build oficial) snap (64 bits)

Shachar Itzhaky (Sep 27 2021 at 18:40):

oh wow the equations release was 10 hours ago LOL

Karl Palmskog (Sep 27 2021 at 18:41):

tag was on Friday, release was today...

Shachar Itzhaky (Sep 27 2021 at 18:41):

yeah nice and timely

Shachar Itzhaky (Sep 27 2021 at 18:41):

I started working on the alpha last week so perhaps it was not there yet ;)

Karl Palmskog (Sep 27 2021 at 18:41):

the tag was made in response to Coq platform maintainer's request

Karl Palmskog (Sep 27 2021 at 18:42):

or as I like to call it, the magic whip/wand

Shachar Itzhaky (Sep 27 2021 at 18:43):

the majority whip!

Shachar Itzhaky (Sep 27 2021 at 18:43):

oh I see they also added Dune build support

Karl Palmskog (Sep 27 2021 at 18:43):

a very polite figurative whip though: https://github.com/mattam82/Coq-Equations/issues/427

Shachar Itzhaky (Sep 27 2021 at 18:45):

oh wait. Do I need HoTT now?

Karl Palmskog (Sep 27 2021 at 18:46):

no, the HoTT release for 8.14 is not out (though apparently an old release worked), so I disabled that in the Equations package for the time being

Shachar Itzhaky (Sep 27 2021 at 18:47):

how did you disable it? it's still trying to build it when I do dune build

Karl Palmskog (Sep 27 2021 at 18:49):

I don't think there is a way, based on how Emilio organizes the build. The regular build uses a flag to configure.sh.

Shachar Itzhaky (Sep 27 2021 at 18:49):

oh I thought the Dune files in the repo are the regular build now.

Karl Palmskog (Sep 27 2021 at 18:50):

we're trying to avoid Dune builds in releases for the time being, even though it was probably more inertia here

Shachar Itzhaky (Sep 27 2021 at 18:51):

ok anyway I guess rm theories/HoTT/dune will do for now :P

Emilio Jesús Gallego Arias (Sep 27 2021 at 18:52):

we are at 1400 commits, nice number to celebrate 0.14 XD

Shachar Itzhaky (Sep 27 2021 at 18:52):

heh cool

Shachar Itzhaky (Sep 27 2021 at 18:56):

btw Matthieu has a demo page with jsCoq, but it's a pretty old version (0.10), perhaps we can just include that demo on our website since we have the package already.

Emilio Jesús Gallego Arias (Sep 27 2021 at 18:59):

Sure

Emilio Jesús Gallego Arias (Sep 27 2021 at 18:59):

maybe the demo was even updated in the repos?

Shachar Itzhaky (Sep 27 2021 at 19:34):

probably yeah

Shachar Itzhaky (Sep 27 2021 at 19:35):

Ok epli question: Do you know how one can change the elpi search path? Currently the path contains ., ./., ./.., and a bunch of other directories. So there should be a way to add more right?

Shachar Itzhaky (Sep 27 2021 at 20:26):

seems to be no way other than to set the COQPATH environment variable. Oh well.

Shachar Itzhaky (Sep 27 2021 at 20:37):

Ok I failed with mathcomp-analysis for now :pensive:

Karl Palmskog (Sep 27 2021 at 20:38):

are you using the latest Hierarchy Builder release? I'm not sure mathcomp-analysis even builds on 8.14 yet.

Shachar Itzhaky (Sep 27 2021 at 20:39):

Ok that might be possible.

Shachar Itzhaky (Sep 27 2021 at 20:39):

I am using HB 1.2.0 which does build on 8.14.

Shachar Itzhaky (Sep 27 2021 at 20:40):

from 3 days ago

Karl Palmskog (Sep 27 2021 at 20:40):

that sounds like the right HB release, but unclear if it works with mathcomp-analysis, their CI doesn't test 8.14 yet.

Enrico Tassi (Sep 28 2021 at 05:44):

for elpi, why do you need to hack the path?

Shachar Itzhaky (Sep 28 2021 at 10:15):

:wave: @Enrico Tassi I am trying to build with Dune. I have a workspace containing several jsCoq addons; for some reason, when Dune runs Coq, the current working directory is the workspace root. So Elpi Accumulate is unable to find the sources...

Enrico Tassi (Sep 28 2021 at 10:42):

I see. I can patch that upstream, if there is a clean way for that.
Are you basing your work on https://github.com/LPCIC/coq-elpi/pull/82 ?

Shachar Itzhaky (Sep 28 2021 at 18:08):

Huh no actually was not aware of this PR.

Shachar Itzhaky (Sep 28 2021 at 18:09):

But I did ask Emilio's advice for some parts, esp. compiling the plugin. https://github.com/jscoq/addon-elpi

Shachar Itzhaky (Sep 28 2021 at 18:12):

In elpi (command-line) you can configure the path with -I. Currently coq-elpi uses Envvars.coqpath but adds /elpi at the end, which means the directory must be named elpi -- that's ok but a bit limiting. E.g. in HB the directory is called HB.

Enrico Tassi (Sep 28 2021 at 19:06):

Hum, I don't know your scenario, but these paths are needed only for compiling the .vo files, once a .elpi is accumulated inside the .vo file, the .elpi file is not needed anymore. So distributing HB should be trivial, if you can compile it.

Enrico Tassi (Sep 28 2021 at 19:07):

And I'm OK applying a patch that detects dune and adds dirname current_vo_file_path

Shachar Itzhaky (Sep 29 2021 at 20:33):

Yes, I understand. I could compile HB with coq_makefile and then package the .vos, but I have a whole setup with Dune so I kinda want it to be uniform :grinning:

Shachar Itzhaky (Sep 29 2021 at 20:35):

Enrico Tassi said:

And I'm OK applying a patch that detects dune and adds dirname current_vo_file_path

Thanks! Although I suppose that won't be what the user expects in all cases. It really should be the project directory (the one containing dune-project), as opposed to the workspace root which is currently the PWD. I assume Dune communicates that location somehow? @Emilio Jesús Gallego Arias ?

Emilio Jesús Gallego Arias (Sep 29 2021 at 21:24):

I think what Enrico is proposing is to have coq-elpi to use as search path the directory where the .vo file is; umm, for the rest I think it should just suffice to add the right flags? I'm not sure right now, but I made it work in one my dune patches.

Likely, to hack a solution as we speak, the easiest may be to just use copy_files

Shachar Itzhaky (Sep 30 2021 at 16:27):

oh I did not even consider copy_files. Good idea. My solution was way more horrible :face_palm:

Last updated: Apr 16 2024 at 19:01 UTC