Stream: jsCoq

Topic: 8.14


view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:42):

Hi @Shachar Itzhaky , so IIUC, we can wrap up the 8.13 series, correct?

view this post on Zulip Shachar Itzhaky (Sep 15 2021 at 11:42):

Yes, I have set the default version to 0.13.2.

view this post on Zulip Shachar Itzhaky (Sep 15 2021 at 11:43):

It was a minor bump because I had some trouble uploading 0.13.1 to NPM.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:43):

Ok I'll clean the milestones up and make the v8.14 branch the default

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:43):

what about the hotfix?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:43):

is that one included in 8.13.2 ?

view this post on Zulip Shachar Itzhaky (Sep 15 2021 at 11:44):

Yes. For 8.14 we should rethink it. It is commit 5c8ee304ca6904c2e895f965db9d12fc2a12e37e.

view this post on Zulip Shachar Itzhaky (Sep 15 2021 at 11:44):

Hmm actually the tag is one commit before that.

view this post on Zulip Shachar Itzhaky (Sep 15 2021 at 11:44):

So I might have patched it quickly on the website without updating the package :(

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:45):

Yup I was suspecting that, let's release 8.13.3 then

view this post on Zulip Shachar Itzhaky (Sep 15 2021 at 11:45):

Ok I want to see if there's a better way to solve this.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:47):

Ok, so that's why you keep open https://github.com/jscoq/jscoq/issues/249

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:47):

I do not recall the concrete problem there

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:47):

but IMHO having an "automaton" that reacts to Coq messages is not so bad

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:48):

if the tradeoff is to have more state in the clinet

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:48):

I am positive by talking to Makarius that this is a bad idea in the end

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:48):

turn out later or sooner, state between client and server gets desynced, Isabelle even has a call to reset everything

view this post on Zulip Emilio Jesús Gallego Arias (Sep 15 2021 at 11:48):

so 0 state, that's the real happiness

view this post on Zulip Shachar Itzhaky (Sep 15 2021 at 11:57):

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.

view this post on Zulip 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

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

but hopefully I get to it today

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

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

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

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 13:15):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 13:43):

XD

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 13:43):

Ok i was able to make SerAPI 8.14 work

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 13:43):

jsCoq should arrive soon

view this post on Zulip Shachar Itzhaky (Sep 16 2021 at 13:50):

Cool! I thought SerAPI worked already

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 13:53):

I know XD

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

but in chrome dev, it works

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

I dunno

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 14:52):

gonna have to do more cleanu

view this post on Zulip Shachar Itzhaky (Sep 16 2021 at 15:11):

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

view this post on Zulip Shachar Itzhaky (Sep 16 2021 at 15:22):

oh the patches are commented out

view this post on Zulip Shachar Itzhaky (Sep 16 2021 at 15:22):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 16:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 16:24):

was scary

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 16:24):

But we need to keep an eye on that

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2021 at 16:25):

Maybe we can release 0.14.0 tomorrow :D

view this post on Zulip Shachar Itzhaky (Sep 16 2021 at 16:49):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2021 at 11:49):

Great, thanks! I guess we can release?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Sep 17 2021 at 12:40):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 11:24):

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

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 11:24):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 11:27):

too many subdirs, that's what happens

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 11:37):

that's acceptable.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Sep 21 2021 at 11:49):

I thought it was a fallback rule.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 11:52):

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

view this post on Zulip 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 :/

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 11:52):

Obviously

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 13:47):

Umm, most addons should already have an 8.14 branch

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 13:50):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 14:02):

Yup!

view this post on Zulip Emilio Jesús Gallego Arias (Sep 21 2021 at 14:02):

Thanks for the screen shot

view this post on Zulip 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...

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 14:03):

A cancelled sid is essentially a rejected promise.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 14:09):

it is in fact in the Docker CI.

view this post on Zulip Shachar Itzhaky (Sep 21 2021 at 14:09):

it's part of the affiliated addons build.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Sep 23 2021 at 20:19):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 24 2021 at 17:43):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 24 2021 at 17:43):

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

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 24 2021 at 17:45):

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

view this post on Zulip Shachar Itzhaky (Sep 24 2021 at 18:04):

actually it was two tiny things :)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 24 2021 at 18:05):

Nice! default branch updated

view this post on Zulip Shachar Itzhaky (Sep 24 2021 at 18:17):

testing the docker now

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Shachar Itzhaky (Sep 24 2021 at 18:33):

hmm yeah maybe

view this post on Zulip Shachar Itzhaky (Sep 25 2021 at 14:36):

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

view this post on Zulip Shachar Itzhaky (Sep 25 2021 at 14:39):

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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Sep 25 2021 at 17:57):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:38):

oh hmm ok let me try again with that branch then

view this post on Zulip Karl Palmskog (Sep 27 2021 at 18:38):

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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:38):

yeah, tag whatever :)

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:39):

Is this Chromium?

view this post on Zulip 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

view this post on Zulip 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

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

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

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

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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:40):

oh wow the equations release was 10 hours ago LOL

view this post on Zulip Karl Palmskog (Sep 27 2021 at 18:41):

tag was on Friday, release was today...

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:41):

yeah nice and timely

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:41):

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

view this post on Zulip Karl Palmskog (Sep 27 2021 at 18:41):

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

view this post on Zulip Karl Palmskog (Sep 27 2021 at 18:42):

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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:43):

the majority whip!

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:43):

oh I see they also added Dune build support

view this post on Zulip Karl Palmskog (Sep 27 2021 at 18:43):

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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:45):

oh wait. Do I need HoTT now?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:49):

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

view this post on Zulip 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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:51):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2021 at 18:52):

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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 18:52):

heh cool

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2021 at 18:59):

Sure

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2021 at 18:59):

maybe the demo was even updated in the repos?

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 19:34):

probably yeah

view this post on Zulip 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?

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 20:26):

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

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 20:37):

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

view this post on Zulip 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.

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 20:39):

Ok that might be possible.

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 20:39):

I am using HB 1.2.0 which does build on 8.14.

view this post on Zulip Shachar Itzhaky (Sep 27 2021 at 20:40):

from 3 days ago

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Sep 28 2021 at 05:44):

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

view this post on Zulip 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...

view this post on Zulip 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 ?

view this post on Zulip Shachar Itzhaky (Sep 28 2021 at 18:08):

Huh no actually was not aware of this PR.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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: Jan 30 2023 at 19:04 UTC