- May 08, 2022
-
-
Shachar Itzhaky authored
`<kbd>` formatting and a hint for newcomers to look at the scratchpad icon.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
- May 07, 2022
-
-
Shachar Itzhaky authored
Also generated symbols for the examples.
-
Shachar Itzhaky authored
It is no longer in use. Serving from source dir still works with `make links`, but you must run `make links-clean` before building with Dune again.
-
Shachar Itzhaky authored
This fell into disrepair following some refactoring of the package format.
-
Shachar Itzhaky authored
Updated to reflect current implementation. Fixes #267.
-
Shachar Itzhaky authored
-
- May 06, 2022
-
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
Filled in the links in the navbar, etc. Added hover action to quick-start reference.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
Added meaningful names to comparison lemmas. Renamed module to `sqrt_2` so the import looks nicer on the landing page.
-
Shachar Itzhaky authored
Added flag `--no-recurse` to disable subdir recursion when building packages.
-
Shachar Itzhaky authored
Added a link to Coq in "settings". The top-left link now points to jsCoq's homepage instead. Landing-page CSS moved to a separate file.
-
Shachar Itzhaky authored
As suggested by @hannelita.
-
Shachar Itzhaky authored
It is longer, yes, but perhaps easier to understand in prose. Fixed indentation.
-
- May 05, 2022
-
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
Allows multiple jobs to invoke the SDK in parallel. If the SDK is not installed, the first to lock the file will carry out the install.
-
Shachar Itzhaky authored
A bind-mount is too slow. `sudo` is required to copy onto the volume. The implementation is currently non-reentrant, so `-j1` is needed.
-
- May 04, 2022
-
-
Shachar Itzhaky authored
Allow specifying sub-branch for quick testing of feature branches. Makefile targets for uploading SDK images to Dockerhub.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
This directory is now excluded from Dune. Because it contains `dune` files that serve as examples themselves. (Currently, there is one in `sdk-demo`.)
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
When mounting `/home`, gosu may inadvertantly write to the host's because of `useradd`.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
As subcommand `jscoq sdk`.
-
Shachar Itzhaky authored
Allows a dev to only build core jsCoq and SDK.
-
- May 03, 2022
-
-
Shachar Itzhaky authored
Included `index.html` and a `package.json` to show how to load and run the resulting package. Also added `playful.html`. (Which is a bit unrelated.)
-
Shachar Itzhaky authored
Currently separate from the main cli, but for no good reason. Should be a sub-command.
-
Shachar Itzhaky authored
Made the example a little bit smaller by removing some unneeded boilerplate. (Possible thanks to Dune 3's `glob_files_rec`.) Also, the example now showcases `group-theory` instead of Coqoban. Mainly because we already have Coqoban as an addon.
-
Shachar Itzhaky authored
Docker multiarch
-
- May 01, 2022
-
-
Shachar Itzhaky authored
We will keep editing to add some documentation around the actual proof.
-
Karl Palmskog authored
-
Karl Palmskog authored
-
Karl Palmskog authored
-
Shachar Itzhaky authored
-
- Apr 30, 2022
-
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
Cleanup apt lists.
-