search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

Use of fcsl namespace and packaging #2

Closed palmskog closed 6 years ago

palmskog commented 6 years ago

Note that since this development uses the namespace/directory fcsl (and not, say, fcslpcm or fcsl_pcm), it would conflict with any other (OPAM) package in the future that also uses the namespace fcsl. For example, if I first installed both coq-fcsl-pcm and the other hypothetical package via OPAM, and then removed coq-fcsl-pcm, the other package's files would be removed also. Are you sure this won't be an issue in the future, i.e., that there will be no packaging of other FCSL code?

anton-trunov commented 6 years ago

The current plan is to deprecate coq-fcsl-pcm at some point and release the full coq-fcsl library which will include coq-fcsl-pcm.

palmskog commented 6 years ago

So if I port something to this library now, I will have to re-port it again to the full coq-fcsl in the near future? Can you give some indication of how much things will change going from coq-fcsl-pcm to coq-fcsl?

anton-trunov commented 6 years ago

We are only planning to add more stuff, like more instances of pcm structure, morphisms between PCMs, some examples of verification of concurrent algorithms. So coq-fcsl-pcm is essentially a stripped down version of the future coq-fcsl library, but that one will be released only in the second half of this year.

palmskog commented 6 years ago

OK, that sounds reasonable as long as the core definitions don't undergo radical changes. Here's an example of what it took to port one project to coq-fcsl-pcm from HTT, for reference.

anton-trunov commented 6 years ago

Thanks for sharing this. I will add your projects to the future coq-fcsl's CI.