Projects related to the puzzle game Escape

Status: intermittently active; 2019-2020 (supersedes any conflicting remarks left on this page; see the home page for definitions)

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.

My modified version of Escape[# Top]

Status: intermittently active; 2019-2020 (supersedes any conflicting remarks left on this page; see the home page for definitions)

Icon for my version of Escape, featuring the upstream icon and the favicon of this site.

I have a modified version of the Escape application with a number of bug fixes and small enhancements (not affecting the rules of the game).  While the amount of work I've done is modest compared to that of Tom 7 and other contributors, the changes may give you a significantly better experience depending on what you do with Escape.  Some of the most notable changes:

• Redoing a single move now uses animation.  This can be a big help in understanding what is happening in complex levels.
• An option to work with levels that exceed the standard size limits, subject to available memory.  This can be useful for experimenting with large embeddings.  (Of course, the main server still only accepts levels within the standard limits.)
• New hotkeys and features to reveal previously hidden information in both play and edit modes.
• A new mode in the level browser that sorts unsolved and solved levels separately by difficulty, useful for finding the easiest unsolved levels.

For more information, see the bottom of the help file.

Source code, issue tracking, etc. on GitLab.  (Note about hosting: 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.)

Currently, the only officially supported way to use my Escape application is to build the latest source revision from the repository on Linux; if you're using a different OS, you could use a Linux virtual machine of some kind.  Old binary releases for Linux and Windows are still available and may provide a convenient way for you to try out some of my improvements before you decide whether to go to the trouble to get the latest revision.  As of November 2023, I'm not aware of anyone else using my version of Escape and thus can't justify time-consuming tasks that don't benefit my own usage, such as making new releases or maintaining support for any OS other than Linux.  If you are using or want to use my version, please tell me!

Klotski embedding[# Top]

Status: dormant; 2019 (supersedes any conflicting remarks left on this page; see the home page for definitions)

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.

Coq formalization[# Top]

Status: dormant; 2020 (supersedes any conflicting remarks left on this page; see the home page for definitions)

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

• Proving that the current speed record for a given puzzle cannot be beaten;
• Formalizing another problem and its embedding in Escape, proving the embedding correct, and generating the Escape puzzle via extraction.

(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[# Top]

Status: on hold; 2020 (supersedes any conflicting remarks left on this page; see the home page for definitions)

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.