Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • hamelin/jscoq-light
  • rousselin/jscoq-light
2 results
Show changes
Commits on Source (34)
Hide whitespace changes
Inline Side-by-side
Showing
with 484 additions and 226 deletions
.gitlab-ci.yml 0 → 100644
View file @ 2a40a0b1
stages:
- build
jscoq:
stage: build
image: i386/debian
script:
- apt update && apt upgrade && apt install -y curl git make nodejs wget gcc unzip rsync g++-multilib gcc-multilib libgmp-dev bzip2 npm zip
- wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh && chmod +x install.sh && bash -c "printf '\n' | ./install.sh" && opam init -y --disable-sandboxing
- echo "test -r '/root/.opam/opam-init/init.sh' && . '/root/.opam/opam-init/init.sh' > /dev/null 2> /dev/null || true" >> ~/.bashrc
- ./etc/toolchain-setup.sh && make coq && make jscoq && npm link
- source ~/.bashrc
- make addons
- cp coqdoclight.py _build/jscoq+32bit/
- cp coqdoclight_sample.v _build/jscoq+32bit/
- zip -r jscoq.zip _build/jscoq+32bit/
when: manual
artifacts:
paths:
- jscoq.zip
expire_in: never
.gitmodules deleted 100644 → 0
View file @ f2fb5884
[submodule "CodeMirror-TeX-input"]
path = frontend/classic/external/CodeMirror-TeX-input
url = https://github.com/ejgallego/CodeMirror-TeX-input.git
[submodule "vendor/coq-serapi"]
path = vendor/coq-serapi
url = https://github.com/ejgallego/coq-serapi.git
CHANGES.md
View file @ 2a40a0b1
# jsCoq 0.17.0
--------------
# jsCoq 0.17.1 "Night slip"
---------------------------
- Update to Coq 8.17.1. (@ejgallego)
- Fix some dist mishaps - missing CLI, zarith version change
(@corwin-of-amber)
# jsCoq 0.17.0 "Rocker style"
-----------------------------
- Update to Coq 8.17.0. (@corwin-of-amber)
- Add support for saving and loading scratchpad snippets using Gist (@Eladkay)
......
Dockerfile 0 → 100644
View file @ 2a40a0b1
FROM i386/debian AS jscoq-dev
CMD ["/usr/bin/python3", "-m", "http.server", "-d", "/root/jscoq", "8000" ]
RUN apt update && apt upgrade && apt install -y curl git make nodejs wget gcc unzip rsync g++-multilib gcc-multilib libgmp-dev bzip2 npm
RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh && chmod +x install.sh && bash -c "printf '\n' | ./install.sh" && opam init -y --disable-sandboxing
RUN echo "test -r '/root/.opam/opam-init/init.sh' && . '/root/.opam/opam-init/init.sh' > /dev/null 2> /dev/null || true" >> ~/.bashrc
Makefile
View file @ 2a40a0b1
......@@ -89,6 +89,9 @@ all:
@echo " coq: download and build Coq and addon libraries"
@echo " install: install Coq version used by jsCoq to ~/.opam/$(BUILD_CONTEXT)"
addons: force
cd addons && make
jscoq: force
$(DUNE) build @jscoq $(DUNE_FLAGS)
......@@ -176,7 +179,7 @@ distclean: clean
dist: dist-npm dist-tarball
BUILDOBJ = ${addprefix $(BUILDDIR)/./, \
jscoq.js coq-pkgs frontend backend dist examples docs}
jscoq.js coq-pkgs frontend backend dist dist-cli dist-webpack examples docs}
DISTOBJ = README.md index.html package.json package-lock.json $(BUILDOBJ)
DISTDIR = _build/dist
......
README.md
View file @ 2a40a0b1
Run the Coq Proof Assistant in your browser!
------------------------
jscoq light
--------------------
![Build Status](https://github.com/jscoq/jscoq/actions/workflows/ci.yml/badge.svg)
A trimmed down version of jscoq for teaching purposes.
jsCoq is an Online Integrated Development Environment for the
[Coq](https://coq.inria.fr) proof assistant and runs in your browser!
We aim to enable new UI/interaction possibilities and to improve the
accessibility of the Coq platform itself. Current stable version is
jsCoq 0.16.1 supporting Coq 8.16.0, try it:
### First time setup
<https://coq.vercel.app>
- Install docker. Docker requires `sudo` by default, because it uses `chroot` to create a lightweight "virtual machine".
If you are not comfortable with this, there exists an experimental [rootless version of Docker ](https://docs.docker.com/engine/security/rootless/). However, I haven't yet tested whether it works.
jsCoq is written to conform to ES2017; any recent standard-compliant
browser should be able to run it. No servers or external programs are needed.
See the [Troubleshooting](#Troubleshooting) section if you have problems.
jsCoq is community-developed by a [team of contributors](#Credits).
## Are you a jsCoq user?
Have you developed or taught a course **using jsCoq**? Do you have some feedback for us?
If so, please submit a pull request or an issue so we can add your
lectures to the list of [jsCoq users](#jsCoq-Users). This is essential
to guarantee future funding of the project.
## Basic Usage
The main page showcases jsCoq by walking through a proof for the infinitude of primes using
[`math-comp`](https://github.com/math-comp/math-comp), due to Georges Gonthier.
Once jsCoq finishes loading, you can step through the proof using the
arrow buttons on the toolbar (top right), or using these keyboard
shortcuts:
| Shortcut | Action |
|--------------------|------------------|
| Alt-N or Alt-↓ | Go to next |
| Alt-P or Alt-↑ | Go to previous |
| Alt-Enter or Alt-→ | Go to cursor |
You can open a blank editor and experiment with your own Coq developments using the
[scratchpad](https://coq.vercel.app/scratchpad.html).
The same keyboard shortcuts apply here.
The scratchpad's contents are saved in your browser's local storage (IndexedDB, specifically),
so they are not lost if you close the browser window or refresh the page.
You can, in fact, store more than one document using the local open/save file dialogs:
| Shortcut | Action |
|--------------------|------------------------------------------------------------------------------|
| Ctrl-S | Save file (with the last name provided, or `untitled.v`) |
| Ctrl-Shift-S | Save file as (prompts for file name; also has options to download or share the content) |
| Ctrl-Alt-S | Save file to disk (using the browser's Save dialog, or preset destination) |
| Ctrl-O | Open file (prompts for file name, supports tab completion) |
| Ctrl-Alt-O | Open file from disk (using the browser's Open dialog) |
On Mac, replace Ctrl with ⌘ (command) and Alt with ⌥ (option), as is traditional.
Drag `.v` files from your local drive onto the scratchpad to open them.
You can also drag multiple files, which will open up a project pane to the left of the editor, allowing you to switch between them; this functionality is still experimental.
### Sharing your development
A small pastebin-like server based on [Hastebin](https://hastebin.com) is available for sharing `.v` files between users.
Open the save dialog (Ctrl-Shift-S) and click "Share"; then share the URL from your browser's location bar with anyone you like.
The URL represents the state of the document at the moment it was shared, and this state is read-only. Every time you click "Share", a fresh URL is generated.
Shared content is not saved forever, though; documents are typically available for a period of ~30 days.
## How to build your own jsCoq documents
See the [dedicated page](docs/embedding.md) for information on advanced
options and jsCoq HTML embedding API. A quick setup can be done with:
- In the root of the project run `sudo docker build --tag jscoq-dev-image .` this will take a while.
- While still in the root of the project, create a container using
```
$ npm install jscoq
sudo docker container create -p 8000:8000 --mount type=bind,source=.,target=/root/jscoq --name jscoq-dev jscoq-dev-image
```
then copy and adapt the [template page](https://github.com/ejgallego/jscoq/blob/v8.14/examples/npm-template.html)
page to your needs.
*For a more detailed tutorial and information, refer to* [docs/embedding.md](docs/embedding.md).
## Contributing and Developer Information
See the [dedicated page](docs/developing.md) for developer information
as well as links to past versions and tools.
This is a beta-status project, but any contribution or comment is
really welcome! See [the contributing guide](CONTRIBUTING.md) for more
information.
## Publications
See the [dedicated file](docs/papers.md)
## Examples
The main page includes a proof of the infinitude of primes by
G. Gonthier. We provide some more examples as a showcase of the tool:
- The Software Foundations suite (so far, LF and PLF volumes):
+ https://jscoq.github.io/ext/sf
- Mike Nahas's Coq Tutorial: https://corwin-of-amber.github.io/jscoq/tut/nahas/nahas_tutorial.html
### Outdated examples [but still working]
- dft.v: https://x80.org/rhino-coq/v8.11/examples/dft.html
A small development of the theory of the Fourier Transform following
Julius Orion Smith III's "The Mathematics of the Discrete Fourier
Transform"
- equations: https://x80.org/rhino-coq/v8.11/examples/equations_intro.htmla
Introduction to the [Coq Equations](https://github.com/mattam82/Coq-Equations) package from
the official documentation.
- The IRIS program logic, by Robbert Krebbers et al.
https://x80.org/rhino-coq/v8.9/examples/iris.html
- Mtac: The Mtac tutorial by Beta Zilliani:
https://x80.org/rhino-coq/v8.5/examples/mtac_tutorial.html
- StackMachine: The First chapter of the book "Certified Programming
with Dependent Types" by Adam Chlipala:
https://x80.org/rhino-coq/v8.5/examples/Cpdt.StackMachine.html
- MirrorCore:
- A simple demo:
https://x80.org/rhino-coq/v8.5/examples/mirrorcore.html
- A demo of developing a cancellation algorithm for commutative
monoids:
https://x80.org/rhino-coq/v8.5/examples/mirror-core-rtac-demo.html
## jsCoq Users:
Incomplete list of places where jsCoq has been used:
* Coq Winter School 2016: “Advanced Software Verification And Computer Proof”. _Sophia Antipolis_
https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/
* Coq Winter School 2016-2017 (SSReflect & MathComp) “Advanced
Software Verification And Computer Proof”. _Sophia Antipolis_
https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016-2017/
* Mathematical Components, an Introduction, _Satellite workshop of the ITP 2016 conference_, August 27th, Nancy, France
https://github.com/math-comp/wiki/wiki/tutorial-itp2016
* Several examples of the "Mathematical Components Book" https://math-comp.github.io/mcb/
* School on "Preuves et Programmes" at l'École de Mines https://www-sop.inria.fr/marelle/mines/
* Mini Corso di Coq a Pavoda: http://www-sop.inria.fr/members/Enrico.Tassi/padova2017/
* Elpi Tutorial / Demo at CoqPL 2017 _Los Angeles_ https://lpcic.github.io/coq-elpi-www/tutorial-demo_CoqPL2018.html
* Coq Winter School 2017-2018 (SSReflect & MathComp) _Sophia Antipolis_ https://team.inria.fr/marelle/en/coq-winter-school-2017-2018-ssreflect-mathcomp/
* Lectures at the "Journées Nationales du Calcul Formel" by Assia Mahboubi:
https://specfun.inria.fr/amahboub/Jncf18/cours2.html
* [Types Summer School](https://sites.google.com/view/2018eutypesschool/home): http://www-sop.inria.fr/teams/marelle/types18/
* Coq Winter School 2018-2019 (SSReflect & MathComp) https://team.inria.fr/marelle/en/coq-winter-school-2018-2019-ssreflect-mathcomp/
* CASS 2020, Coq Andes Summer School https://cass.pleiad.cl/
* [Lectures on Separation Logic](https://madiot.fr/sepcourse/) by Jean-Marie Madiot in MPRI's course "Proofs of programs", using Arthur Charguéraud's material. [See it in action!](https://madiot.fr/sepcourse/coq/)
* [EPIT 2020 - Spring School on Homotopy Type Theory](https://github.com/HoTT/EPIT-2020)
### jsCoq in the press
- http://www.mines-paristech.fr/Actualites/jsCoq-ou-Coq-dans-un-navigateur/2118
- https://news.ycombinator.com/item?id=9836900
### Addon Packages
One of jsCoq's strengths is its support for bundling addon
packages. In order to add your Coq package to jsCoq, you need to compile
it with jsCoq's version of Coq.
Head over to [jscoq/addons](https://github.com/jscoq/addons) for pointers to
some well-known packages that have been compiled for jsCoq and are bundled
with every version of jsCoq.
You can use these as examples for bundling your own libraries.
## Troubleshooting
**Are you getting a `StackOverflow` exception?** Unfortunately these
are hard to fix; you may be stuck with them for a while.
* Clearing the browser cache usually solves lots of issues.
* Change browser, if using Firefox try Chrome, if using Chrome try Firefox.
### Reporting Bugs ###
Feel free to use the issue tracker. Please include your
browser/OS/user-agent and any command-line options.
### Contact and on-line help ###
- [jsCoq's Zulip Room](https://coq.zulipchat.com/#narrow/stream/256336-jsCoq), main developer chat
- [jsCoq's gitter](https://gitter.im/jscoq/Lobby), legacy developer chat
- [Coq's discourse](https://coq.discourse.group/) [use the jscoq tag], for general announcements and questions
- [StackOverflow](https://stackoverflow.com/) [use the jscoq tag]
### What is broken ###
* Loading ML modules is slow.
* Loading `.vo` files is slow.
* There surely are threading and performance problems.
* `vm_compute` and `native_compute` fall back to regular `compute`.
- You can now start the container using `sudo docker container start jscoq-dev`. This runs a web server hosting your local version of jscoq on port 8000. You can stop it using `sudo docker container stop jscoq-dev`.
## Documents
- After the container has been started, run `sudo docker exec -it jscoq-dev bash -c "cd /root/jscoq && ./etc/toolchain-setup.sh && make coq && make jscoq && npm link"` to compile everything for the first time
See the `etc/notes/` directory for some random notes about the project.
### Compiling jscoq
## Credits
- Make sure the container is started by running `sudo docker container start jscoq-dev`
### Core developer team
- Run `sudo docker exec -it jscoq-dev bash` : you are now in a shell inside the container.
- [Emilio Jesús Gallego Arias](https://www.irif.fr/~gallego/) , Inria, Université de Paris, IRIF
- [Shachar Itzhaky](https://cs.technion.ac.il/~shachari/) , Technion
- `cd /root/jscoq` to enter to the `jscoq` directory source.
This is a bind mount, meaning `/root/jscoq` inside the container is actually the same directory as the git repository on your machine. You can edit the source code of jscoq outside of the container and the changes will be reflected inside the container.
### Past Contributors
- To compile jscoq, run `make jscoq`. The result will be saved in `_build/jscoq+32bit`. You can upload this directory to a web server; it contains an `index.html` which should work in your browser.
- Benoît Pin, [CRI, MINES ParisTech](https://www.cri.ensmp.fr)
- You don't need to copy this directory to a web server to test your version, [the docker container runs a web server for this purpose](http://localhost:8000/_build/jscoq%2B32bit/).
## Acknowledgements
![FEEVER Logo](/frontend/classic/images/feever-logo.png?raw=true "Feever Logo")
### Adding your own Coq files
jsCoq was made possible thanks to funding by the
[FEEVER](http://feever.fr) project and support from [MINES
ParisTech](http://www.mines-paristech.eu)
You can add your own Coq files in the directory `./addons/teach/workdir/theories/` if you recompile jscoq (using `make jscoq`) they will be compiled.
You can compile only your files using `make addons` at the root of the directory inside the container.
We want to _strongly thank_ the `js_of_ocaml` developers. Without
their great and quick support jsCoq wouldn't have been possible.
Then, you will be able to use `From Teach Require Import YourFile` in jscoq.
[CodeMirror](https://codemirror.net/) has played a crucial role in the
project, we are very happy with it, thanks a lot!
### Creating your own worksheets
Please consider supporting the development of CodeMirror with a donation.
You can modify `index.html` to create your own worksheet.
(TODO: expand on this).
README.original.md 0 → 100644
View file @ 2a40a0b1
Run the Coq Proof Assistant in your browser!
------------------------
![Build Status](https://github.com/jscoq/jscoq/actions/workflows/ci.yml/badge.svg)
jsCoq is an Online Integrated Development Environment for the
[Coq](https://coq.inria.fr) proof assistant and runs in your browser!
We aim to enable new UI/interaction possibilities and to improve the
accessibility of the Coq platform itself. Current stable version is
jsCoq 0.16.1 supporting Coq 8.16.0, try it:
<https://coq.vercel.app>
jsCoq is written to conform to ES2017; any recent standard-compliant
browser should be able to run it. No servers or external programs are needed.
See the [Troubleshooting](#Troubleshooting) section if you have problems.
jsCoq is community-developed by a [team of contributors](#Credits).
## Are you a jsCoq user?
Have you developed or taught a course **using jsCoq**? Do you have some feedback for us?
If so, please submit a pull request or an issue so we can add your
lectures to the list of [jsCoq users](#jsCoq-Users). This is essential
to guarantee future funding of the project.
## Basic Usage
The main page showcases jsCoq by walking through a proof for the infinitude of primes using
[`math-comp`](https://github.com/math-comp/math-comp), due to Georges Gonthier.
Once jsCoq finishes loading, you can step through the proof using the
arrow buttons on the toolbar (top right), or using these keyboard
shortcuts:
| Shortcut | Action |
|--------------------|------------------|
| Alt-N or Alt-↓ | Go to next |
| Alt-P or Alt-↑ | Go to previous |
| Alt-Enter or Alt-→ | Go to cursor |
You can open a blank editor and experiment with your own Coq developments using the
[scratchpad](https://coq.vercel.app/scratchpad.html).
The same keyboard shortcuts apply here.
The scratchpad's contents are saved in your browser's local storage (IndexedDB, specifically),
so they are not lost if you close the browser window or refresh the page.
You can, in fact, store more than one document using the local open/save file dialogs:
| Shortcut | Action |
|--------------------|------------------------------------------------------------------------------|
| Ctrl-S | Save file (with the last name provided, or `untitled.v`) |
| Ctrl-Shift-S | Save file as (prompts for file name; also has options to download or share the content) |
| Ctrl-Alt-S | Save file to disk (using the browser's Save dialog, or preset destination) |
| Ctrl-O | Open file (prompts for file name, supports tab completion) |
| Ctrl-Alt-O | Open file from disk (using the browser's Open dialog) |
On Mac, replace Ctrl with ⌘ (command) and Alt with ⌥ (option), as is traditional.
Drag `.v` files from your local drive onto the scratchpad to open them.
You can also drag multiple files, which will open up a project pane to the left of the editor, allowing you to switch between them; this functionality is still experimental.
### Sharing your development
A small pastebin-like server based on [Hastebin](https://hastebin.com) is available for sharing `.v` files between users.
Open the save dialog (Ctrl-Shift-S) and click "Share"; then share the URL from your browser's location bar with anyone you like.
The URL represents the state of the document at the moment it was shared, and this state is read-only. Every time you click "Share", a fresh URL is generated.
Shared content is not saved forever, though; documents are typically available for a period of ~30 days.
## How to build your own jsCoq documents
See the [dedicated page](docs/embedding.md) for information on advanced
options and jsCoq HTML embedding API. A quick setup can be done with:
```
$ npm install jscoq
```
then copy and adapt the [template page](https://github.com/ejgallego/jscoq/blob/v8.14/examples/npm-template.html)
page to your needs.
*For a more detailed tutorial and information, refer to* [docs/embedding.md](docs/embedding.md).
## Contributing and Developer Information
See the [dedicated page](docs/developing.md) for developer information
as well as links to past versions and tools.
This is a beta-status project, but any contribution or comment is
really welcome! See [the contributing guide](CONTRIBUTING.md) for more
information.
## Publications
See the [dedicated file](docs/papers.md)
## Examples
The main page includes a proof of the infinitude of primes by
G. Gonthier. We provide some more examples as a showcase of the tool:
- The Software Foundations suite (so far, LF and PLF volumes):
+ https://jscoq.github.io/ext/sf
- Mike Nahas's Coq Tutorial: https://corwin-of-amber.github.io/jscoq/tut/nahas/nahas_tutorial.html
### Outdated examples [but still working]
- dft.v: https://x80.org/rhino-coq/v8.11/examples/dft.html
A small development of the theory of the Fourier Transform following
Julius Orion Smith III's "The Mathematics of the Discrete Fourier
Transform"
- equations: https://x80.org/rhino-coq/v8.11/examples/equations_intro.htmla
Introduction to the [Coq Equations](https://github.com/mattam82/Coq-Equations) package from
the official documentation.
- The IRIS program logic, by Robbert Krebbers et al.
https://x80.org/rhino-coq/v8.9/examples/iris.html
- Mtac: The Mtac tutorial by Beta Zilliani:
https://x80.org/rhino-coq/v8.5/examples/mtac_tutorial.html
- StackMachine: The First chapter of the book "Certified Programming
with Dependent Types" by Adam Chlipala:
https://x80.org/rhino-coq/v8.5/examples/Cpdt.StackMachine.html
- MirrorCore:
- A simple demo:
https://x80.org/rhino-coq/v8.5/examples/mirrorcore.html
- A demo of developing a cancellation algorithm for commutative
monoids:
https://x80.org/rhino-coq/v8.5/examples/mirror-core-rtac-demo.html
## jsCoq Users:
Incomplete list of places where jsCoq has been used:
* Coq Winter School 2016: “Advanced Software Verification And Computer Proof”. _Sophia Antipolis_
https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/
* Coq Winter School 2016-2017 (SSReflect & MathComp) “Advanced
Software Verification And Computer Proof”. _Sophia Antipolis_
https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016-2017/
* Mathematical Components, an Introduction, _Satellite workshop of the ITP 2016 conference_, August 27th, Nancy, France
https://github.com/math-comp/wiki/wiki/tutorial-itp2016
* Several examples of the "Mathematical Components Book" https://math-comp.github.io/mcb/
* School on "Preuves et Programmes" at l'École de Mines https://www-sop.inria.fr/marelle/mines/
* Mini Corso di Coq a Pavoda: http://www-sop.inria.fr/members/Enrico.Tassi/padova2017/
* Elpi Tutorial / Demo at CoqPL 2017 _Los Angeles_ https://lpcic.github.io/coq-elpi-www/tutorial-demo_CoqPL2018.html
* Coq Winter School 2017-2018 (SSReflect & MathComp) _Sophia Antipolis_ https://team.inria.fr/marelle/en/coq-winter-school-2017-2018-ssreflect-mathcomp/
* Lectures at the "Journées Nationales du Calcul Formel" by Assia Mahboubi:
https://specfun.inria.fr/amahboub/Jncf18/cours2.html
* [Types Summer School](https://sites.google.com/view/2018eutypesschool/home): http://www-sop.inria.fr/teams/marelle/types18/
* Coq Winter School 2018-2019 (SSReflect & MathComp) https://team.inria.fr/marelle/en/coq-winter-school-2018-2019-ssreflect-mathcomp/
* CASS 2020, Coq Andes Summer School https://cass.pleiad.cl/
* [Lectures on Separation Logic](https://madiot.fr/sepcourse/) by Jean-Marie Madiot in MPRI's course "Proofs of programs", using Arthur Charguéraud's material. [See it in action!](https://madiot.fr/sepcourse/coq/)
* [EPIT 2020 - Spring School on Homotopy Type Theory](https://github.com/HoTT/EPIT-2020)
### jsCoq in the press
- http://www.mines-paristech.fr/Actualites/jsCoq-ou-Coq-dans-un-navigateur/2118
- https://news.ycombinator.com/item?id=9836900
### Addon Packages
One of jsCoq's strengths is its support for bundling addon
packages. In order to add your Coq package to jsCoq, you need to compile
it with jsCoq's version of Coq.
Head over to [jscoq/addons](https://github.com/jscoq/addons) for pointers to
some well-known packages that have been compiled for jsCoq and are bundled
with every version of jsCoq.
You can use these as examples for bundling your own libraries.
## Troubleshooting
**Are you getting a `StackOverflow` exception?** Unfortunately these
are hard to fix; you may be stuck with them for a while.
* Clearing the browser cache usually solves lots of issues.
* Change browser, if using Firefox try Chrome, if using Chrome try Firefox.
### Reporting Bugs ###
Feel free to use the issue tracker. Please include your
browser/OS/user-agent and any command-line options.
### Contact and on-line help ###
- [jsCoq's Zulip Room](https://coq.zulipchat.com/#narrow/stream/256336-jsCoq), main developer chat
- [jsCoq's gitter](https://gitter.im/jscoq/Lobby), legacy developer chat
- [Coq's discourse](https://coq.discourse.group/) [use the jscoq tag], for general announcements and questions
- [StackOverflow](https://stackoverflow.com/) [use the jscoq tag]
### What is broken ###
* Loading ML modules is slow.
* Loading `.vo` files is slow.
* There surely are threading and performance problems.
* `vm_compute` and `native_compute` fall back to regular `compute`.
## Documents
See the `etc/notes/` directory for some random notes about the project.
## Credits
### Core developer team
- [Emilio Jesús Gallego Arias](https://www.irif.fr/~gallego/) , Inria, Université de Paris, IRIF
- [Shachar Itzhaky](https://cs.technion.ac.il/~shachari/) , Technion
### Past Contributors
- Benoît Pin, [CRI, MINES ParisTech](https://www.cri.ensmp.fr)
## Acknowledgements
![FEEVER Logo](/frontend/classic/images/feever-logo.png?raw=true "Feever Logo")
jsCoq was made possible thanks to funding by the
[FEEVER](http://feever.fr) project and support from [MINES
ParisTech](http://www.mines-paristech.eu)
We want to _strongly thank_ the `js_of_ocaml` developers. Without
their great and quick support jsCoq wouldn't have been possible.
[CodeMirror](https://codemirror.net/) has played a crucial role in the
project, we are very happy with it, thanks a lot!
Please consider supporting the development of CodeMirror with a donation.
addons/.gitignore 0 → 100644
View file @ 2a40a0b1
.*.swp
.DS_Store
_build
node_modules
addons/.gitmodules 0 → 100644
View file @ 2a40a0b1
addons/Makefile 0 → 100644
View file @ 2a40a0b1
PKGS = teach
CONTEXT = jscoq+32bit
ifeq ($(DUNE_WORKSPACE:%.64=64), 64)
CONTEXT = jscoq+64bit
endif
ifeq ($(DUNE_WORKSPACE:%.wacoq=wacoq), wacoq)
CONTEXT = wacoq
endif
# needed when invoking `opam install`
OPAMSWITCH = $(CONTEXT)
export OPAMSWITCH
ifeq ($(DUNE_WORKSPACE),)
ifeq ($(CONTEXT), wacoq)
DUNE_WORKSPACE = $(PWD)/dune-workspace.wacoq
endif
ifeq ($(CONTEXT), jscoq+64bit)
DUNE_WORKSPACE = $(PWD)/dune-workspace.64
endif
endif
ifneq ($(DUNE_WORKSPACE),)
export DUNE_WORKSPACE
endif
OPAM_ENV = eval `opam env`
BUILT_PKGS = ${filter $(PKGS), ${notdir ${wildcard _build/$(CONTEXT)/*}}}
_V = ${firstword $(VERSION) $(VER) $(V)}
COMMIT_FLAGS = -a
ifneq ($(_V),)
MSG = [deploy] Prepare for $(_V).
else
ifeq ($(CONTEXT), wacoq)
_V = ${shell wacoq --version}
else
_V = ${shell jscoq --version}
endif
MSG = ${error MSG= is mandatory}
endif
world:
cd teach && make
privates:
.PHONY: %
env:
@echo export DUNE_WORKSPACE=$(DUNE_WORKSPACE)
set-ver:
_scripts/set-ver ${addprefix @,$(CONTEXT)} $(_V)
if [ -e _build/$(CONTEXT) ] ; then \
$(OPAM_ENV) && dune build _build/$(CONTEXT)/*/package.json ; fi # update build directory as well
pack:
rm -rf _build/$(CONTEXT)/*.tgz
_scripts/set-ver ${addprefix @,$(CONTEXT)} $(_V) _build/$(CONTEXT)
cd _build/$(CONTEXT) && npm pack ${addprefix ./, $(BUILT_PKGS)}
commit-all:
for d in $(PKGS); do ( cd $$d && git commit $(COMMIT_FLAGS) -m "$(MSG)" ); done
git commit $(COMMIT_FLAGS) -m "$(MSG)"
push-all:
for d in $(PKGS); do ( cd $$d && git push $(PUSH_FLAGS) ); done
commit+push-all:
for d in $(PKGS); do ( cd $$d && \
git commit $(COMMIT_FLAGS) -m "$(MSG)" && \
git push $(PUSH_FLAGS) ); done
git commit $(COMMIT_FLAGS) -m "$(MSG)" && git push $(PUSH_FLAGS)
clean-slate:
rm -rf */workdir
rm -rf _build
ci:
$(MAKE) clean-slate
$(OPAM_ENV) && $(MAKE)
$(MAKE) pack
addons/README.md 0 → 100644
View file @ 2a40a0b1
# jsCoq Addons Central
This is a meta-repo with references to jsCoq addon libraries as submodules.
These submodules contain "recipes" for downloadining, compiling and packaging
these libraries as jsCoq packages (`.json` and `.coq-pkg` files).
addons/_scripts/set-ver 0 → 100755
View file @ 2a40a0b1
#!/usr/bin/env node
/**
* Sets the "version" field in `package.json` for all
* modules at once.
* (useful for release candidates)
*/
import * as fs from 'fs';
import * as path from 'path';
import * as assert from 'assert';
function setAll(ver, scope='@jscoq', workspaceDir='.') {
for (let d of fs.readdirSync(workspaceDir)) {
var fn = path.join(workspaceDir, d, 'package.json');
if (fs.existsSync(fn)) {
var inp = fs.readFileSync(fn, 'utf-8');
var out = inp.replace(/"version": .*/, `"version": "${ver}",`)
.replace(/"name": "@[^/]+\// /*"*/, `"name": "${scope}/`);
var v = JSON.parse(out); // make sure
console.log(v.name, v.version);
assert(v.version === ver);
fs.chmodSync(fn, "0644"); // allow running in Dune build dir
fs.writeFileSync(fn, out);
}
}
}
function parseArgs() {
var opts = {};
for (let arg of process.argv.slice(2)) {
if (arg.startsWith('@')) opts.scope = arg.replace(/\+.*/, ''); // remove e.g. +32bit
else if (arg.match(/^\d/)) opts.ver = arg;
else if (!opts.dir) opts.dir = arg;
else console.warn(`[set-ver] extraneous argument: '${arg}'`);
}
return opts;
}
var opts = parseArgs();
if (opts.ver) {
setAll(opts.ver, opts.scope, opts.dir);
}
else {
console.log("usage: set-ver [scope] <version-number>");
}
addons/dune 0 → 100644
View file @ 2a40a0b1
(dirs :standard \ node_modules)
addons/dune-project 0 → 100644
View file @ 2a40a0b1
(lang dune 2.5)
(using coq 0.2)
addons/dune-workspace 0 → 100644
View file @ 2a40a0b1
(lang dune 2.4)
(profile release)
(context
(opam (switch jscoq+32bit)
(merlin)))
addons/dune-workspace.64 0 → 100644
View file @ 2a40a0b1
(lang dune 2.4)
(profile release)
(context
(opam (switch jscoq+64bit)
(merlin)))
addons/dune-workspace.wacoq 0 → 100644
View file @ 2a40a0b1
(lang dune 2.4)
(profile release)
(context
(opam (switch wacoq)
(env
(_ (env-vars ("pkgtool" wacoq))))
(merlin)))
addons/teach/.gitignore 0 → 100644
View file @ 2a40a0b1
.*.swp
_build
addons/teach/Makefile 0 → 100644
View file @ 2a40a0b1
.PHONY: all get
all:
# not parallel: some Dune dependency mixup with generating META file
dune build -j1
addons/teach/README.md 0 → 100644
View file @ 2a40a0b1
# addon-equations
Coq-Equations addon plugin for jsCoq