Comments (10)
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.
from mdnahas.github.io.
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.
from mdnahas.github.io.
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.
from mdnahas.github.io.
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.
from mdnahas.github.io.
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.
from mdnahas.github.io.
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).
from mdnahas.github.io.
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?
from mdnahas.github.io.
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.
from mdnahas.github.io.
@corwin-of-amber can't we have a version of node_modules
that only includes release-mode artifacts?
from mdnahas.github.io.
Tutorial (draft) is here:
https://github.com/corwin-of-amber/jscoq/blob/v8.11%2Btut-embed/docs/embedding.md
from mdnahas.github.io.
Related Issues (2)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from mdnahas.github.io.