Code Monkey home page Code Monkey logo

do-supplement's Introduction

Supplemental material for the paper "'do' Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)"

This supplement consists of a Lean 4 package containing translation rules and example proofs of equivalence as described in the paper. Each extension is declared in a separate .lean file in the Do directory:

Do/
  Basic.lean     # Section 2, Figure 1
  Mut.lean       # Section 2, Figures 3 & 5
  Return.lean    # Section 3
  For.lean       # Section 4

  LazyList.lean  # nondeterministic monad implementation used in `Mut.lean` examples

Do/Formal.lean contains the formalization of the equivalence proof written in a literate style explaining more details not mentioned in the paper. Each Lean file comes with a corresponding .html file rendered using Alectryon that allows for exploring the file including type and goal information in any browser without installing Lean (hosted here for the latest version of the source repository). The directory gh-survey contains simple scripts for aggregating the use of extended do notation from Lean projects on GitHub.

Exploring the supplement with Lean

While the generic instructions for setting up Lean 4 can be used for interacting with this package, we will give a simplified workflow using the specific version of Lean 4 and a single editor, VS Code, that minimizes changes to the host machines in the following:

  • Download and unpack your platform's release of Lean 4.0.0-nightly-2022-06-01
  • Add the bin directory of that archive to your shell's search path, e.g.
$ export PATH=$PATH:~/Downloads/lean-4.0.0-linux/bin
  • Install VS Code and open the package in it: code .. It is very important that lean is in the search path of VS Code and that the supplement folder is opened as a workspace, which this command should ensure.
  • Open the Extensions tab (Ctrl+Shift+X) and install the lean4 extension (author: leanprover).
  • You should now have working error diagnostics, go-to-definition, as well as a goal display for tactic proofs in the supplement files!

Regenerating the HTML output

The versions of Alectryon and its Lean 4 backend LeanInk used to generate the accompanying HTML files are archived in the folders alectryon and LeanInk, respectively. To regenerate the output, first install the local Alectryon version as described in its readme:

python3 -m pip install ./alectryon

After ensuring that alectryon is now in your PATH, running make html (optionally preceded by make clean) should regenerate the files.

do-supplement's People

Contributors

kha avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar

Forkers

suhr

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.