search

math-comp / multinomials

Multinomials for the Mathematical Components library.
Other
14 stars 12 forks source link

Add coq-native support (if available) as per CEP 48 #45

Closed erikmd closed 3 years ago

erikmd commented 3 years ago

Subsumes and replaces PR https://github.com/math-comp/multinomials/pull/41

erikmd commented 3 years ago

Hi @strub, the PR is almost ready; I specifically prepared it in a "TDD" way.

An upside of the proposed patch is that it is not necessary to exclude Coq versions before 8.12.1.

However the job build (mathcomp/mathcomp:1.12.0-coq-8.12) still fails in a weird way: https://github.com/math-comp/multinomials/pull/45/checks?check_run_id=3727362037

@ejgallego do you have a idea of what's missing?

erikmd commented 3 years ago

do you have a idea of what's missing?

On second thought I guess this is precisely what we had documented in this section:

https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#note-to-library-developers-and-package-maintainers

Roughly, in order to ensure that coq-mathcomp-ssreflect are native-compiled with Coq < 8.13, one should just apply the CEP 48 / item 3 strategy (given coq-mathcomp-ssreflect is built using coq_makefile) in the coq-opam-archive…

I'll try do to this soon.

Cc @proux01 @CohenCyril FYI

proux01 commented 3 years ago

We can also just forget about Coq < 8.13 and coq-native, it would already be great to have things working with Coq >= 8.13. I'm not sure there are much users of Coq < 8.13 and native_compute around. native_compute with anything using multinomials is broken for more than six months now, having it work even with Coq >= 8.13 would be a huge progress.

erikmd commented 3 years ago

I see what you mean, but wouldn't it be a pity not to take advantage of coq-native for at least 8.12? As the fix is simple and documented (item 3 of the CEP 48, which BTW should have been applicable just as well for Coq 8.5+). Otherwise, if we give up this item-3 idea, this would strongly restrict the number of Coq versions we'll be able to compare for running ValidSDP benchmarks, for example.

Le 28 septembre 2021 08:49:09 GMT+02:00, Pierre Roux @.***> a écrit :

We can also just forget about Coq < 8.13 and coq-native, it would already be great to have things working with Coq >= 8.13. I'm not sure there are much users of Coq < 8.13 and native_compute around. native_compute with anything using multinomials is broken for more than six months now, having it work even with Coq >= 8.13 would be a huge progress.

-- You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub: https://github.com/math-comp/multinomials/pull/45#issuecomment-928904972

proux01 commented 3 years ago

I really don't care. My point is rather: don't put too much effort in supporting older versions as there isn't much use for it. Of course, if it's easy why not. But I'd really prefer something working with current versions to something not working at all.

strub commented 3 years ago

I really don't care. My point is rather: don't put too much effort in supporting older versions as there isn't much use for it. Of course, if it's easy why not. But I'd really prefer something working with current versions to something not working at all.

Same for me.

erikmd commented 3 years ago

I really don't care. My point is rather: don't put too much effort in supporting older versions as there isn't much use for it. Of course, if it's easy why not. But I'd really prefer something working with current versions to something not working at all.

OK. Regarding the effort involved, I'd say the vast majority of this effort is already done! (discussing and refining the CEP, preparing and merging the coq-native package, proposing a workflow to adapt packaging for both dune and coq_makefile).

Anyway, I agree with your pragmatism:

erikmd commented 3 years ago

I will push a tiny extra commit that won't require having (coq.8.12, mathcomp.1.12.0, coq-native) working…

done. Does this look good to you?

proux01 commented 3 years ago

LGTM However, this looks quite heavy, we'll definitely need to fix dune when 3.0 will be there to avoid such painful work.

ejgallego commented 3 years ago

@erikmd indeed that error usually happens when the native files for a depending library weren't compiled.