Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

GMP-ECM, a library for elliptic curve method based prime number checks #20105

Merged
merged 2 commits into from Dec 1, 2021

Conversation

MSoegtropIMC
Copy link
Contributor

This PR adds GMP-ECM, a C/C++ library for elliptic curve method based prime number checks and proof certificates to opam.

This library is used by a tool to generate primality proofs for (large) prime numbers for Coq.

This PR does not contain an OCaml wrapper for the library since the Coq proof generator is also written in C, but I still think it might be useful in the non Coq part of the OCaml world. If you think this is a bit of a stretch, I am fine to include it in Coq's separate opam repository.

This is a "compile from sources" package tested on macOS MacPorts, macOS homebrew, Ubuntu and Windows. A corresponding package is available in various OS package managers, but partially outdated versions not suitable for use in Coq.

@MSoegtropIMC MSoegtropIMC marked this pull request as draft November 26, 2021 12:54
packages/gmp-ecm/gmp-ecm.7.0.3/opam Outdated Show resolved Hide resolved
Co-authored-by: Kartik Singhal <kartiksinghal@gmail.com>
@mseri
Copy link
Member

mseri commented Nov 29, 2021

While,centos/fedora/oraclelinux seem all fine, alpine/debian/ubuntu all contain the following error

- libtool: install: chmod 644 /home/opam/.opam/4.12/lib/libecm.a
- libtool: install: ranlib /home/opam/.opam/4.12/lib/libecm.a
- libtool: finish: PATH="/home/opam/.opam/4.12/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/sbin" ldconfig -n /home/opam/.opam/4.12/lib
- /home/opam/.opam/4.12/.opam-switch/build/gmp-ecm.7.0.3/libtool: line 1719: ldconfig: command not found

is that something we should worry about?

@MSoegtropIMC
Copy link
Contributor Author

MSoegtropIMC commented Nov 30, 2021

@mseri : are you looking at an old CI run? I had this initially but fixed it by adding ("conf-libtool" {build}) - the CI runs after that went through for all platforms.

The latest CI run - after replacing CXX with CPP - seems to hang on MacOS (since a day or so).

@mseri
Copy link
Member

mseri commented Nov 30, 2021

For the macos builders, that happens, they are still experimental, don't rely too much on those

@mseri
Copy link
Member

mseri commented Nov 30, 2021

Looks like ldconfig should be provided by libc-bin (at least on debian-based distribution). I would be curious to understand if it is somehow missing, or maybe the sandbox is preventing access, I don't know. I would expect more things to fail badly if it was really missing

@MSoegtropIMC
Copy link
Contributor Author

@mseri : I read about this and as it looks ldconfig is a root tool, so it is normal than one can't run it. I think it is also not desirable to run it, the ""./configure" "--prefix" prefix" is sufficient in the opam C++ world (I usually need to tell programs which need the library to search the opam lib folder for it - the library doesn't come with a pkgconfig file).

I can also confirm that the result works on Ubuntu as expected.

One could think about patching the makefile such that it doesn't even try to run libtool in such a way that it tries to modify the system load path - which IMHO is a bug if configured with a prefix - but this might be tricky because the makefile is automake generated - I didn't have a closer look, though.

@MSoegtropIMC
Copy link
Contributor Author

@mseri : I would have to look at this on a VM. I had a look at the libtool script generated by automake and libtool on my Mac, and it doesn't contain a call to ldconfig.

Btw.: the autogenerated libtool script has 11645 lines, the autogenerated configure file 19360 lines and the autogenerated Makefile 2819 lines. I am always astonished that this automake stuff works at all despite being so insanely complicated, but I guess that it works is all one can expect then.

@MSoegtropIMC
Copy link
Contributor Author

MSoegtropIMC commented Dec 1, 2021

@mseri, @dinosaure : IMHO this is ready to merge. The failing ldconf call - which is correct to fail in an opam environment - is I would say a bug in libtool and I don't see chances that we get this fixed any time soon.

It might even be the right thing - if one would run opam as root, the libtool call to ldconf would succeed and add the installation target folder to the system wide load paths. Possibly this is intentional in libtool.

As far as I can tell there is no other open point, so I don't understand the "needs reporter action" label.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants