-
Notifications
You must be signed in to change notification settings - Fork 13
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
switch from Travis to Github CI, use coq template
- Loading branch information
Showing
5 changed files
with
179 additions
and
73 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,33 @@ | ||
| # 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.13.0-coq-8.13' | ||
| - 'mathcomp/mathcomp:1.14.0-coq-8.15' | ||
| - 'mathcomp/mathcomp-dev:coq-dev' | ||
| fail-fast: false | ||
| steps: | ||
| - uses: actions/checkout@v2 | ||
| - uses: coq-community/docker-coq-action@v1 | ||
| with: | ||
| opam_file: 'coq-fcsl-pcm.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 was deleted.
Oops, something went wrong.
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 |
|---|---|---|
| @@ -1,38 +1,41 @@ | ||
| # 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" | ||
| maintainer: "FCSL <[email protected]>" | ||
|
|
||
| homepage: "http://software.imdea.org/fcsl/" | ||
| bug-reports: "https://github.com/imdea-software/fcsl-pcm/issues" | ||
| homepage: "https://github.com/imdea-software/fcsl-pcm" | ||
| dev-repo: "git+https://github.com/imdea-software/fcsl-pcm.git" | ||
| bug-reports: "https://github.com/imdea-software/fcsl-pcm/issues" | ||
| license: "Apache-2.0" | ||
|
|
||
| build: [ make "-j%{jobs}%" ] | ||
| install: [ make "install" ] | ||
| synopsis: "Partial Commutative Monoids" | ||
| description: """ | ||
| The PCM library provides a formalisation of Partial Commutative Monoids (PCMs), | ||
| a common algebraic structure used in separation logic for verification of | ||
| pointer-manipulating sequential and concurrent programs. | ||
|
|
||
| The library provides lemmas for mechanised and automated reasoning about PCMs | ||
| in the abstract, but also supports concrete common PCM instances, such as heaps, | ||
| histories, and mutexes. | ||
|
|
||
| This library relies on propositional and functional extentionality axioms.""" | ||
|
|
||
| build: [make "-j%{jobs}%"] | ||
| install: [make "install"] | ||
| depends: [ | ||
| "coq" {(>= "8.13" & < "8.16~") | (= "dev")} | ||
| "coq-mathcomp-ssreflect" {(>= "1.13.0" & < "1.15~") | (= "dev")} | ||
| "coq" { (>= "8.13" & < "8.16~") | (= "dev") } | ||
| "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") } | ||
| ] | ||
|
|
||
| tags: [ | ||
| "keyword:separation logic" | ||
| "keyword:partial commutative monoid" | ||
| "category:Computer Science/Data Types and Data Structures" | ||
| "keyword:partial commutative monoids" | ||
| "keyword:separation logic" | ||
| "keyword:concurrency" | ||
| "logpath:fcsl" | ||
| ] | ||
| authors: [ | ||
| "Aleksandar Nanevski" | ||
| ] | ||
| synopsis: "Partial Commutative Monoids" | ||
| description: """ | ||
| The PCM library provides a formalisation of Partial Commutative Monoids (PCMs), | ||
| a common algebraic structure used in separation logic for verification of | ||
| pointer-manipulating sequential and concurrent programs. | ||
| The library provides lemmas for mechanised and automated reasoning about PCMs | ||
| in the abstract, but also supports concrete common PCM instances, such as heaps, | ||
| histories and mutexes. | ||
|
|
||
| This library relies on extensionality axioms: propositional and | ||
| functional extentionality.""" | ||
| url { | ||
| src: "git+https://github.com/imdea-software/fcsl-pcm.git#master" | ||
| } |
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,79 @@ | ||
| fullname: The PCM library | ||
| shortname: fcsl-pcm | ||
| organization: imdea-software | ||
| opam_name: coq-fcsl-pcm | ||
| community: false | ||
| action: true | ||
| coqdoc: false | ||
|
|
||
| synopsis: >- | ||
| Partial Commutative Monoids | ||
| description: |- | ||
| The PCM library provides a formalisation of Partial Commutative Monoids (PCMs), | ||
| a common algebraic structure used in separation logic for verification of | ||
| pointer-manipulating sequential and concurrent programs. | ||
| The library provides lemmas for mechanised and automated reasoning about PCMs | ||
| in the abstract, but also supports concrete common PCM instances, such as heaps, | ||
| histories, and mutexes. | ||
| This library relies on propositional and functional extentionality axioms. | ||
| authors: | ||
| - name: Aleksandar Nanevski | ||
| initial: true | ||
|
|
||
| maintainers: | ||
| - name: Alexander Gryzlov | ||
| nickname: clayrat | ||
|
|
||
| opam-file-maintainer: [email protected] | ||
|
|
||
| opam-file-version: dev | ||
|
|
||
| license: | ||
| fullname: Apache-2.0 | ||
| identifier: Apache-2.0 | ||
| file: LICENSE | ||
|
|
||
| supported_coq_versions: | ||
| text: Coq 8.13 to 8.15 | ||
| opam: '{ (>= "8.13" & < "8.16~") | (= "dev") }' | ||
|
|
||
| tested_coq_opam_versions: | ||
| - version: '1.13.0-coq-8.13' | ||
| repo: 'mathcomp/mathcomp' | ||
| - version: '1.14.0-coq-8.15' | ||
| repo: 'mathcomp/mathcomp' | ||
| - version: 'coq-dev' | ||
| repo: 'mathcomp/mathcomp-dev' | ||
|
|
||
| dependencies: | ||
| - opam: | ||
| name: coq-mathcomp-ssreflect | ||
| version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }' | ||
| description: |- | ||
| [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io) | ||
| namespace: fcsl | ||
|
|
||
| keywords: | ||
| - name: partial commutative monoids | ||
| - name: separation logic | ||
| - name: concurrency | ||
|
|
||
| categories: | ||
| - name: Computer Science/Data Types and Data Structures | ||
|
|
||
| documentation: |- | ||
| ## Getting help | ||
| If you need assistance or would like to report a bug, drop us an email: | ||
| <[email protected]> or open an [issue](https://github.com/imdea-software/fcsl-pcm/issues). | ||
| ## History and context | ||
| More information can be obtained via the [FCSL web page](https://software.imdea.org/fcsl/). | ||
| An earlier version of this library was developed as a part of [Hoare type | ||
| theory](https://github.com/imdea-software/htt), which is now rebased on FCSL-PCM. The original | ||
| version of HTT can be found [here](https://software.imdea.org/~aleks/htt/). |