-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add meta.yml and generate opam file, README.md and CI
- Loading branch information
Showing
4 changed files
with
236 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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: | ||
| - master | ||
| 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| # 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. | ||
|
|
||
| Besides MathComp, this project also uses the Equations plugin. | ||
|
|
||
| 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" | ||
| ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,117 @@ | ||
| --- | ||
| fullname: Functional Data Structures and Algorithms in SSReflect | ||
| shortname: fav-ssr | ||
| opam_name: coq-fav-ssr | ||
| organization: coq-community | ||
| community: true | ||
| action: true | ||
| 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. | ||
| Besides MathComp, this project also uses the Equations plugin. | ||
| 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 <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 | ||
| --- |