Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Jan 22 22:22

    corwin-of-amber on v8.12

    [doc] Updated README. Misc thi… (compare)

  • Jan 21 12:23

    corwin-of-amber on v8.12

    [gfx] Icon enhancement. Fav ic… [port] Upgrade to Coq 8.12.1, a… [bugfix] Significant slowdown i… (compare)

  • Jan 19 18:03
    Matafou commented #215
  • Jan 19 18:01
    Matafou commented #215
  • Jan 19 17:53
    Matafou commented #215
  • Jan 19 08:15
    corwin-of-amber commented #216
  • Jan 19 08:10
    corwin-of-amber commented #216
  • Jan 18 10:01
    Matafou commented #215
  • Jan 17 11:45
    HKalbasi commented #216
  • Jan 16 14:27
    corwin-of-amber commented #216
  • Jan 16 14:25
    corwin-of-amber commented #216
  • Jan 16 14:14
    HKalbasi opened #216
  • Jan 12 17:20
    ejgallego commented #215
  • Jan 12 11:29
    Matafou commented #215
  • Jan 11 16:12
    ejgallego commented #215
  • Jan 09 16:09
    gasche commented #166
  • Jan 09 13:42

    corwin-of-amber on v8.12

    [bugfix] Avoid static member in… (compare)

  • Jan 05 17:49

    dependabot[bot] on npm_and_yarn

    (compare)

  • Jan 05 17:49

    corwin-of-amber on v8.12

    Bump ini from 1.3.5 to 1.3.8 B… Merge pull request #214 from js… (compare)

  • Jan 05 17:49
    corwin-of-amber closed #214
Emilio Jesús Gallego Arias
@ejgallego
seems a problem with the upload / coq version?
Shachar Itzhaky
@corwin-of-amber
ah hmm.
That's pretty fundamental. I definitely did test Induction.v.
ok that definitely happens now. Perhaps I updated jsCoq's binaries and forgot SF.
Shachar Itzhaky
@corwin-of-amber

ok that definitely happens now. Perhaps I updated jsCoq's binaries and forgot SF.

Yup. I compiled SF with rc4 by mistake :facepunch:

This part of the deployment is still pretty much manual :\
Emilio Jesús Gallego Arias
@ejgallego
Yup we should have the CI doing it
with github actions it's pretty simple now to:
  • build a docker image on each jscoq tag
  • trigger the build of the addons once that docker job is completed
Shachar Itzhaky
@corwin-of-amber
I am using my Dockerfile right now, so it should be easy to do. It is a single Dockerfile with stages, one for installing OPAM and deps, one for jsCoq, and one for addons.
Emilio Jesús Gallego Arias
@ejgallego
nice
Once that is setup I can also add a hook to keep collacoq updated
Shachar Itzhaky
@corwin-of-amber
I was actually thinking of integrating the collacoq page into jscoq.github.io. It's basically a scratchpad with the hastebin toolbar. Your code is implemented as a modification of hastebin's code with jsCoq plugged in, but it should be easier to pull out the toolbar from hastebin and stick it in our page. The server does not have to change, you can still host it on x80.org (with CORS enabled) or we can use some public platform such as Heroku (I have one running at https://hastbp.herokuapp.com).
Emilio Jesús Gallego Arias
@ejgallego
Sure it would be nice to improve this; maybe we should open an issue to outline the plan?
By the way did you tag the 0.12 release?
Shachar Itzhaky
@corwin-of-amber
oh, I did not. Wanna do it?
I can attach the dist tarball as always; problem is that now the tarball does not contain mathcomp. We can make a unified tarball of jscoq + addons for 0.12.1 maybe
currently the addons are still accessible, but you have to npm install them individually
Emilio Jesús Gallego Arias
@ejgallego
As you prefer, it does indeed make sense to have the addons in separate packages.
Shachar Itzhaky
@corwin-of-amber
Hey, can you take a look at some Coq issue I've been having?
Shachar Itzhaky
@corwin-of-amber
I tagged v0.12.0 to remember the point where we made the release. Do you want to create a Releases entry with the list of changes like you usually do?
Emilio Jesús Gallego Arias
@ejgallego
@corwin-of-amber would be great
Shachar Itzhaky
@corwin-of-amber
Oh I was suggesting that you do the honors since your name is on all the previous releases :)
Emilio Jesús Gallego Arias
@ejgallego
Oh sure I can do but IMHO it is time your name appears there :)
Shachar Itzhaky
@corwin-of-amber
lol ok I will do it :)
but it is your job to choose a tagline for 0.12.1
Emilio Jesús Gallego Arias
@ejgallego
:D
Stas Fomin
@belonesox
Hello! Just checkouted jscoq and trying to build it, «dune build»/«make jscoq» results «[ERROR] The selected switch jscoq+32bit is not installed.». What I am missed?
Shachar Itzhaky
@corwin-of-amber
Hi @belonesox, thank you for your interest in jsCoq! Before building, you need to setup the switch using the script ./etc/toolchain-setup.sh. See https://github.com/jscoq/jscoq/blob/v8.12/docs/build.md for detailed instructions.
Stas Fomin
@belonesox
@corwin-of-amber Sorry, I have read all "readmes" in root folder, and missed "docs". But I still failed with 32-bit toolchain (I have Fedora 32) → https://kopy.io/LkiNl
, config.log → https://kopy.io/zcOsU
Shachar Itzhaky
@corwin-of-amber
no worries. The docs are not glaringly easy to find -_-
it is possible that Fedora does not come with a multilib compiler. (E.g., try gcc -m32 hello.c.)
You may be able to install gcc-multilib. Alternatively you can choose the 64-bit route:
% ./etc/toolchain-setup.sh --64
Stas Fomin
@belonesox

