Tutorial with JsCoq

[Zimmi48]

Hello,

I've just learned through @palmskog of the existence of https://corwin-of-amber.github.io/jscoq/tut/nahas/nahas_tutorial.html, a JsCoq-powered version of your Coq tutorial (by @corwin-of-amber and @ejgallego). Would it make sense to host this version at https://mdnahas.github.io/doc/nahas_tutorial instead of the current static version that is there? [Note that as of today, the links to your tutorial on the Coq documentation page point to the latter.]

[corwin-of-amber]

Hi, thanks for your interest in jsCoq, the version I put up is somewhat of a proof-of-concept and I'm still working on cleaning up a few hacks I had to make and solve a few minor bugs in jsCoq. But yes, I will be happy to help @mdnahas publish a stable version of it.

[mdnahas]

Thanks for the pointer, @Zimmi48!

@corwin-of-amber, Thanks for choosing my tutorial and making it easier to understand!

I've always thought that formal math needed a JavaScript-enabled implementation. It is much easier to recruit new people if they can see something without having to install software. I'd love to see Coq redesigned for web-native/networked use, but jsCoq looks like it will be enough to give new users a taste.

I'd be glad to host a jsCoq-enabled version of the tutorial. I'm glad to make any changes you request. I should definitely update the section "Seeing where you are in a proof" to explain jsCoq's controls.

BTW, is it possible to specify the version of Coq for jsCoq? There's been discussion of changing Coq's tactics and it sounded like the Coq authors may change a tactic that I use often in the tutorial. There is not an easy replacement for the tactic, so the tutorial might not work with future versions of Coq until I do a time-consuming rewrite. Making sure the tutorial runs in a version of Coq that can read it is important. Otherwise, readers may get confused.

Let me know how I can help.

[corwin-of-amber]

BTW, is it possible to specify the version of Coq for jsCoq?

Each version of jsCoq is bound to a particular version of Coq, so you can choose the version of jsCoq that suits your needs and install it. Using npm it is easy to specify which version you want. 8.11 seems to work well with your tutorial, we are still working on it but you might want to alpha-test as I fixed some bugs that I found while working on your tutorial.

[Zimmi48]

There's been discussion of changing Coq's tactics and it sounded like the Coq authors may change a tactic that I use often in the tutorial.

@mdnahas I think you are talking about case and elim. Don't worry, this is not going away anytime soon, and not without further discussion first (and then if it does happen, you'd be welcome to request help for the porting).

[mdnahas]

BTW, is it possible to specify the version of Coq for jsCoq?

Each version of jsCoq is bound to a particular version of Coq, so you can choose the version of jsCoq that suits your needs and install it. Using npm it is easy to specify which version you want.

I'm using github's static pages to host the tutorial. I haven't run a node server and I'm not sure how to do it. It looks like you're also using github.io. Can you point me to a webpage that describes how to get it working?

[corwin-of-amber]

No need to run a server. You can serve everything statically. The easiest way IMO is with npm. You do have to commit the node_modules directory, which can be around 130MB; sorry about that.

Why don't we do the following:

• I will make an alpha release based on my fixes for SF and your tutorial.
• I will write a small document describing how to acquire jsCoq through npm and how to embed it in your web page (there is quite a bit of boilerplate involved).

I can also fork your repo and make a PR which you can then review.

[corwin-of-amber]

I've posted an (internal) alpha release here.

You are welcome to experiment with it first, try this in a clean folder:

npm i https://github.com/corwin-of-amber/jscoq/releases/download/private%2Fv0.11.0-alpha1/jscoq-0.11.0-alpha1-npm.tar.gz

Then copy npm-template.html and edit it.

[ejgallego]

@corwin-of-amber can't we have a version of node_modules that only includes release-mode artifacts?

[corwin-of-amber]

We can try, but out of the 130MB, around 100MB is packages (.coq-pkg and .cma.js files) and 15MB are from external dependencies.

If you don't need mathcomp, you can save 40MB by deleting mathcomp.coq-pkg. If you don't need load/save functionality you can remove localforage and a few others I guess, but we will have to tweak our code to detect that these are missing and gracefully disable the features that depend on them.

Another approach could be to host jsCoq on some CDN that allows other sites to pull the packages from it.

[corwin-of-amber]

Tutorial (draft) is here:
https://github.com/corwin-of-amber/jscoq/blob/v8.11%2Btut-embed/docs/embedding.md