Stream: Hierarchy Builder devs & users

Topic: Trouble with HB in Debian with Coq 8.17.0


view this post on Zulip Julien Puydt (Jun 08 2023 at 08:19):

Debian is frozen since months so I hadn't updated any Coq-related packages.

Since the new release is planned next week, I'll finally be able to push new versions so I started planning the updates.

I have now packages for coq 1.17.0, elpi 1.16.10 and coq-elpi 1.17.1.

HB is still 1.4.0, and the package doesn't build anymore, because line 20 in tests/infer.v doesn't fail... is it normal?

view this post on Zulip Pierre Roux (Jun 08 2023 at 08:24):

The test is broken (or actually no longer broken ;) ) but the package isn't I think.

view this post on Zulip Julien Puydt (Jun 08 2023 at 08:25):

Well, the package is broken if its testsuite doesn't pass... so I should just drop that test?

view this post on Zulip Cyril Cohen (Jun 08 2023 at 08:35):

Thanks for pointing that out: https://github.com/math-comp/hierarchy-builder/pull/358

view this post on Zulip Julien Puydt (Jun 08 2023 at 08:55):

Will you do a new release I'll just package or should I patch the previous one?

view this post on Zulip Cyril Cohen (Jun 08 2023 at 08:59):

I suggest you patch the previous one. There is more than one problem in the test suite for coq 8.17 and I do not see the point of releasing just to fix the test suite. BTW why is the debian package running the test-suite in the first place ?

view this post on Zulip Julien Puydt (Jun 08 2023 at 09:03):

It's a normal part of compiling a package: compile the software and check the result isn't broken.

view this post on Zulip Julien Puydt (Jun 08 2023 at 09:33):

I also found a few trivial whitespace issues, but now my package builds:

Description: fix the test suite for Coq 8.17
Author: Cyril Cohen & Julien Puydt
Forwarded: discussed with upstream

--- coq-hierarchy-builder.orig/tests/infer.v
+++ coq-hierarchy-builder/tests/infer.v
@@ -17,7 +17,7 @@
 HB.structure Definition bar A P B := { T of barm A P B T }.

 #[skip="8.1[0-5].*"] HB.check (bar.type_ bool nat bool).
-#[skip="8.16.*", fail] HB.check (bar.type_ bool nat bool).
+#[skip="8.1[6-9].*", fail] HB.check (bar.type_ bool nat bool).
 Print bar.phant_type.
 Print bar.type.
 Check bar.type bool nat bool.
--- coq-hierarchy-builder.orig/tests/compress_coe.v.out
+++ coq-hierarchy-builder/tests/compress_coe.v.out
@@ -1,4 +1,4 @@
-Datatypes_prod__canonical__compress_coe_D =
+Datatypes_prod__canonical__compress_coe_D =
 fun D D' : D.type =>
 {|
   D.sort := D.sort D * D.sort D';
--- coq-hierarchy-builder.orig/tests/hnf.v.out
+++ coq-hierarchy-builder/tests/hnf.v.out
@@ -1,12 +1,12 @@
-Datatypes_nat__canonical__hnf_S =
+Datatypes_nat__canonical__hnf_S =
 {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
      : S.type
-HB_unnamed_mixin_12 =
+HB_unnamed_mixin_12 =
 {| M.x := f.y nat HB_unnamed_factory_10 + 1 |}
      : M.axioms_ nat
-Datatypes_bool__canonical__hnf_S =
+Datatypes_bool__canonical__hnf_S =
 {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |}
      : S.type
-HB_unnamed_mixin_16 =
+HB_unnamed_mixin_16 =
 Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13
      : M.axioms_ bool

Last updated: Apr 21 2024 at 02:41 UTC