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

ejgallego · 2020-09-17T15:34:00Z

Configure is quite messy, but we will improve it once we can link it
with findlib and move to dune [that will actually allow to remove all
ad-hoc calls to ocamlfind in favor of findlib code.

Fixes coq#13041 coq#13047 Configure is quite messy, but we will improve it once we can link it with findlib and move to dune [that will actually allow to remove all ad-hoc calls to `ocamlfind` in favor of `findlib` code.

ejgallego · 2020-09-17T15:38:18Z

Nix needs a bump:

You have the Num library installed. Good!
Zarith version 1.10 is required, you have 1.9
Configuration script failed!

Zimmi48 · 2020-09-17T15:55:20Z

I opened a PR: NixOS/nixpkgs#98164

ejgallego · 2020-09-17T15:57:02Z

configure.ml

-    if vi < [3; 0; 0] then
+  try
+    let vl = numeric_prefix_list v in
+    let vn = List.map int_of_string vl in


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.

ejgallego · 2020-09-17T15:57:47Z

I opened a PR: NixOS/nixpkgs#98164

Thanks @Zimmi48 , please push the ref update when merged.

JasonGross · 2020-09-17T22:34:00Z

configure.ml

+    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)


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

Added this question to the next call.

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.

ejgallego · 2020-09-18T11:21:16Z

@JasonGross concern is orthogonal to this PR, which is IMO of high priority for users of master, thus I request to dismiss the review and go ahead.

JasonGross · 2020-09-18T15:05:50Z

Indeed, let's merge this PR and discuss whether or not to revert both the code dependency and this check on the call next week. I would suggest splitting this PR into two commits, though, one for lablgtk and one for zarith, so that it's easier to revert if that's what we decide to do.

JasonGross · 2020-09-18T15:07:12Z

Er, nevermind my suggestion about splitting the commits, I see that we'd actually still want the version check, and would just want to edit the numbers.

Zimmi48 · 2020-09-21T13:50:29Z

Thanks @Zimmi48 , please push the ref update when merged.

Done.

ejgallego · 2020-09-21T14:39:43Z

Done

Thanks a lot @Zimmi48 , this should be ready however the windows error is a bit bizarre :S

ejgallego · 2020-09-21T14:49:06Z

Thanks a lot @Zimmi48 , this should be ready however the windows error is a bit bizarre :S

I see that's unrelated, so IMHO if CI passes this should be ready to merge.

SkySkimmer

Looks OK

SkySkimmer · 2020-09-22T11:14:02Z

@coqbot: merge now

coqbot-app · 2020-09-22T11:14:03Z

@SkySkimmer: You can't merge the PR because some changes are requested.

‮

SkySkimmer · 2020-09-22T11:14:45Z

@coqbot: merge now

gares · 2020-09-28T14:49:10Z

configure.ml

+  try
+    let vl = numeric_prefix_list v in
+    let vn = List.map int_of_string vl in
+    if vn < [3; 1; 0] then


This must be >=

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

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

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.

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

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

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

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.

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...

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

[configure] Fix version checks for lablgtk and zarith

21366f8

Fixes coq#13041 coq#13047 Configure is quite messy, but we will improve it once we can link it with findlib and move to dune [that will actually allow to remove all ad-hoc calls to `ocamlfind` in favor of `findlib` code.

ejgallego requested review from a team as code owners September 17, 2020 15:34

ejgallego requested a review from a team September 17, 2020 15:34

ejgallego added this to the 8.13+beta1 milestone Sep 17, 2020

Zimmi48 added kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools. labels Sep 17, 2020

ejgallego commented Sep 17, 2020

View reviewed changes

JasonGross previously requested changes Sep 17, 2020

View reviewed changes

Bump nixpkgs to get zarith 1.10.

febcda9

ejgallego requested a review from a team as a code owner September 21, 2020 13:25

vbgl approved these changes Sep 21, 2020

View reviewed changes

SkySkimmer approved these changes Sep 22, 2020

View reviewed changes

SkySkimmer self-assigned this Sep 22, 2020

coqbot-app bot merged commit 5a9538e into coq:master Sep 22, 2020

ejgallego deleted the configure+fix_version_checks branch September 22, 2020 11:16

gares mentioned this pull request Sep 24, 2020

Upgrade bound on zarith coq/opam#1429

Merged

gares reviewed Sep 28, 2020

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

ejgallego commented Sep 17, 2020

ejgallego commented Sep 17, 2020

Zimmi48 commented Sep 17, 2020 •

edited

ejgallego Sep 17, 2020 •

edited

ejgallego commented Sep 17, 2020

JasonGross Sep 17, 2020

Zimmi48 Sep 18, 2020

ejgallego Sep 18, 2020

ejgallego commented Sep 18, 2020

JasonGross commented Sep 18, 2020

JasonGross commented Sep 18, 2020

Zimmi48 commented Sep 21, 2020

ejgallego commented Sep 21, 2020

ejgallego commented Sep 21, 2020

SkySkimmer left a comment

SkySkimmer commented Sep 22, 2020

coqbot-app bot commented Sep 22, 2020

SkySkimmer commented Sep 22, 2020

gares Sep 28, 2020

gares Sep 28, 2020

gares Sep 28, 2020

ejgallego Sep 28, 2020

Zimmi48 Sep 29, 2020

ejgallego Sep 29, 2020

ejgallego Sep 29, 2020

treinen Oct 2, 2020

ejgallego Oct 8, 2020

glondu Oct 9, 2020

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

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

Conversation

ejgallego commented Sep 17, 2020

ejgallego commented Sep 17, 2020

Zimmi48 commented Sep 17, 2020 • edited

ejgallego Sep 17, 2020 • edited

Choose a reason for hiding this comment

ejgallego commented Sep 17, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ejgallego commented Sep 18, 2020

JasonGross commented Sep 18, 2020

JasonGross commented Sep 18, 2020

Zimmi48 commented Sep 21, 2020

ejgallego commented Sep 21, 2020

ejgallego commented Sep 21, 2020

SkySkimmer left a comment

Choose a reason for hiding this comment

SkySkimmer commented Sep 22, 2020

coqbot-app bot commented Sep 22, 2020

SkySkimmer commented Sep 22, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Zimmi48 commented Sep 17, 2020 •

edited

ejgallego Sep 17, 2020 •

edited