Skip to content

Commit 4d7388e

Browse files
hyperpolymathhyperpolymath
authored
Merge branch 'main' into chore/remove-playground-ffi-template
2 parents 6d552b2 + 21a219e commit 4d7388e

10 files changed

Lines changed: 811 additions & 121 deletions

File tree

‎.github/workflows/pages.yml‎

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -29,14 +29,11 @@ jobs:
2929
working-directory: .ddraig-ssg
3030
run: idris2 Ddraig.idr -o ddraig
3131
- name: Build site
32+
run: ./.ddraig-ssg/build/exec/ddraig build site _site https://nesy-prover.dev
33+
- name: Add playground
3234
run: |
33-
mkdir -p src
34-
if [ ! -f src/index.md ] && [ -f README.md ]; then
35-
cp README.md src/index.md
36-
elif [ ! -f src/index.md ]; then
37-
echo "# ${GITHUB_REPOSITORY}" > src/index.md
38-
fi
39-
./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/}
35+
mkdir -p _site/playground
36+
cp echidna-playground/index.html echidna-playground/styles.css _site/playground/
4037
- name: Upload artifact
4138
uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0
4239
with:

‎deno.lock‎

Lines changed: 9 additions & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎echidna-playground/deno.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@
44
"tasks": {
55
"build:res": "deno run -A --node-modules-dir=auto npm:rescript build",
66
"clean:res": "deno run -A --node-modules-dir=auto npm:rescript clean",
7-
"dev": "deno run --allow-net --allow-read server.ts",
8-
"serve": "deno run --allow-net --allow-read server.ts",
7+
"dev": "deno run --allow-net --allow-read jsr:@std/http@^1.0.0/file-server .",
8+
"serve": "deno run --allow-net --allow-read jsr:@std/http@^1.0.0/file-server .",
99
"res:build": "deno run -A --node-modules-dir=auto npm:rescript build",
1010
"res:clean": "deno run -A --node-modules-dir=auto npm:rescript clean",
1111
"res:watch": "deno run -A --node-modules-dir=auto npm:rescript build -w"

‎echidna-playground/index.html‎

Lines changed: 74 additions & 110 deletions
Original file line numberDiff line numberDiff line change
@@ -3,37 +3,39 @@
33
<head>
44
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
55
<meta name="description" content="An Online IDE for the Coq Theorem Prover" />
6-
<link rel="icon" href="ui-images/favicon.ico">
76
<link rel="stylesheet" type="text/css" href="styles.css">
8-
<title>jsCoq – Use Coq in Your Browser</title>
7+
<title>ECHIDNA Playground – Coq in Your Browser</title>
98
</head>
109
<body class="jscoq-main">
1110
<div id="ide-wrapper" class="toggled">
1211
<div id="code-wrapper">
1312
<div id="document">
1413
<div>
15-
<h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online System!</h3>
14+
<div id="load-error" hidden role="alert">
15+
<strong>jsCoq could not be loaded.</strong>
16+
The interactive prover is unavailable right now (the CDN may be
17+
unreachable). The proof script below is still readable, and you
18+
can run it in any local Coq installation.
19+
</div>
20+
<h3>Welcome to the ECHIDNA <span class="jscoq-name">jsCoq</span> Playground</h3>
1621
<p>
17-
Welcome to the <span class="jscoq-name">jsCoq</span> technology demo!
18-
<span class="jscoq-name">jsCoq</span> is an interactive,
19-
web-based environment for the Coq Theorem prover, and is a collaborative
20-
development effort. See the <a href="#team">list of contributors</a>
21-
below.
22+
This page embeds <span class="jscoq-name">jsCoq</span>, an
23+
interactive, web-based environment for the Coq theorem prover.
24+
All the Coq code below is editable and runs directly in your
25+
browser — no installation required. Once
26+
<span class="jscoq-name">jsCoq</span> finishes loading, step
27+
through the proof and watch the intermediate proof states in the
28+
right-hand panel.
2229
</p>
2330
<p>
24-
<span class="jscoq-name">jsCoq</span> is open source. If you find any problem or want to make
25-
any contribution, you are extremely welcome! We await your
26-
feedback at <a href="https://github.com/jscoq/jscoq">GitHub</a>
27-
and <a href="https://gitter.im/jscoq/Lobby">Gitter</a>.
31+
<span class="jscoq-name">jsCoq</span> is open source — feedback
32+
and contributions are welcome at
33+
<a href="https://github.com/jscoq/jscoq">GitHub</a>. The wider
34+
ECHIDNA platform, which orchestrates Coq alongside many other
35+
provers, lives at
36+
<a href="https://github.com/hyperpolymath/echidna">github.com/hyperpolymath/echidna</a>.
2837
</p>
2938
<h4>Instructions:</h4>
30-
<p>
31-
The following document contains embedded Coq code.
32-
All the code is editable and can be run directly on the page.
33-
Once <span class="jscoq-name">jsCoq</span> finishes loading, you are
34-
free to experiment by stepping through the proof and viewing intermediate
35-
proof states on the right panel.
36-
</p>
3739
<h5>Actions:</h5>
3840
<table class="doc-actions">
3941
<tr><th>Button</th><th>Key binding</th><th>Action</th></tr>
@@ -58,100 +60,62 @@ <h5>Actions:</h5>
5860
<td>Toggles the goal panel.</td>
5961
</tr>
6062
</table>
61-
<h5>Saving your own proof scripts:</h5>
62-
<p>
63-
The <a href="scratchpad.html">scratchpad</a> offers simple, local
64-
storage functionality.
65-
Please go to <a href="https://x80.org/collacoq/">CollaCoq</a> if
66-
you want to share your developments with other users.
67-
</p>
6863

69-
<h4>A First Example: The Infinitude of Primes</h4>
70-
<p>
71-
We don't provide a Coq tutorial (yet), but as a showcase, we
72-
display a proof of the infinitude of primes in Coq. The proof relies
73-
in the Mathematical Components library by the
74-
<a href="https://ssr.msr-inria.inria.fr/">MSR/Inria</a> team led
75-
by Georges Gonthier, so our first step will be to load it and
76-
set a few Coq options:
77-
</p>
78-
</div>
79-
<div>
80-
<textarea id="addnC">From Coq Require Import ssreflect ssrfun ssrbool.
81-
From mathcomp Require Import eqtype ssrnat div prime.</textarea>
82-
</div>
83-
<div>
84-
<h5>Ready to do Proofs!</h5>
64+
<h4>A First Example: Addition and Zero</h4>
8565
<p>
86-
Once the basic environment has been set up, we can proceed to
87-
the proof:
66+
As a showcase, we prove a small but genuine theorem about the
67+
natural numbers: adding zero on the right leaves a number
68+
unchanged. In Coq, <code>nat</code> is defined inductively —
69+
a natural number is either <code>0</code> or the successor
70+
<code>S n</code> of a natural number — and <code>+</code>
71+
recurses on its <em>first</em> argument. That makes
72+
<code>0 + n = n</code> true by computation, but
73+
<code>n + 0 = n</code> requires a proof by induction.
8874
</p>
8975
</div>
9076
<div>
91-
<textarea id="prime_above1">(* A nice proof of the infinitude of primes, by Georges Gonthier *)
92-
Lemma prime_above m : {p | m < p & prime p}.
77+
<textarea id="ex1">Lemma add_zero_right : forall n : nat, n + 0 = n.
9378
Proof.</textarea>
9479
<p>
95-
The lemma states that for any number <code>m</code>,
96-
there is a prime number larger than <code>m</code>.
97-
98-
Coq is a <em>constructive system</em>, which among other things
99-
implies that to show the existence of an object, we need to
100-
actually provide an algorithm that will construct it.
101-
102-
In this case, we need to find a prime number <code>p</code>
103-
that is greater than <code>m</code>.
104-
What would be a suitable <code>p</code>?
105-
106-
Choosing <code>p</code> to be the first prime divisor of <code>m! + 1</code>
107-
works.
108-
As we will shortly see, properties of divisibility will imply that
109-
<code>p</code> must be greater than <code>m</code>.
110-
</p>
111-
<textarea id="prime_above2">have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1
112-
by rewrite addn1 ltnS fact_gt0.</textarea>
113-
<p>
114-
Our first step is thus to use the library-provided lemma
115-
<code>pdivP</code>, which states that every number is divided by a
116-
prime. Thus, we obtain a number <code>p</code> and the corresponding
117-
hypotheses <code>pr_p : prime p</code> and <code>p_dv_m1</code>,
118-
"p divides m! + 1".
119-
The ssreflect tactic <code>have</code> provides a convenient way to
120-
instantiate this lemma and discard the side proof obligation
121-
<code>1 &lt; m! + 1</code>.
80+
The lemma states that for every natural number <code>n</code>,
81+
<code>n + 0</code> equals <code>n</code>. We begin the proof by
82+
induction on <code>n</code>, which splits the goal into a base
83+
case for <code>0</code> and an inductive step for
84+
<code>S n</code>:
12285
</p>
123-
<textarea id="prime_above3">exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.</textarea>
86+
<textarea id="ex2"> induction n as [| n IHn].
87+
- (* Base case: 0 + 0 = 0 *)
88+
reflexivity.</textarea>
12489
<p>
125-
It remains to prove that <code>p</code> is greater than <code>m</code>.
126-
We reason by
127-
contraposition with the divisibility hypothesis, which gives us
128-
the goal "if <code>p ≤ m</code> then <code>p</code> is not a prime divisor of "
129-
<code>m! + 1</code>".
90+
The base case is settled by <code>reflexivity</code>, since
91+
<code>0 + 0</code> computes to <code>0</code>. In the inductive
92+
step we may assume the hypothesis <code>IHn : n + 0 = n</code>;
93+
simplification exposes the successor, and rewriting with the
94+
hypothesis closes the goal:
13095
</p>
131-
<textarea id="prime_above4">by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
96+
<textarea id="ex3"> - (* Inductive step: S n + 0 = S n *)
97+
simpl.
98+
rewrite IHn.
99+
reflexivity.
132100
Qed.</textarea>
133101
<p>
134-
The goal follows from basic properties of divisibility, plus
135-
from the fact that if <code>p ≤ m</code>, then <code>p</code> divides
136-
<code>m!</code>, so that for <code>p</code> to divide
137-
<code>m! + 1</code> it must also divide 1,
138-
in contradiction to <code>p</code> being prime.
102+
And that is a complete, machine-checked proof. Try editing the
103+
script — for instance, replace <code>rewrite IHn</code> with
104+
something else and watch Coq object — or state and prove your
105+
own lemma in the editor.
139106
</p>
140107
<hr/>
141108
<p>
142-
<span class="jscoq-name">jsCoq</span> provides many other packages,
143-
including Coq's standard library and the
144-
<a href="https://math-comp.github.io">mathematical components</a>
145-
library.
146-
Feel free to experiment, and bear with the beta status of this demo.
147-
</p>
148-
<p>
149-
<i>¡Salut!</i>
109+
This embedded build ships Coq's standard library packages
110+
(arithmetic, collections, reals). The full ECHIDNA platform
111+
drives Coq and many other provers through one dispatch
112+
pipeline — see the
113+
<a href="https://nesy-prover.dev/docs/index.html">platform documentation</a>.
150114
</p>
151115
</div>
152116
<div id="team">
153117
<a name="team"></a>
154-
<p><i>The dev team</i></p>
118+
<p><i>The jsCoq dev team</i></p>
155119
<ul>
156120
<li>
157121
<a href="https://www.irif.fr/~gallego/">Emilio Jesús Gallego Arias</a>
@@ -177,27 +141,27 @@ <h5>Ready to do Proofs!</h5>
177141
</div>
178142
</div>
179143

180-
<script type="text/javascript">
181-
// jsCoq initialization placeholder
182-
// To enable full jsCoq functionality, run:
183-
// npm install jscoq bootstrap
184-
// Then uncomment the script below:
185-
186-
/*
187-
var jscoq_ids = ['addnC', 'prime_above1', 'prime_above2', 'prime_above3', 'prime_above4'];
188-
var jscoq_opts = {
144+
<script type="module">
145+
const jscoq_ids = ['ex1', 'ex2', 'ex3'];
146+
const jscoq_opts = {
147+
prelude: true,
189148
implicit_libs: false,
190-
focus: false,
191149
editor: { mode: { 'company-coq': true }, keyMap: 'default' },
192150
init_pkgs: ['init'],
193-
all_pkgs: ['coq', 'mathcomp']
151+
all_pkgs: ['coq']
194152
};
195153

196-
var coq;
197-
JsCoq.start(jscoq_ids, jscoq_opts).then(res => coq = res);
198-
*/
199-
200-
console.log('Coq-Jr loaded. Run "npm install" and enable jsCoq for full functionality.');
154+
// Dynamic import, not a static one: a static import that fails to
155+
// fetch aborts module instantiation, so nothing below it — including
156+
// the error handler — would ever run, and the banner would stay
157+
// hidden in exactly the CDN-unreachable case it exists for.
158+
try {
159+
const { JsCoq } = await import('https://cdn.jsdelivr.net/npm/jscoq@0.17.1/jscoq.js');
160+
await JsCoq.start(jscoq_ids, jscoq_opts);
161+
} catch (err) {
162+
console.error('jsCoq failed to load or start:', err);
163+
document.getElementById('load-error').hidden = false;
164+
}
201165
</script>
202166
</body>
203167
</html>

0 commit comments

Comments
 (0)