The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

Dear coq-clubbers,

For those of you interested in learning more about typed lambda calculi through Iron Lambda (perhaps after completing Programming Language Foundations?) but are encountering build errors and/or unsure how to step through the vernacular files interactively in your CoqIDE after a successful build as of late, I hereby present unto you a working version of Iron Lambda with detailed build instructions which should work out of the box in your CoqIDE:

https://github.com/DonaldKellett/iron-lambda

Basically, this repo is a direct port of the finished parts (i.e. those under `done/`) of an older version of Iron Lambda (Jan 2017) but with the Makefile from the original repo replaced with a `_CoqProject` file and a more detailed README guiding you from installing the correct version of Coq/CoqIDE all the way up to opening the project files in your CoqIDE after a successful build. While the build instructions in the README might be rather conservative in its wording (stating how it is not guaranteed to work with OSes other than macOS), I would reasonably expect it to build correctly on any UNIX-like system with `make` and `opam` installed.

Feel free to inform me if this solution does not work for you, and enjoy! :-)

Donald Sebastian Leung

A Year 3 Computer Science and Engineering undergraduate at The Hong Kong University of Science and Technology