Julien Puydt (Jun 08 2023 at 08:19): 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?
Pierre Roux (Jun 08 2023 at 08:24):The test is broken (or actually no longer broken ;) ) but the package isn't I think.
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?
Cyril Cohen (Jun 08 2023 at 08:35):Thanks for pointing that out: https://github.com/math-comp/hierarchy-builder/pull/358
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?
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 ?
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.
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: Sep 15 2024 at 13:02 UTC