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.

Sign up for GitHub

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

Jump to bottom

[configure] Fix version checks for lablgtk and zarith #13049

Merged
merged 2 commits into from Sep 22, 2020
Merged

[configure] Fix version checks for lablgtk and zarith #13049

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
21366f8
[configure] Fix version checks for lablgtk and zarith
ejgallego Sep 17, 2020
febcda9
Bump nixpkgs to get zarith 1.10.
Zimmi48 Sep 21, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion INSTALL.md
View file
Open in desktop
Expand Up @@ -32,7 +32,7 @@ To compile Coq yourself, you need:

- for CoqIDE, the
[lablgtk3-sourceview3](https://github.com/garrigue/lablgtk) library
(version >= 3.0.beta8), and the corresponding GTK 3.x libraries, as
(version >= 3.1.0), and the corresponding GTK 3.x libraries, as
of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18)

The IEEE-754 compliance is required by primitive floating-point
Expand Down
24 changes: 12 additions & 12 deletions configure.ml
View file
Open in desktop
Expand Up @@ -698,10 +698,16 @@ let check_for_numlib () =
die "Num library not installed, required for OCaml 4.06 or later"
| _ -> cprintf "You have the Num library installed. Good!");
let zarith,_ = tryrun camlexec.find ["query";"zarith"] in
let zarith_version, _ = run camlexec.find ["query"; "zarith"; "-format"; "%v"] in
match zarith with
| "" ->
die "Zarith library not installed, required"
| _ -> cprintf "You have the Zarith library installed. Good!"
| _ ->
let zarith_version_int = List.map int_of_string (numeric_prefix_list zarith_version) in
if zarith_version_int >= [1;10;0] then
cprintf "You have the Zarith library %s installed. Good!" zarith_version
else
die ("Zarith version 1.10 is required, you have " ^ zarith_version)
Comment on lines +707 to +710
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is not a single version of Ubuntu nor Debian which ships such a new zarith in libzarith-ocaml-dev. The newest (in Ubuntu focal and groovy and Debian bullseye and sid) is 1.9.1. If 1.9.1 is not new enough, I'd like to request that the switch to zarith be reverted until such time as there is at least some Ubuntu/Debian version with the relevant version of zarith, ideally a stable one (Debian stable currently ships 1.7.1). You can see the newest package versions at https://packages.ubuntu.com/search?keywords=ocaml-zarith&searchon=sourcenames and https://packages.debian.org/search?searchon=names&keywords=libzarith-ocaml

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added this question to the next call.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Usually we have this requirement on OCaml, as upgrading it is significantly complex; in particular it needs recompilation of all OCaml libs.

For an OCaml library I think the situation is much easier, whoever is uploading the Coq Debian package can also upload an updated zarith easily. Or alternatively, it can be vendored easily.


let numlib =
check_for_numlib ()
Expand All @@ -717,20 +723,14 @@ let get_lablgtkdir () =

let check_lablgtk_version () =
let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk3"] in
(true, v)

(* ejgallego: we wait to do version checks until an official release is out *)
(* try
let vi = numeric_prefix_list v in
(* Temporary hack *)
if vi = ["3";"0";"beta3"] then (false, v) else
let vi = List.map s2i vi in
if vi < [3; 0; 0] then
try
let vl = numeric_prefix_list v in
let vn = List.map int_of_string vl in
Copy link
Member Author

@ejgallego ejgallego Sep 17, 2020 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This kind of code is very fragile if the version does contain strings; but it is not easy to fix as string comparison will fail to handle "9" < "10". Only solution is to do the cleanup and vendor opam's code for version comparison.

if vn < [3; 1; 0] then
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This must be >=

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, the problem is not the comparison, but the beta version package by Debian I'm afraid.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@treinen apparently the META from from sid of lablgtk3 does not contain the version = .. line.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, one has to be careful to use the right upstream tar.bz2 that contains the correct meta, or indeed tell dune to generate a meta with a git commit hash + version.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I removed the "resolved" status so that @treinen will be able to spot this discussion more easily.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@treinen I see an override of build indeed; tho we can maybe see this briefly in person some of these days ?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actulally you are right about old makefile in lablgtk being not good for packagers, now the default make target just produces this:

Welcome to lablgtk Dune-based build system. Targets are

  - release:   build lablgtk package in release mode
  - dev:       build in developer mode [requires extra dependencies]
  - dev-all:   build in developer mode [requires extra dependencies]
  - nopromote: dev build but without re-running camlp5 generation
  - opam:      internal, used in CI testing
  - clean:     clean build tree

WARNING: Packagers should not use this makefile, but call dune
directly with the right options for their distribution, see README

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the bug report against the debian package of lablgtk3, @ejgallego, this is fixed now for the latest version in sid.

Concerning the override of the build target, I was looking at 3.1.0-3, and was missing the fact that @glondu had in the meantime uploaded a new version. My bad.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @treinen , I will follow up in Debian BTS; I do believe having a dh_ocaml_dune helper would be great, Dune developers would happily add some features to dune install for example would that help debian.

We could even instruct Dune to produce Debian packages, but that would be a bit inflexible w.r.t. Debian policy IMO, at least until Dune itself is a bit more generic [then dh_dune could just ship a plugin and everything would be taken care of] Note that dune already knows install files etc...

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ejgallego See also https://salsa.debian.org/ocaml-team/dh-ocaml/-/merge_requests/1

(false, v)
else
(true, v)
with _ -> (false, v)
*)

let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"

Expand Down Expand Up @@ -758,7 +758,7 @@ let check_coqide () =
else
let (ok, version) = check_lablgtk_version () in
let found = sprintf "LablGtk3 and LablGtkSourceView3 found (%s)" version in
if not ok then set_ide No (found^", but too old (required >= 3.0, found " ^ version ^ ")");
if not ok then set_ide No (found^", but too old (required >= 3.1.0, found " ^ version ^ ")");
(* We're now sure to produce at least one kind of coqide *)
lablgtkdir := shorten_camllib dir;
if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
Expand Down