eth-sri / ELINA

ELINA: ETH LIbrary for Numerical Analysis
http://elina.ethz.ch/
Other
129 stars 53 forks source link

OPAM packaging #16

Closed skcho closed 6 years ago

skcho commented 6 years ago

Hello, I am Sungkeun Cho. I am developing a buffer overrun analyzer (Inferbo) at Facebook. We are trying to use ELINA in our analyzer, so as a first step I tried packaging the ELINA library for OPAM as our analyzer is developed in OCaml. I would like to get some reviews if you don't mind packaging your great implementation. :blush:

There are three main changes.

cc: @mbouaziz

skcho commented 6 years ago

BTW, using LGPL-2.1 licensed code under LGPL-3 looks OK. LGPL-2.1 says,

If the Library specifies a version number of this License which applies to it and "any later version", you have the option of following the terms and conditions either of that version or of any later version published by the Free Software Foundation.

though I don't have 100% confidence still.

GgnDpSngh commented 6 years ago

Hi Sungkeun,

Thank you for the patch which should make it easier to compile and install ELINA including the OCaml interface. I tried your revisions on my system with -use-opam and without it and in both cases, the compiler produces the following error:

cc: error: unrecognized command line option ‘-install_name’

Do you know what I am missing? I think LGPL-3 should work unless I am missing something. As for the version name, it may be better to start with 1.0 as there have been many changes to ELINA since it was first released.

Cheers, Gagan

skcho commented 6 years ago

Hi Gagan,

cc: error: unrecognized command line option ‘-install_name’

Oh, I should have tried it in another OS and compilers. I will revise that. :sweat_smile: Thank you for your try.

As for the version name, it may be better to start with 1.0

OK. Great! I will change it too.

Sincerely, Sungkeun

skcho commented 6 years ago

Dear Gagan,

I changed it to use the -install_name option only when it is MacOS, by adopting the build script of Apron. I tested opam pin add elina . in MacOS and Linux(CentOS), and there was no issues. Could you try it again?

Thanks, Sungkeun

GgnDpSngh commented 6 years ago

Hi Sungkeun,

Thanks a lot for your changes, ELINA builds except the ocaml_interface now. The configure script seems to create HAS_OCAML=1 even if I do not specify -use-opam. Is it the intended behavior or I am missing something?

Cheers, Gagan

skcho commented 6 years ago

It was intended one, but if you want to disable HAS_OCAML by default, e.g., when -use-opam is not given, I will change it. :smiley:

GgnDpSngh commented 6 years ago

Yes, some users do not have ocaml and it is better to give them this option. Let me know when it is done, so i can merge.

Cheers, Gagan

skcho commented 6 years ago

Hi Gagan,

Thank you for your reply. I changed it to disable HAS_OCAML by default. For now, OCaml support is enabled only when there is a configuration option, -use-ocaml, -use-ocamlfind, or -use-opam; instead, I removed the options -no-ocaml and -no-ocamlfind from the configure because disabling OCaml supports is default now.

Sincerely, Sungkeun

GgnDpSngh commented 6 years ago

Hi Sungkeun,

Thanks a lot for the update. I have merged master with your branch. Will update the ELINA website to reflect the latest build options. Let me know if there is any other issue with ELINA.

Cheers, Gagan

skcho commented 6 years ago

Hi Gagan,

Thank you very much for the review and merge. :heart:

In order to complete the OPAM packaging, we need to do some more things.

  1. Making a tarball (e.g. elina-1.0.tar.gz) for the package manager to get the same files by its version name.

  2. Adding ELINA's info to the main opam repository: If the tarball link is prepared, we can make a PR to the main opam repository, which makes opam users can easily install ELINA with one command, opam install elina.

Though (1) is impossible for me as I can't change tags on your repository, I can do (2) if you are happy with that. :wink:

Sincerely, Sungkeun