meta.yml

---
fullname: Coqoban
shortname: coqoban
organization: coq-community
community: true
action: true

synopsis: >-
  Coqoban (Sokoban in Coq)

description: |-
  A Coq implementation of Sokoban, the Japanese warehouse
  keeper's game.

authors:
- name: Jasper Stein
  initial: true
- name: Hugo Herbelin

maintainers:
- name: Érik Martin-Dorel
  nickname: erikmd

opam-file-maintainer: erik@martin-dorel.org

opam-file-version: dev

license:
  fullname: GNU Lesser General Public License v2.1 or later
  identifier: LGPL-2.1-or-later

supported_coq_versions:
  text: 8.10 or later
  opam: '{>= "8.10"}'

tested_coq_opam_versions:
- version: 'dev'
- version: '8.20'
- version: '8.19'
- version: '8.18'
- version: '8.17'
- version: '8.16'
- version: '8.15'
- version: '8.14'
- version: '8.13'
- version: '8.12'
- version: '8.11'
- version: '8.10'

namespace: Coqoban

keywords:
- name: Sokoban
- name: puzzle
- name: game
  
categories:
- name: Miscellaneous/Logical Puzzles and Entertainment

build: |-
  ## Building instructions

  The recommended way to use Coqoban is to build the
  project locally:

  ```shell
  git clone https://github.com/coq-community/coqoban.git
  cd coqoban
  make   # or make -j <number-of-cores-on-your-machine> 
  ```

  However, you can also build and install the whole project via
  [opam](https://opam.ocaml.org/doc/Install.html):

  ```shell
  opam repo add coq-released https://coq.inria.fr/opam/released
  opam install coq-coqoban
  ```

documentation: |
  ## Documentation

  Welcome to Coqoban!

  This is a Coq implementation of Sokoban, the Japanese
  warehouse keeper's game. The keeper must push the boxes to specified
  destination places. He can only push one box at a time, no more, and
  he can't pull. How to put the boxes in place?

  Thanks to [jsCoq](https://jscoq.github.io), you can play Coqoban
  [directly in your browser](https://coq.vercel.app/fun/coqoban.html)
  without installing Coq!
  
  If you want to install and run Coq and Coqoban locally:

  * [Coqoban\_engine.v](theories/Coqoban_engine.v) contains the actual Sokoban
      implementing script/program/data. It has a fair amount of
      remarks explaining what's going on, for those interested to know
      more about this implementation.

      You may just load this file into your favorite Coq editor and play.

  * [Coqoban\_levels.v](theories/Coqoban_levels.v) contains 355 levels to be
      played with `Coqoban_engine`.

  To import both the engine and levels in Coq:
  ```coq
  From Coqoban Require Import Coqoban_levels.
  ```
  
  The levels are called `Level_1` up to `Level_355`. From
  [Coqoban\_levels.v](theories/Coqoban_levels.v):
  
  ```coq
  (* These Sokoban levels I have taken from the game KSokoban and include all of the *)
  (* Sasquatch (1-50), Mas Sasquatch (51-100), Sasquatch III (101-150), Microban *)
  (* (151-305), and Sasquatch IV (306-355) collections. These collections are made by *)
  (* David W. Skinner (sasquatch@bentonrea.com) http://users.bentonrea.com/~sasquatch/ *)
  ```
  
  There are more levels on [this website](http://www.abelmartin.com/rj/sokobanJS/Skinner/David%20W.%20Skinner%20-%20Sokoban.htm).
  You can download them and transform them into additional `Coqoban_levels`.v-like files using the Haskell program [ksoq2coqsok.hs](src/ksoq2coqsok.hs).
  And obviously you can define your own new levels.
  Beware that Coq's lexer requires spaces after `X` and `O`!
  See [Coqoban\_engine.v](theories/Coqoban_engine.v) for more details on parsing/printing.
  
  To play, say, e.g.,

  ```coq
  Coq < Goal (solvable Level_274).
  1 subgoal
  
    ============================
     (solvable Level_274)
  
  Unnamed_thm < unfold Level_274. (* Optional but useful *)
  1 subgoal
  
    ============================
     solvable
       |> # # # # # # # # # # # # # # <|
       |> # _ _ _ _ _ _ # _ _ _ _ _ # <|
       +> # _ X + X X _ # _ O _ O O # <|
       |> # # _ # # _ # # # _ # # _ # <|
       |> _ # _ # _ _ _ _ _ _ _ # _ # <|
       |> _ # _ # _ _ _ # _ _ _ # _ # <|
       |> _ # _ # # # # # # # # # _ # <|
       |> _ # _ _ _ _ _ _ _ _ _ _ _ # <|
       |> _ # # # # # # # # # # # # # <|
       |><|
  ```
       
  Boards are represented by rows between `|>` and `<|`. Other signs:

  * `_` = open field
  * `#` = wall
  * `+` = YOU
  * `O` = destination square
  * `X` = box
  * `*` = a box on a destination square
  * `o` = YOU, on a destination square
  
  Tactics used to play Coqoban are:
  * `n.` (step/push north)
  * `e.` (step/push east)
  * `s.` (step/push south)
  * `w.` (step/push west)
  
  These apply even if there's a wall in the way. You can also use Coq
  tacticals, e.g.,

  ```coq
  do 5 n.
  Undo 3.
  Restart.
  Abort.
  ```

  Share and enjoy!
---