Please create a tag for Coq 8.14 in Coq Platform 2021.11 about coqprime HOT 20 CLOSED

@MSoegtropIMC sorry coq is becoming too technological for me. I've lost my morning trying to compile coq8.14 and now I am stuck trying to compile bignums. Is there an easy to get a hold on coq8.14+rc1?

from coqprime.

@MSoegtropIMC I finally got something that seems to work (coq + bignums) and coqprime compiles for it. I wonder if the last commit by @SkySkimmer fixes the problem. Can you retry seeing if there is a problem with the current version of master.

from coqprime.

@thery : yes, I will try that.

Btw.: you might want to try the Coq Platform scripts linked above to reproduce the state I am testing. This branch includes Coq 8.14+rc1 (and a few other versions). The scripts should be easy to use. If you already have opam, they will create a new opam switch, so that nothing of your current opam state is touched, otherwise they will setup opam. Just download the zip from the above branch and run the coq_platform_make.sh script (for macOS, Linux or the .bat file on Windows). It will ask a few questions and then install opam, Coq, ....

from coqprime.

@MSoegtropIMC I have tried no problem with coq.8.14rc1 but I also need coq-bignums and it does not seem available.

from coqprime.

The Coq Platform development (main) branch tends to have a largish number of local opam patches. coq-bignums is included there.

See (https://github.com/coq/platform/tree/main/opam/opam-coq-archive/extra-dev/packages)
specifically (https://github.com/coq/platform/blob/main/opam/opam-coq-archive/extra-dev/packages/coq-bignums/coq-bignums.8.14.0/opam)

The reason I do it this way is that I need to change some opam packages a few times to adjust them to requirements of additional packages and it is less messy to publish the final result - I will do the PRs tomorrow.

from coqprime.

@MSoegtropIMC with coq 8.14 of the platform + local installation of bignum, the current version of Coqprime compiles. There are many warning about rewrite hint that I will try to fix soon.

from coqprime.

@thery : thanks, I will check what went wrong in my tests - maybe just a typo in a test script or the like.

from coqprime.

Hmm, when I try in the 8.14+rc1 version of Coq Platform (that is in opam switch __coq-platform.2021.09.0~8.14+beta1) the command:

opam install coq-coqprime.1.0.6

It fails with an error (only visible in the opam log file - the log tail has warnings):

File "./src/Coqprime/Z/ZCAux.v", line 188, characters 0-9:
Error: No product even after head-reduction.

Did you try installation via opam or did you compile it locally? Maybe something is wrong with the opam file (it works with 8.13, though).

from coqprime.

sorry I've compiled it against master, my bad.
I've just added a tag v8.14.

Sorry again to wasting your time,

from coqprime.

No issue - Coq Platform makes such tests quick.

So are you saying coq-prime 1.0.6 (which uses tag v8.12) works with Coq 8.13.2 and Coq master but not with 8.14+rc1?
Or did you mean you compiled coq-prime master against 8.14+rc1?

I don't see the tag on this git repo yet - did you push it?

from coqprime.

no I'ven´t retrieved 1.0.6 I was compiling coqprime/master with 8.14rc1

The tag is pushed now. Should I have to do a release 1.1?

from coqprime.

no I'ven´t retrieved 1.0.6 I was compiling coqprime/master with 8.14rc1

Ah ok, this explains it.

The tag is pushed now. Should I have to do a release 1.1?

You mean on opam? yes please!

from coqprime.

done #1849

from coqprime.

@MSoegtropIMC is it ok? can I close the issue?

from coqprime.

Please let me close it - I will do so in the next days (likely today). I need the issues to remain open until I updated Coq Platform to ensure that I don't forget anything.

from coqprime.

@thery : I updated Coq Platform 2021.09. Thanks!

from coqprime.

@thery : I made a straight forward autoconf file and it finds the libraries gmp and gmp-ecm.

But there is one issue: you use __ecm_get_random_ul (unsigned long) but the version of ecm available on macports (6.3) doesn't have this function, only __ecm_get_random_ui (for int instead of long).

I guess you need gmp-ecm 7.X - which means I would have to update gmp-ecm on MacPorts.

from coqprime.

@thery : I simply created an opam package for library gmp-ecm. This works. I guess for such rather exotic libraries this is the safest way to get a reproducible version in a platform independent way.

from coqprime.

@thery : the certificate generator is now also included in Coq Platform (well still in my local working branch, but soon).

from coqprime.

@MSoegtropIMC Thanks!

from coqprime.