diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 0000000..c5cd081 --- /dev/null +++ b/.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 diff --git a/README.md b/README.md index 88783bd..de162a2 100644 --- a/README.md +++ b/README.md @@ -1,14 +1,53 @@ + # 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 +``` ## Contents diff --git a/coq-fav-ssr.opam b/coq-fav-ssr.opam new file mode 100644 index 0000000..0442d89 --- /dev/null +++ b/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: "palmskog@gmail.com" +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" +] diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..1999c55 --- /dev/null +++ b/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: palmskog@gmail.com + +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 + ``` + +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 +---