OK, I tried 64bit-way. «./etc/toolchain-setup.sh --64» → OK.
But

«««
make jscoq
dune build @jscoq --workspace=/home/stas/projects/blockchain/jscoq//dune-workspace-64
make: execvp: dune: Permission denied
»»»

I see, that it tried to run «./dune», which does not look like executable, but as like DSL for building system.

What else I missed?

Shachar Itzhaky
@corwin-of-amber
it is not trying to run ./dune, but the program called dune, which is like GNU make for OCaml (and @ejgallego would add: for everything else too).
this program should have been installed by toolchain-setup.sh; perhaps your path is not set up for opam? try eval $(opam env)
Shachar Itzhaky
@corwin-of-amber
Hey @ejgallego and everyone, website now has 0.12.1-rc1. I will do a bit more testing and make this 0.12.1.
Emilio Jesús Gallego Arias
@ejgallego
Nice, thanks!
Yeah the toolchain for jscoq is not trivial, hopefully we will make everything work under docker soon
and make that the recommended system

the program called dune, which is like GNU make for OCaml (and @ejgallego would add: for everything else too)

Indeed it is a general-purpose build engine, a bit incomparable with make; if you follow the classification from "Build systems à la carte", Dune sits in an interesting spot; once the rule engine is declared stable and people use the API we will see how it works for other use cases; shake has been pretty popular for example.

IIANM most large projects have migrated from make long time ago, indeed make works really bad for one of the use cases Dune was designed for: build of large set of independent packages.

Shachar Itzhaky
@corwin-of-amber
I totally agree that make does not have what it takes anymore. The Software Foundations build process is one evidence to that.
Shachar Itzhaky
@corwin-of-amber
BTW there is a fully operational Dockerfile that also builds the addons in etc/docker.
Emilio Jesús Gallego Arias
@ejgallego
That we should recommend indeed :) I will even switch to it myself
Shachar Itzhaky
@corwin-of-amber
It is a bit of a bore to use during development, since it pulls the source from Github, which means you have to push to some branch before you can test your stuff. As for making releases, I have used this Docker setup exclusively since 0.12.0.
(which had four release candidates before actually being announced, making this automation very beneficial.)
Shachar Itzhaky
@corwin-of-amber
BTW I've been delaying the release of 0.12.1 because I don't know what to write in the tagline :P
Emilio Jesús Gallego Arias
@ejgallego
Tagline looks good to me :)

It is a bit of a bore to use during development, since it pulls the source from Github

I was thinking of actually using the image with the dev tools, but before the actual build is, and login into the dev env this way, I'll see.

Shachar Itzhaky
@corwin-of-amber
ah ok. The only issue is that jscoq.opam is in the repo and it is the ultimate source of all the dependencies that have to be installed from OPAM. So there is no clear install/build phase separation :( but you can make an image right after the "opam install".
Emilio Jesús Gallego Arias
@ejgallego
Good point, I wonder how to cleanly workaround this.
Shachar Itzhaky
@corwin-of-amber
Hello there @ejgallego, did you have a nice winter break?