Matt McCutchen's Web SiteEscape  (Top, Klotski embedding, My modified version of Escape, Coq formalization, Escape in Escape embedding, Bottom).  Email me about this page.

Escape projects

This part of my web site collects various projects related to the puzzle game Escape.  Please see that web site for an overview of Escape; I won't repeat the information here.  I welcome your feedback on any of the projects on this page; I can set up a mailing list or discussion forum of some kind if it seems worthwhile.

Warning: If you plan to work or play seriously with Escape on Linux, note that as of this writing (2020-02-28), both the Linux binary and the source tarball on the official web site are way out of date and have at least one severe known bug (a bookmark is silently lost if you try to save more than one bookmark on the same puzzle).  I urge you to get a more recent version of Escape, e.g., by building from the official source repository or using my modified version below.

Klotski embedding

I've developed an embedding of several Klotski puzzles in Escape, meaning that the Klotski puzzles can be played from within Escape.  My write-up on this is long enough that it is on its own page.

My modified version of Escape

I have developed a modified version of Escape with minor enhancements.  I plan to offer the changes that are suitable for upstream to upstream, but some changes are unsuitable and I don't know how responsive upstream will be.  You may wish to use my version if it meets your needs, and you are welcome to offer me changes, which I will accept if they are valuable enough to me to be worth maintaining.

The project is hosted on GitLab; you can get the code and submit issues and merge requests there.  (For the first time, I had a completely free choice of hosting for one of my projects and have chosen an external service, despite my usual preference to keep everything under my control, because I hope it will be less work for both me and potential contributors and I believe the security and privacy risk is low.  If you have any concerns about my use of GitLab, feel free to email me.)

Notable changes in my version:

Coq formalization

I have reimplemented the rules of Escape in the Coq mechanized proof system, anticipating use cases such as:

(Caveat: It's a huge amount of work to prove anything interesting in Coq about a system as complex as Escape, at least without Coq skills orders of magnitude better than mine.  So I don't know if the use cases will end up being realistic.  So far, I just had fun reimplementing and testing the rules.)

In addition to the core Escape logic in Coq, there is OCaml code that works with the data types extracted from Coq and can read and write puzzle files (esx) and read the solutions from a player file (esp).

Like my version of the Escape application, this codebase is hosted on GitLab and the same remarks apply.

Escape in Escape embedding

I've done some design work for an embedding of Escape in itself (not the identity!).  Since the rules of Escape are so complicated, I expect the output puzzles to be way over the standard size limits even for the most trivial input puzzles; this was a large motivation for me to remove the limits in my version of Escape.  I have a sketch of the UI and some ideas about the data representation and the implementation of certain parts.  I have no materials to share yet, but if you are working on the same thing, please do contact me so we can avoid duplicating work.


Matt McCutchen's Web SiteEscape  (Top, Klotski embedding, My modified version of Escape, Coq formalization, Escape in Escape embedding, Bottom).  Email me about this page.
Modification time of this page's main source file: 2020-03-18 01:02:20 +0000
Except where otherwise noted, Matt McCutchen waives his copyright to the content of this site.  This site comes with absolutely no warranty.  Why?