jscoq/Lobby

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

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

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?

Where communities thrive

People

Repo info

Activity