add meta.yml and generate opam file, README.md and CI

.github/workflows/docker-action.yml

@@ -0,0 +1,36 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - trunk
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:1.19.0-coq-8.19'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-fav-ssr.opam'
+          custom_image: ${{ matrix.image }}
+
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -1,14 +1,53 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
 # Functional Data Structures and Algorithms in SSReflect
 
-A port of https://functional-algorithms-verified.org/ to Coq/SSReflect.
+[![Docker CI][docker-action-shield]][docker-action-link]
+[![Contributing][contributing-shield]][contributing-link]
+[![Code of Conduct][conduct-shield]][conduct-link]
+[![Zulip][zulip-shield]][zulip-link]
+
+[docker-action-shield]: https://github.com/coq-community/fav-ssr/actions/workflows/docker-action.yml/badge.svg?branch=trunk
+[docker-action-link]: https://github.com/coq-community/fav-ssr/actions/workflows/docker-action.yml
+
+[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
+[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
+
+[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg
+[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md
+
+[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg
+[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users
+
+
+
+A port of the book https://functional-algorithms-verified.org/ to Coq/SSReflect.
 
 The book was previously called "Functional Algorithms Verified", hence the FAV acronym.
 
-## Dependencies
+## Meta
+
+- Author(s):
+  - Alex Gryzlov (initial)
+- Coq-community maintainer(s):
+  - Alex Gryzlov ([**@clayrat**](https://github.com/clayrat))
+- License: [MIT license](LICENSE)
+- Compatible Coq versions: 8.15 to 8.19
+- Additional dependencies:
+  - [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+  - [MathComp algebra](https://math-comp.github.io)
+  - [Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
+- Coq namespace: `favssr`
+- Related publication(s): none
+
+## Building instructions
 
-- [MathComp ssreflect 1.17](https://math-comp.github.io)
-- [MathComp algebra](https://math-comp.github.io)
-- [Equations 1.3](https://mattam82.github.io/Coq-Equations/)
+To build manually, do:
+```shell
+make   # or make -j <number-of-cores-on-your-machine>
+```
 
 ## Contents
 

coq-fav-ssr.opam

@@ -0,0 +1,35 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "[email protected]"
+version: "dev"
+
+homepage: "https://github.com/coq-community/fav-ssr"
+dev-repo: "git+https://github.com/coq-community/fav-ssr.git"
+bug-reports: "https://github.com/coq-community/fav-ssr/issues"
+license: "MIT"
+
+synopsis: "A port of the Functional Data Structures and Algorithms book to Coq/SSReflect"
+description: """
+A port of the book https://functional-algorithms-verified.org/ to Coq/SSReflect.
+
+The book was previously called "Functional Algorithms Verified", hence the FAV acronym."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.15" & < "8.20"}
+  "coq-mathcomp-ssreflect" {>= "1.17" & < "2.0"}
+  "coq-mathcomp-algebra" 
+  "coq-equations" {>= "1.3"}
+]
+
+tags: [
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms"
+  "keyword:program verification"
+  "logpath:favssr"
+]
+authors: [
+  "Alex Gryzlov"
+]

meta.yml

@@ -0,0 +1,116 @@
+---
+fullname: Functional Data Structures and Algorithms in SSReflect
+shortname: fav-ssr
+opam_name: coq-fav-ssr
+organization: coq-community
+community: true
+action: true
+branch: trunk
+dune: false
+
+synopsis: A port of the Functional Data Structures and Algorithms book to Coq/SSReflect
+
+description: |-
+  A port of the book https://functional-algorithms-verified.org/ to Coq/SSReflect.
+
+  The book was previously called "Functional Algorithms Verified", hence the FAV acronym.
+
+authors:
+- name: Alex Gryzlov
+  initial: true
+
+maintainers:
+- name: Alex Gryzlov
+  nickname: clayrat
+
+opam-file-maintainer: [email protected]
+
+opam-file-version: dev
+
+license:
+  fullname: MIT license
+  identifier: MIT
+
+supported_coq_versions:
+  text: 8.15 to 8.19
+  opam: '{>= "8.15" & < "8.20"}'
+
+tested_coq_opam_versions:
+- version: '1.19.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+
+dependencies:
+- opam:
+    name: coq-mathcomp-ssreflect
+    version: '{>= "1.17" & < "2.0"}'
+  description: |-
+    [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+- opam:
+    name: coq-mathcomp-algebra
+  description: |-
+    [MathComp algebra](https://math-comp.github.io)
+- opam:
+    name: coq-equations
+    version: '{>= "1.3"}'
+  description: |-
+    [Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
+
+namespace: favssr
+
+keywords:
+- name: program verification
+
+categories:
+- name: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
+
+build: |-
+  ## Building instructions
+
+  To build manually, do:
+  ```shell
+  make   # or make -j <number-of-cores-on-your-machine>
+  ```
+
+documentation: |-
+  ## Contents
+
+  1. [Basics](src/basics.v)
+  ### Part I: Sorting and Selection
+  2. [Sorting](src/sorting.v)
+  3. [Selection](src/selection.v)
+  ### Part II: Search Trees
+  4. [Binary Trees](src/bintree.v)
+  5. [Binary Search Trees](src/bst.v)
+  6. [Abstract Data Types](src/adt.v)
+  7. [2-3 Trees](src/twothree.v)
+  8. [Red-Black Trees](src/redblack.v)
+  9. [AVL Trees](src/avl.v)
+  10. [Beyond Insert and Delete: \cup, \cap and -](src/beyond.v)
+  11. [Arrays via Braun Trees](src/braun.v)
+  12. [Tries](src/trie.v)
+  13. [Region Quadtrees](src/quadtree.v)
+  ### Part III: Priority Queues
+  14. [Priority Queues](src/priority.v)
+  15. [Leftist Heaps](src/leftist.v)
+  16. [Priority Queues via Braun Trees](src/braun_queue.v)
+  17. [Binomial Heaps](src/binom_heap.v)
+  ### Part IV: Advanced Design and Analysis Techniques
+  18. Dynamic Programming
+  19. Amortized Analysis
+  20. Queues
+  21. Splay Trees
+  22. Skew Heaps
+  23. Pairing Heaps
+  ### Part V: Selected Topics
+  24. Knuth–Morris–Pratt String Search
+  25. [Huffman’s Algorithm](src/huffman.v)
+  26. Alpha-Beta Pruning
+---