tmEgg: a document-oriented Coq interface

tmEgg is my in-development interface to the Coq proof assistant. It uses (and requires) TeXmacs, leveraging the latter to allow the creation of scientific documents with Coq code embedded. Its user interaction model is that the user is always allowed to change any coq command embedded in the document, and it will automatically do whatever is necessary for that to take effect.


You can get tmEgg as tarball in statically linked binary (for i386 architecture computers running GNU/Linux) or source form at the bottom of this page, or in source form from my GNU Arch (tla) archive. The tmegg--mainline branch contains code that actually works.

Version 0 of the tmegg--mainline branch corresponds to tmEgg version 1 and version 1 of the tmegg--mainline branch corresponds to alpha-quality tmEgg version 2. The tarballs contain tmEgg version 1.

Installation and use

See the spartan documentation for installation and usage instructions.

This list of ressources is autogenerated by a self-hacked version of a PHP script I found somewhere.

NameLast modified (UTC time)
README2007/3/6 14:38:36
regexp-pp-debian-10_pp.dpatch2007/3/6 13:37:45
fat_tmEgg--mainline--0--patch-123--i386.tar.bz22007/3/6 21:20:52
tmEgg--mainline--0--patch-123.tar.bz22007/3/6 21:20:52

Have fun!