Stream: Miscellaneous

Topic: jscoq and SF

view this post on Zulip Bas Spitters (Sep 05 2020 at 09:39):

The new SF on jscoq looks very beautiful. @Emilio Jesús Gallego Arias
However, there seems to be a dependency problem:
https://jscoq.github.io/ext/sf/lf/full/Induction.html
"Compiled library LF.Basics (in file /lib/LF/Basics.vo) makes inconsistent assumptions over library Coq.Init.Ltac"
Do you want me to create an issue?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:11):

Hi @Bas Spitters , thanks for the report, indeed I have checked this is not due to some caching issue, so I suggest you open an issue so @Shachar Itzhaky who is the SF maintainer can see it.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:11):

I wonder why the build went wrong tho.

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

@Emilio Jesús Gallego Arias perhaps it's time to move JsCoq and SerAPI to the Zulip? A joint stream?

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

otherwise we will get jsCoq and SerAPI questions spread out even more.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:13):

They are pretty separate projects IMO

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:13):

yeah maybe it is time, I'm still worried about the accesibility of Zulip tho

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:13):

well, we could work on setting up the HTML dumps during CUDW

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:15):

but sure, there can be different streams for jsCoq / SerAPI

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

Karl Palmskog said:

but sure, there can be different streams for jsCoq / SerAPI

Indeed I think it's best to separate, they projects will go in very different directions IMO; for SerAPI you and @Clément Pit-Claudel are the main contributors, so if you wanna move here I'm perfectly fine with the move, let's just update the README ; for jsCoq I'm OK if @Shachar Itzhaky is OK, last time we talked we decided to keep gitter but we can also move

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

OK then I vote for having a "SerAPI devs & users" stream. @Théo Zimmermann could you help us out?

view this post on Zulip Théo Zimmermann (Sep 07 2020 at 10:28):

Anyone can create a stream. You only need my help to rename it or modify its description.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:31):

OK that was indeed quite straightforward https://coq.zulipchat.com/#narrow/stream/256331-SerAPI-devs.20.26.20users -- as before, the main concern is just overload of different chat systems

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:35):

Thanks @Karl Palmskog , let's update the readme and post a gitter notice then

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:36):

OK, I can submit a README PR later today, maybe you can post on Gitter

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:37):

Sure

view this post on Zulip Shachar Itzhaky (Sep 07 2020 at 10:39):

Bas Spitters said:

The new SF on jscoq looks very beautiful. Emilio Jesús Gallego Arias
However, there seems to be a dependency problem:
https://jscoq.github.io/ext/sf/lf/full/Induction.html
"Compiled library LF.Basics (in file /lib/LF/Basics.vo) makes inconsistent assumptions over library Coq.Init.Ltac"
Do you want me to create an issue?

There was a glitch during the deploy process and the SF libs were indeed outdated relative to Coq's standard lib. It should be fixed now (you may have to clear your browser's cache to avoid getting the bad version).

view this post on Zulip Shachar Itzhaky (Sep 07 2020 at 10:41):

I have no problem with migrating to Zulip, the Gitter channel is mostly @Emilio Jesús Gallego Arias and me right now anyway... if this can get more traction from Coq users then sure we can move.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:42):

OK, then I can create "jsCoq devs & users" and invite the usual people if you give thumbs up as well @Emilio Jesús Gallego Arias

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:51):

Note the "jsCoq" vs "jsCoq devs and users"

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:52):

for example metacoq stream is just called "MetaCoq"

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:53):

Also "CertiCoq"

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:53):

IMHO visually, the short form is much easier to work with

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 10:53):

so I'd prefer the streams to be named just "SerAPI" and "jsCoq"

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

the "devs & users" overtakes IMO the main subject so the left list becomes cluttered and it is hard to locate for example vscoq or dune

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:55):

we settled on the "X devs & users" convention quite early, since some streams have separate dev and user streams. @Théo Zimmermann will have to change the name of the SerAPI stream

view this post on Zulip Théo Zimmermann (Sep 07 2020 at 11:08):

Renaming done. But yes, we're encouraging this naming scheme to clearly announce the intent of the streams (so that people know what questions are welcome).

view this post on Zulip Emilio Jesús Gallego Arias (Sep 07 2020 at 11:16):

Thanks @Théo Zimmermann , I dunno about the naming scheme, so far we have both choices in the stream; IMHO for small projects indeed that may not be worth it. I feel a big difference visually , but that's obviously a subjective criteria.

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

ok, it's done: https://coq.zulipchat.com/#narrow/stream/256336-jsCoq

Last updated: Jun 10 2023 at 06:31 UTC