Skip to content

Embed jsCoq in the Coq tutorial#3

Open
corwin-of-amber wants to merge 2 commits intomdnahas:masterfrom
corwin-of-amber:jscoq
Open

Embed jsCoq in the Coq tutorial#3
corwin-of-amber wants to merge 2 commits intomdnahas:masterfrom
corwin-of-amber:jscoq

Conversation

@corwin-of-amber
Copy link

@corwin-of-amber corwin-of-amber commented Feb 10, 2020

Hi!

I enclose the needed additions in order to make jsCoq operate in nahas_tutorial.html. (#2)

You can merge this PR, then run npm i in the root of your project to download the jsCoq distribution files and then commit the node_modules directory so that it is served as part of your Github pages website.

If you want to save about 40MB, you can delete node_modules/jscoq/coq-pkgs/mathcomp.coq-pkg before committing, since your tutorial does not use the mathcomp library.

@corwin-of-amber corwin-of-amber changed the title Embedded jsCoq in the Coq tutorial Embedd jsCoq in the Coq tutorial Feb 10, 2020
@corwin-of-amber corwin-of-amber changed the title Embedd jsCoq in the Coq tutorial Embed jsCoq in the Coq tutorial Mar 21, 2020
@corwin-of-amber
Copy link
Author

I noticed that jsCoq can now be used in "CDN"-like mode where you don't even need to install the package; you can direct the browser to jscoq.github.io. Of course, that means that you rely on whichever version is currently published, but I think for this tutorial this would work fine actually.

So I've updated the PR accordingly. I also keep a preview of it here:
https://corwin-of-amber.github.io/jscoq/tut/nahas/nahas_tutorial.html

(In the preview, I stole some styles from SF just for fun. It's not included in the PR.)

@mdnahas
Copy link
Owner

mdnahas commented Mar 24, 2020 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants