Skip to content

feat(site): real multi-page site for nesy-prover.dev #329

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 3 commits into from
Jul 28, 2026
Merged

feat(site): real multi-page site for nesy-prover.dev #329

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
acfd198
feat(site): multi-page nesy-prover.dev site — landing, docs, playground
hyperpolymath Jul 28, 2026
8a516be
chore: restore deno.lock to origin state
hyperpolymath Jul 28, 2026
1b7949b
fix(site): correct the API reference against the implemented services
hyperpolymath Jul 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 4 additions & 7 deletions .github/workflows/pages.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,11 @@ jobs:
working-directory: .ddraig-ssg
run: idris2 Ddraig.idr -o ddraig
- name: Build site
run: ./.ddraig-ssg/build/exec/ddraig build site _site https://nesy-prover.dev
- name: Add playground
run: |
mkdir -p src
if [ ! -f src/index.md ] && [ -f README.md ]; then
cp README.md src/index.md
elif [ ! -f src/index.md ]; then
echo "# ${GITHUB_REPOSITORY}" > src/index.md
fi
./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/}
mkdir -p _site/playground
cp echidna-playground/index.html echidna-playground/styles.css _site/playground/
- name: Upload artifact
uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0
with:
Expand Down
11 changes: 9 additions & 2 deletions deno.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions echidna-playground/deno.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@
"tasks": {
"build:res": "deno run -A --node-modules-dir=auto npm:rescript build",
"clean:res": "deno run -A --node-modules-dir=auto npm:rescript clean",
"dev": "deno run --allow-net --allow-read server.ts",
"serve": "deno run --allow-net --allow-read server.ts",
"dev": "deno run --allow-net --allow-read jsr:@std/http@^1.0.0/file-server .",
"serve": "deno run --allow-net --allow-read jsr:@std/http@^1.0.0/file-server .",
"res:build": "deno run -A --node-modules-dir=auto npm:rescript build",
"res:clean": "deno run -A --node-modules-dir=auto npm:rescript clean",
"res:watch": "deno run -A --node-modules-dir=auto npm:rescript build -w"
Expand Down
184 changes: 74 additions & 110 deletions echidna-playground/index.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,37 +3,39 @@
<head>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<meta name="description" content="An Online IDE for the Coq Theorem Prover" />
<link rel="icon" href="ui-images/favicon.ico">
<link rel="stylesheet" type="text/css" href="styles.css">
<title>jsCoq – Use Coq in Your Browser</title>
<title>ECHIDNA Playground – Coq in Your Browser</title>
</head>
<body class="jscoq-main">
<div id="ide-wrapper" class="toggled">
<div id="code-wrapper">
<div id="document">
<div>
<h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online System!</h3>
<div id="load-error" hidden role="alert">
<strong>jsCoq could not be loaded.</strong>
The interactive prover is unavailable right now (the CDN may be
unreachable). The proof script below is still readable, and you
can run it in any local Coq installation.
</div>
<h3>Welcome to the ECHIDNA <span class="jscoq-name">jsCoq</span> Playground</h3>
<p>
Welcome to the <span class="jscoq-name">jsCoq</span> technology demo!
<span class="jscoq-name">jsCoq</span> is an interactive,
web-based environment for the Coq Theorem prover, and is a collaborative
development effort. See the <a href="#team">list of contributors</a>
below.
This page embeds <span class="jscoq-name">jsCoq</span>, an
interactive, web-based environment for the Coq theorem prover.
All the Coq code below is editable and runs directly in your
browser — no installation required. Once
<span class="jscoq-name">jsCoq</span> finishes loading, step
through the proof and watch the intermediate proof states in the
right-hand panel.
</p>
<p>
<span class="jscoq-name">jsCoq</span> is open source. If you find any problem or want to make
any contribution, you are extremely welcome! We await your
feedback at <a href="https://github.com/jscoq/jscoq">GitHub</a>
and <a href="https://gitter.im/jscoq/Lobby">Gitter</a>.
<span class="jscoq-name">jsCoq</span> is open source — feedback
and contributions are welcome at
<a href="https://github.com/jscoq/jscoq">GitHub</a>. The wider
ECHIDNA platform, which orchestrates Coq alongside many other
provers, lives at
<a href="https://github.com/hyperpolymath/echidna">github.com/hyperpolymath/echidna</a>.
</p>
<h4>Instructions:</h4>
<p>
The following document contains embedded Coq code.
All the code is editable and can be run directly on the page.
Once <span class="jscoq-name">jsCoq</span> finishes loading, you are
free to experiment by stepping through the proof and viewing intermediate
proof states on the right panel.
</p>
<h5>Actions:</h5>
<table class="doc-actions">
<tr><th>Button</th><th>Key binding</th><th>Action</th></tr>
Expand All @@ -58,100 +60,62 @@ <h5>Actions:</h5>
<td>Toggles the goal panel.</td>
</tr>
</table>
<h5>Saving your own proof scripts:</h5>
<p>
The <a href="scratchpad.html">scratchpad</a> offers simple, local
storage functionality.
Please go to <a href="https://x80.org/collacoq/">CollaCoq</a> if
you want to share your developments with other users.
</p>

<h4>A First Example: The Infinitude of Primes</h4>
<p>
We don't provide a Coq tutorial (yet), but as a showcase, we
display a proof of the infinitude of primes in Coq. The proof relies
in the Mathematical Components library by the
<a href="https://ssr.msr-inria.inria.fr/">MSR/Inria</a> team led
by Georges Gonthier, so our first step will be to load it and
set a few Coq options:
</p>
</div>
<div>
<textarea id="addnC">From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import eqtype ssrnat div prime.</textarea>
</div>
<div>
<h5>Ready to do Proofs!</h5>
<h4>A First Example: Addition and Zero</h4>
<p>
Once the basic environment has been set up, we can proceed to
the proof:
As a showcase, we prove a small but genuine theorem about the
natural numbers: adding zero on the right leaves a number
unchanged. In Coq, <code>nat</code> is defined inductively —
a natural number is either <code>0</code> or the successor
<code>S n</code> of a natural number — and <code>+</code>
recurses on its <em>first</em> argument. That makes
<code>0 + n = n</code> true by computation, but
<code>n + 0 = n</code> requires a proof by induction.
</p>
</div>
<div>
<textarea id="prime_above1">(* A nice proof of the infinitude of primes, by Georges Gonthier *)
Lemma prime_above m : {p | m < p & prime p}.
<textarea id="ex1">Lemma add_zero_right : forall n : nat, n + 0 = n.
Proof.</textarea>
<p>
The lemma states that for any number <code>m</code>,
there is a prime number larger than <code>m</code>.

Coq is a <em>constructive system</em>, which among other things
implies that to show the existence of an object, we need to
actually provide an algorithm that will construct it.

In this case, we need to find a prime number <code>p</code>
that is greater than <code>m</code>.
What would be a suitable <code>p</code>?

Choosing <code>p</code> to be the first prime divisor of <code>m! + 1</code>
works.
As we will shortly see, properties of divisibility will imply that
<code>p</code> must be greater than <code>m</code>.
</p>
<textarea id="prime_above2">have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1
by rewrite addn1 ltnS fact_gt0.</textarea>
<p>
Our first step is thus to use the library-provided lemma
<code>pdivP</code>, which states that every number is divided by a
prime. Thus, we obtain a number <code>p</code> and the corresponding
hypotheses <code>pr_p : prime p</code> and <code>p_dv_m1</code>,
"p divides m! + 1".
The ssreflect tactic <code>have</code> provides a convenient way to
instantiate this lemma and discard the side proof obligation
<code>1 &lt; m! + 1</code>.
The lemma states that for every natural number <code>n</code>,
<code>n + 0</code> equals <code>n</code>. We begin the proof by
induction on <code>n</code>, which splits the goal into a base
case for <code>0</code> and an inductive step for
<code>S n</code>:
</p>
<textarea id="prime_above3">exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.</textarea>
<textarea id="ex2"> induction n as [| n IHn].
- (* Base case: 0 + 0 = 0 *)
reflexivity.</textarea>
<p>
It remains to prove that <code>p</code> is greater than <code>m</code>.
We reason by
contraposition with the divisibility hypothesis, which gives us
the goal "if <code>p ≤ m</code> then <code>p</code> is not a prime divisor of "
<code>m! + 1</code>".
The base case is settled by <code>reflexivity</code>, since
<code>0 + 0</code> computes to <code>0</code>. In the inductive
step we may assume the hypothesis <code>IHn : n + 0 = n</code>;
simplification exposes the successor, and rewriting with the
hypothesis closes the goal:
</p>
<textarea id="prime_above4">by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
<textarea id="ex3"> - (* Inductive step: S n + 0 = S n *)
simpl.
rewrite IHn.
reflexivity.
Qed.</textarea>
<p>
The goal follows from basic properties of divisibility, plus
from the fact that if <code>p ≤ m</code>, then <code>p</code> divides
<code>m!</code>, so that for <code>p</code> to divide
<code>m! + 1</code> it must also divide 1,
in contradiction to <code>p</code> being prime.
And that is a complete, machine-checked proof. Try editing the
script — for instance, replace <code>rewrite IHn</code> with
something else and watch Coq object — or state and prove your
own lemma in the editor.
</p>
<hr/>
<p>
<span class="jscoq-name">jsCoq</span> provides many other packages,
including Coq's standard library and the
<a href="https://math-comp.github.io">mathematical components</a>
library.
Feel free to experiment, and bear with the beta status of this demo.
</p>
<p>
<i>¡Salut!</i>
This embedded build ships Coq's standard library packages
(arithmetic, collections, reals). The full ECHIDNA platform
drives Coq and many other provers through one dispatch
pipeline — see the
<a href="https://nesy-prover.dev/docs/index.html">platform documentation</a>.
</p>
</div>
<div id="team">
<a name="team"></a>
<p><i>The dev team</i></p>
<p><i>The jsCoq dev team</i></p>
<ul>
<li>
<a href="https://www.irif.fr/~gallego/">Emilio Jesús Gallego Arias</a>
Expand All @@ -177,27 +141,27 @@ <h5>Ready to do Proofs!</h5>
</div>
</div>

<script type="text/javascript">
// jsCoq initialization placeholder
// To enable full jsCoq functionality, run:
// npm install jscoq bootstrap
// Then uncomment the script below:

/*
var jscoq_ids = ['addnC', 'prime_above1', 'prime_above2', 'prime_above3', 'prime_above4'];
var jscoq_opts = {
<script type="module">
const jscoq_ids = ['ex1', 'ex2', 'ex3'];
const jscoq_opts = {
prelude: true,
implicit_libs: false,
focus: false,
editor: { mode: { 'company-coq': true }, keyMap: 'default' },
init_pkgs: ['init'],
all_pkgs: ['coq', 'mathcomp']
all_pkgs: ['coq']
};

var coq;
JsCoq.start(jscoq_ids, jscoq_opts).then(res => coq = res);
*/

console.log('Coq-Jr loaded. Run "npm install" and enable jsCoq for full functionality.');
// Dynamic import, not a static one: a static import that fails to
// fetch aborts module instantiation, so nothing below it — including
// the error handler — would ever run, and the banner would stay
// hidden in exactly the CDN-unreachable case it exists for.
try {
Comment thread
hyperpolymath marked this conversation as resolved.
const { JsCoq } = await import('https://cdn.jsdelivr.net/npm/jscoq@0.17.1/jscoq.js');
await JsCoq.start(jscoq_ids, jscoq_opts);
} catch (err) {
console.error('jsCoq failed to load or start:', err);
document.getElementById('load-error').hidden = false;
}
</script>
</body>
</html>
Loading