search

imdea-software / fcsl-pcm

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

Release v1.2.0 after mathcomp 1.10.0 is out #15

Closed anton-trunov closed 4 years ago

anton-trunov commented 4 years ago

We use some of the future mathcomp 1.10.0's features, so fcsl-pcm's master branch only compiles with mathcomp's master

germanD commented 4 years ago

Hi @anton-trunov, I'm trying to fix my FCSL fork, as well as the main mathador FCSL dev branch. Currently they are not working with mathcomp's dev. Cherrypicking from here should work, right? At least for the lemmas that haven't changed between fcsl-pcm 1.x and whatever we should call the things that are in FCSL's gitlab.

anton-trunov commented 4 years ago

I think so, yes. Even if cherrypicking isn’t working, you might want to follow some solutions provided for this repo.

germanD commented 4 years ago

Well yes, I meant cherrypicking by hand. Indeed, some of the files that are in the FCSL "pre-release" (this year OOPSLA paper's artefact) have more content than their corresponding fcsl-pcm library ones.

I don't know what's the plan there, and I guess Aleks is waiting for having the new guy on board in Madrid before releasing FCSL in opam... but, I guess that at some point fcsl-pcm should be updated with those, and FCSL import the release libraries (and installl the dependency through opam).

This was the original plan, right?

anton-trunov commented 4 years ago

Released in https://github.com/coq/opam-coq-archive/pull/1071