Where communities thrive

Join over 1.5M+ people
Join over 100K+ communities
Free without limits
Create your own community

Explore more communities

jscoq/Lobby

Welcome to the jsCoq developer channel, feel free to ask any question about jsCoq

People

Repo info

Activity

May 31 07:58

Ngoguey42 starred jscoq/jscoq
May 30 23:49

vollmerm starred jscoq/jscoq
May 30 06:50

ccianos starred jscoq/jscoq
May 29 07:23

mkanenobu starred jscoq/jscoq
May 23 07:27

Raiszo starred jscoq/jscoq
May 15 21:08

alexpantyukhin starred jscoq/jscoq
May 12 20:31

h908714124 starred jscoq/jscoq
May 05 21:40

elegaanz starred jscoq/jscoq
May 05 12:38

yzyzsun starred jscoq/jscoq
May 04 14:08

mobop starred jscoq/jscoq
Apr 30 15:32

ejgallego on v8.11

[readme] Fix link to Travis CI … (compare)
Apr 30 13:49

ejgallego on npm_and_yarn

(compare)
Apr 30 13:49

ejgallego on v8.11

Bump jquery from 3.4.0 to 3.5.0… Merge pull request #189 from js… (compare)
Apr 30 13:49

ejgallego closed #189
Apr 30 13:49

ejgallego commented #189
Apr 30 13:45

corwin-of-amber commented #189
Apr 30 13:44

ejgallego assigned #189
Apr 30 13:44

ejgallego commented #189
Apr 30 09:46

ik5 starred jscoq/jscoq
Apr 30 05:08

dannypsnl starred jscoq/jscoq

Emilio Jesús Gallego Arias

@ejgallego

Coq uses it for some parsing of warning flags

Also some stuff in Search uses it

did you see the thread about testing the new jsoo implementation?

Shachar Itzhaky

@corwin-of-amber

yes maybe it was for search, or perhaps Elpi depended on it?

Emilio Jesús Gallego Arias

@ejgallego

ocsigen/js_of_ocaml#976

Also elpi dependend on it

[new github notification interface is painful....]

Shachar Itzhaky

@corwin-of-amber

oh ok yeah I see that you already tested it

and with that new PR ocsigen/js_of_ocaml#998 we won't even need str.js

Shachar Itzhaky

@corwin-of-amber

the commit message mentioned that str.js was needed for splitting dirpaths. Not sure what I meant by that :)

Emilio Jesús Gallego Arias

@ejgallego

likely turning Coq.Init.Notations into [Coq;Init;Notations]

Shachar Itzhaky

@corwin-of-amber

urm how do I pin a pull request? I forgot :sob:
I tried: opam pin add js_of_ocaml git+https://github.com/ocsigen/js_of_ocaml.git#998

Emilio Jesús Gallego Arias

@ejgallego

I pin the original tree

Emilio Jesús Gallego Arias

@ejgallego

I use hub pr list -f '%I: %au/%H%n'to extract the branch but it is still not optimal :S

so in this case

https://github.com/hhugo/js_of_ocaml.git#str

hub checkout <pr-url> works pretty well when I want to review stuff

also I can pin locally once the branch is there

Shachar Itzhaky

@corwin-of-amber

thx

Emilio Jesús Gallego Arias

@ejgallego

you are welcome!

Shachar Itzhaky

@corwin-of-amber

Oh looks like lf in your page (at x80.org) is empty

Emilio Jesús Gallego Arias

@ejgallego

Yes that build is bugged I'll redirect

One reason I was still keeping my builds is as to have url-stable versioned jscoq

Will see if I can do with npm

Shachar Itzhaky

@corwin-of-amber

Sure, npm is easy; but I haven't made a package for SF stuff

Shachar Itzhaky

@corwin-of-amber

Hi, I have started this repo for building addons outside of the jsCoq source tree: https://github.com/jscoq/addons

I have split it into smaller projects with Makefiles that fetch and compile (with dune where I managed to do it) the addons, then creates .coq-pkg files for them.

Not entirely sure that this organization is sensible as these modules are rather small... but I wanted it to be modular so that essentially you can update only the ones you wish to build.

(sfdev in particular is a private repo, so only members can clone it; currently there is no public-safe repo, only downloadable tarballs and they are pretty old)

Emilio Jesús Gallego Arias

@ejgallego

Hi @corwin-of-amber , looks pretty good; for SF for example in Coq we use a link to the CircleCI artifact, maybe that would work here? I guess otherwise that's fine, tho maybe using the tarball would more sensible in the end as this is something people may want to build?

actually I'm quite convinced we could just push the changes upstream and avoid the local repos

Shachar Itzhaky

@corwin-of-amber

The only thing I'm not sure maintainers would like to have at this point is the .coq-pkg file generation step.

For SF, the common use case that I see is instructors using it for their lectures, which would be awesome. Such instructors do tend to make local modifications to their book sources and would like to build their versions.

Emilio Jesús Gallego Arias

@ejgallego

The only thing I'm not sure maintainers would like to have at this point is the .coq-pkg file generation step.

That rule is simple enough that we'll add it to dune, otherwise we could indeed add it to the project's dune files tho

as long as we mark it optional, so if jscoq-packer is not in scope

it is not run

Shachar Itzhaky

@corwin-of-amber

oh ok

Emilio Jesús Gallego Arias

@ejgallego

not sure if a rule can be optional

let me see

for sure we should push all dune-files upstream

Emilio Jesús Gallego Arias

@ejgallego

not sure if a rule can be optional

Seems not but that should be Ok

Shachar Itzhaky

@corwin-of-amber

I fixed jscoq.github.io, but somehow it still shows as an alert.

Emilio Jesús Gallego Arias

@ejgallego

where?

Shachar Itzhaky

@corwin-of-amber

https://github.com/jscoq/jscoq.github.io/network/alerts

Emilio Jesús Gallego Arias

@ejgallego

I think there still is an insecure dep on the jscoq field, isn't it?

Shachar Itzhaky

@corwin-of-amber

that may be the case. it does not specify which field. I guess this will be fixed with the next NPM release; for now, the version of jquery that is actually installed is 3.5.0, so no need to worry about the security issue

(anyway, the vulnerability is ACE, so for a page that does not contain any private or sensitive data, the risk is minimal.)

Emilio Jesús Gallego Arias

@ejgallego

that's the problematic line, isn't it https://github.com/jscoq/jscoq.github.io/blob/master/package-lock.json#L109 ?

Shachar Itzhaky

@corwin-of-amber

guess so, but notice that https://github.com/jscoq/jscoq.github.io/blob/6fb9b5a88c8766a2b7c1e48a1fa4b9bebc13fa06/package-lock.json#L95 does say 3.5.0

"requires" specifies the minimal version IIUC, so it should not trigger the alert, but dependbot may not be 100% accurate