by

Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
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
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
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?
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
Shachar Itzhaky
@corwin-of-amber
"requires" specifies the minimal version IIUC, so it should not trigger the alert, but dependbot may not be 100% accurate