Jason Gross (Jul 28 2023 at 05:02): Jason Gross (Jul 28 2023 at 05:02):I am trying to build coq-interval (not via opam, because duplicating the entire ocaml install for every version of Coq is too heavy), and I see
File "./src/Float/Primitive_ops.v", line 485, characters 4-51:
Error:
In nested Ltac calls to "now (tactic)", "t" (bound to
rewrite Hp'; compute; split; [ | left; lra ]) and
"lra", last call failed.
No applicable tactic.
Failed to build src/Float/Primitive_ops.vo
./configure gave
$ ./configure
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C... yes
checking whether gcc accepts -g... yes
checking for gcc option to enable C11 features... none needed
checking how to run the C preprocessor... gcc -E
checking for coqc... /home/jgross/.local64/bin/coqc
checking Coq version... 81700
checking for coqdep... /home/jgross/.local64/bin/coqdep
checking for coqdoc... /home/jgross/.local64/bin/coqdoc
checking for ocamlfind... /home/jgross/.opam/4.11.2+fp/bin/ocamlfind
checking for Flocq... yes
checking for Flocq >= 4.1... yes
checking for primitive floats... yes
checking for Ssreflect... yes
checking for MathComp version... 2
checking for Coquelicot... yes
checking for Bignums... yes
checking for native development files... yes
checking for bytecode development files... yes
checking for g++... g++
checking whether the compiler supports GNU C++... yes
checking whether g++ accepts -g... yes
checking for g++ option to enable C++11 features... none needed
configure: building remake...
/usr/bin/ld: /tmp/cc9jepz2.o: in function `main':
remake.cpp:(.text.startup+0xbb3): warning: the use of `tempnam' is dangerous, better use `mkstemp'
=== Summary ===
Vernacular directory /home/jgross/.local64/coq/coq-8.17.0/lib/coq/user-contrib/Interval
Plugin directory /home/jgross/.opam/4.11.2+fp/lib/coq-interval
Primitive floats yes
Language tactics yes
Plot tactic native bytecode
configure: creating ./config.status
config.status: creating Remakefile
config.status: creating src/Plot.v
config.status: creating src/Missing/Int63Compat.v
config.status: creating src/Missing/MathComp1or2.v
I'm running
Jason Gross (Jul 28 2023 at 05:08):The goal lra is failing to solve is
((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * (R1 + R1))))))))))))))))))))))))))))))))))))))))))))))))))))
<
R1 + (R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * ((R1 + R1) * (R1 + R1))))))))))))))))))))))))))))))))))))))))))))))))))))%R
(cc @Guillaume Melquiond )
Jason Gross (Jul 28 2023 at 05:09):lra is defined here as Ltac lra := first [ psatzl R | psatzl QArith_base.Q ] according to Print Ltac
Jason Gross (Jul 28 2023 at 05:13):When I convert to Z, the goal is 9007199254740992 < 4503599627370497, which is false...
Jason Gross (Jul 28 2023 at 05:16):Before compute; left; lra, the goal is le_upper (Xreal 9007199254740992) (toX (ldexp (of_uint63 (Uint63.of_Z (Z.shiftr 9007199254740992 (Z.log2 9007199254740992 - 52)) + 1)) (Z.log2 9007199254740992 - 52)))
Jason Gross (Jul 28 2023 at 05:19):Which I guess simplifies to le_upper (Xreal 9007199254740992) (toX (ldexp 4503599627370497 (53 - 52)))
Jason Gross (Jul 28 2023 at 05:22):Possibly this is the issue?
Print ldexp. (* = fun (f : PrimFloat.float) (_ : Z) => f
: PrimFloat.float -> Z -> PrimFloat.float *)
Locate ldexp.
(*
Constant Flocq.IEEE754.PrimFloat.ldexp
Notation Coq.Floats.FloatOps.ldexp
(shorter name to refer to it in current context is FloatOps.ldexp)
Notation Flocq.IEEE754.PrimFloat.Z.ldexp
(shorter name to refer to it in current context is Z.ldexp)
Constant Coq.Floats.FloatOps.Z.ldexp
(shorter name to refer to it in current context is FloatOps.Z.ldexp)
*)
Relevant code in Flocq is
(* Compatibility workaround, remove once requiring Coq >= 8.15 *)
Definition ldexp f (_ : Z) : float := f.
Definition frexp (f : float) := (f, Z0).
Import FloatOps.
Module Import Z.
Notation ldexp := ldexp.
Notation frexp := frexp.
End Z.
Import Floats.
Import Zaux BinarySingleNaN.
(Why not Local Definition ldexp ... @Erik Martin-Dorel @Pierre Roux ?)
Jason Gross (Jul 28 2023 at 05:27):In any case, replacing ldexp with Z.ldexp seems to fix the problem.
Jason Gross (Jul 28 2023 at 05:28):Should I be reporting an issue somewhere? (Is there a way to get an INRIA gitlab account?)
Jason Gross (Jul 28 2023 at 05:29):(I also need to replace frexp with Z.frexp)
Jason Gross (Jul 28 2023 at 05:31):Overall patch is
diff --git a/src/Float/Primitive_ops.v b/src/Float/Primitive_ops.v
index 35622d9..d25eed0 100644
--- a/src/Float/Primitive_ops.v
+++ b/src/Float/Primitive_ops.v
@@ -59,7 +59,7 @@ Definition fromZ_UP (p : precision) x :=
let d := Z.log2 x in
let e := (d - 52)%Z in
let m := Z.shiftr x e in
- ldexp (of_int63 (of_Z m + 1)) e
+ Z.ldexp (of_int63 (of_Z m + 1)) e
end
| Zneg x =>
match (x ?= 9007199254740992)%positive (* 2^53 *) with
@@ -69,7 +69,7 @@ Definition fromZ_UP (p : precision) x :=
let d := Z.log2 x in
let e := (d - 52)%Z in
let m := Z.shiftr x e in
- next_up (ldexp (-(of_int63 (of_Z m))) e)
+ next_up (Z.ldexp (-(of_int63 (of_Z m))) e)
end
end.
@@ -84,7 +84,7 @@ Definition fromZ_DN (p : precision) x :=
let d := Z.log2 x in
let e := (d - 52)%Z in
let m := Z.shiftr x e in
- next_down (ldexp (of_int63 (of_Z m)) e)
+ next_down (Z.ldexp (of_int63 (of_Z m)) e)
end
| Zneg x =>
match (x ?= 9007199254740992)%positive (* 2^53 *) with
@@ -94,7 +94,7 @@ Definition fromZ_DN (p : precision) x :=
let d := Z.log2 x in
let e := (d - 52)%Z in
let m := Z.shiftr x e in
- ldexp (-(of_int63 (Int63.of_Z m + 1))) e
+ Z.ldexp (-(of_int63 (Int63.of_Z m + 1))) e
end
end.
@@ -494,7 +494,7 @@ intros prec [ |p|p]; unfold fromZ_UP.
apply Zle_minus_le_0.
refine (proj1 (Z.log2_le_pow2 _ _ _) _); [now simpl| ].
generalize (Pos2Z.pos_lt_pos _ _ Hp'); lia. }
- rewrite <-(B2Prim_Prim2B (ldexp _ _)) at 1; rewrite toX_Prim2B.
+ rewrite <-(B2Prim_Prim2B (Z.ldexp _ _)) at 1; rewrite toX_Prim2B.
rewrite ldexp_equiv.
generalize (shiftr_pos p Pe); intros [H1 H2]; revert H1 H2; fold e s.
intros [_ H1] H2.
@@ -717,7 +717,7 @@ assert (Pe : (0 <= e)%Z).
apply Zle_minus_le_0.
refine (proj1 (Z.log2_le_pow2 _ _ _) _); [now simpl| ].
generalize (Pos2Z.pos_lt_pos _ _ Hp'); lia. }
-rewrite <-(B2Prim_Prim2B (ldexp _ _)) at 1; rewrite toX_Prim2B.
+rewrite <-(B2Prim_Prim2B (Z.ldexp _ _)) at 1; rewrite toX_Prim2B.
rewrite ldexp_equiv, opp_equiv.
rewrite Bldexp_Bopp_NE.
rewrite BtoX_Bopp.
@@ -2594,7 +2594,7 @@ case (Prim2B x) as [s|s| |s m e B]; clear x; [ |now simpl..| ]; intros _.
rewrite toX_Prim2B, Prim2B_B2Prim; unfold BtoX.
set (f := B2Prim (B754_finite s m e B)).
generalize (frexp_equiv f).
-unfold frexp.
+unfold Z.frexp.
case frshiftexp as [f' e'].
generalize (Bfrexp_correct _ _ _ (Prim2B f)).
unfold f; rewrite Prim2B_B2Prim; clear f.
CoqInterval is no longer in Coq CI and its own CI doesn't test Coq master (only 8.11.0 and 8.17.0) so I wouldn't expect it to compile on master. I opened a merge request with your patch there though: https://gitlab.inria.fr/coqinterval/interval/-/merge_requests/10 Thanks for taking the time to investigate.
Pierre Roux (Jul 28 2023 at 14:37):@Jason Gross merged: https://gitlab.inria.fr/coqinterval/interval/-/merge_requests/10
Jason Gross (Jul 28 2023 at 16:02):Did it get removed from Coq CI for some reason?
Michael Soegtrop (Jul 28 2023 at 16:22):As far as I remember it was never in Coq CI. I think Guillaume prefers to adjust it to releases of Coq and not touch it in between. It would be useful though (I found a few inconsistencies based on coq-interval results).
Michael Soegtrop (Jul 28 2023 at 16:24):But then from a Coq Platform point of view the way Guillaume does it works perfectly fine, so we should respect his preference in managing his projects.
Jason Gross (Jul 28 2023 at 17:10):I guess my main interest in having coq-interval be in CI would be so that I could add the project I'm working on to Coq's CI as well (though this is currently blocked on #17833)
Guillaume Melquiond (Jul 29 2023 at 04:16):Michael Soegtrop said:
As far as I remember it was never in Coq CI.
It was. But at some point, it became a bit too much if a hindrance, since 1. Flocq was stuck at version 3 in the CI, and 2. I was in the process of implementing the Plot command. (Coq's CI makes it tedious to maintain any kind of OCaml code in a backward compatible way.)
Michael Soegtrop (Jul 29 2023 at 08:06):@Guillaume Melquiond : so would you be fine with adding it back now (any may be removing it again in case you do some intense work on it)?
Guillaume Melquiond (Jul 31 2023 at 07:08):I don't really care one way or other. But note that there are various requirements in order to be part of the CI, which are not currently fulfilled: https://github.com/coq/coq/blob/master/dev/ci/README-users.md
Last updated: Oct 13 2024 at 01:02 UTC