[Agda] Agda Interactive Notebooks

[Andrea Amantini]

Dear all,

I'd like to share some facts on our platform for collaborative interactive
polyglot notebooks https://nextjournal.com where we’re working on some
experimental support for Agda. Some example first:

- https://nextjournal.com/plfa/ToC (Programming Language Foundations in
Agda; Kokke, Siek, Wadler)
- https://nextjournal.com/agda/euclid-theorem (Strickland)
- https://nextjournal.com/zampino/russell-paradox (based on an Altenkirch’s
lecture)
- https://nextjournal.com/zampino/finite-decidable-setoids

You can get started by remixing any of the above articles, or our Agda
template

- https://nextjournal.com/nextjournal/agda-template
- https://nextjournal.com/try/nextjournal/agda-template

On the teaching side, students at University of Bergen collaborate on
shared notes for their PhD seminar on MLTT and Univalence:

- https://nextjournal.com/uib-types/journal-part-2 (shared with permission
from the authors)

This is how our Agda environment is built, it’s also a Notebook :-) which I
try to update on a regular basis:

- https://nextjournal.com/nextjournal/agda-environment

but you could build your own as long as you install our fork of Agda
Jupyter Kernel along with Agda dependencies:
https://github.com/nextjournal/agda-kernel.

We currently support only a subset of Agda Emacs Mode given the constraints
of Jupyter interaction: apart from type-checking code, the kernel currently
supports Agsy Auto, Give, Split, Refine (via Tab) and Context Inspection
(via Shift+Tab). It would be nice to explore richer interactions in the
future, possibly via a custom Haskell Socket REPL-ish thing, is there prior
work in that direction?

Nextjournal runtimes/environments are easily shareable and reusable (both
in the same notebook or across different documents) and in the specific
case of Agda, exported runtimes are immediately importable as Agda modules
(see Euclid's Theorem formalisation above).

I'll be very glad to help anyone willing to port existing work to
nextjournal for teaching, publication or blogging. So far we’re able to
import markdown and jupyter ipynb formats (Strickland's essay above was
converted from LaTeX (.lagda) to markdown via Pandoc <https://pandoc.org>
first). More built-in conversions might come soon.

Signup is free and there’s special deals for students/academics should
anyone need more computing power than the free plan allows... but that
shouldn’t be the most common case with Agda.

Looking forward for feedback, have a nice day,
Andrea
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201201/898a9e17/attachment.html>