Missing join message

.github/workflows/main.yml

@@ -19,6 +19,7 @@ jobs:
         coq_version:
           - '8.15'
           - '8.16'
+          - '8.17'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1

.nix/config.nix

@@ -1,37 +1,37 @@
 {
   format = "1.0.0";
   attribute = "hierarchy-builder";
-  default-bundle = "coq-8.15";
+  default-bundle = "coq-8.16";
   bundles = let
     mcHBcommon = {
       mathcomp.override.version = "hierarchy-builder";
       mathcomp.job = true;
       mathcomp-single.job = true;
       hierarchy-builder-shim.job = true;
       mathcomp-single-planB-src.job = true;
-      mathcomp-single-planB.job = true;
       graph-theory.job = false;
       fourcolor.override.version = "master";
-      odd-order.override.version = "hirarchy-builder";
-      mathcomp-finmap.override.version = "proux01:hierarchy-builder";
-      mathcomp.analyis.override.version = "#694";
+      odd-order.override.version = "master";
+      mathcomp-finmap.override.version = "master";
+      mathcomp.analyis.override.version = "hierarchy-builder";
+      interval.override.version = "master";
+      reglang.override.version = "hierarchy-builder";
+      coq-bits.override.version = "hierarchy-builder";
+      deriving.job = false;
     };
   in {
-    "coq-mcHB-8.16".coqPackages = {
-      coq.override.version = "8.16";
-      mathcomp-analysis.override.version = "coq816";
-    } // mcHBcommon;
-
-    "coq-mcHB-8.15".coqPackages = {
-      coq.override.version = "8.15";
+    "coq-8.17".coqPackages = {
+      coq.override.version = "8.17";
     } // mcHBcommon;
 
     "coq-8.16".coqPackages = {
       coq.override.version = "8.16";
-      mathcomp.override.version = "mathcomp-1.15.0";
-    };
+    } // mcHBcommon;
+
     "coq-8.15".coqPackages = {
       coq.override.version = "8.15";
+      mathcomp.job = false;
+      mathcomp-infotheo.job = false;
     };
   };
   cachix.coq = {};

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"4f0eb194b37b6e0db28be2eb4643bd6924abf7ab"
+"721d4a5e7a4db115f7576828c354d62a84d7055b"

.nix/coq-overlays/mathcomp-single/default.nix

@@ -1,5 +1,2 @@
-{ mathcomp, coq-elpi, hierarchy-builder, version ? null }:
-(mathcomp.override {single = true;}).overrideAttrs (old: {
-  propagatedBuildInputs = old.propagatedBuildInputs ++
-                          [ coq-elpi hierarchy-builder ];
-})
+{ mathcomp, version ? null }:
+mathcomp.override {single = true; inherit version;}

HB/common/database.elpi

@@ -223,21 +223,24 @@ distinct-pairs-below CurrentClass AllSuper C1 C2 :-
     not(sub-class? C1 C2),
     not(sub-class? C2 C1),
     if (join C1n C2n C3n)
-       (assert-building-bottom-up CurrentClass C3n, fail) % a join, not a valid pair
+       (assert-building-bottom-up CurrentClass C3n C1n C2n, fail) % a join, not a valid pair
        true, % no join, valid pair
   ].
 
-pred assert-building-bottom-up i:class, i:classname.
-assert-building-bottom-up CurrentClass C3n :-
+pred assert-building-bottom-up i:class, i:classname, i:classname, i:classname.
+assert-building-bottom-up CurrentClass C3n C1n C2n :-
   class-def (class C3n X Y),
   CurrentClass = class CC _ _,
   if (not (sub-class? CurrentClass (class C3n X Y)))
-     (gref->modname CC 2 "." Before, gref->modname C3n 2 "." After,
-      Msg1 is "- declare structure " ^ Before ^ " before structure " ^ After ^ ";",
-      coq.error "You must declare the hierarchy bottom-up."
+     (gref->modname CC 1 "." Before, gref->modname_short C3n "." After,
+      Msg1 is "- declare structure " ^ Before ^ " before structure " ^ After ^ " if " ^ After ^ " inherits from it;",
+      Msg2 is "- declare an additional structure that inherits from both "
+        ^ {gref->modname_short C1n "."} ^ " and " ^ {gref->modname_short C2n "."}
+        ^ " and from which " ^ Before ^ " and/or " ^ After ^ " inherit.",
+      coq.error "You must declare the hierarchy bottom-up or addd a missing join."
        "There are two ways out:"
        Msg1
-       "- declare an additional structure from which both inherit")
+       Msg2)
      true.
 
 pred distinct-pairs_pair i:prop, o:pair class class.

coq-hierarchy-builder.opam

@@ -12,7 +12,7 @@ build: [ [ make "build"]
          [ make "test-suite" ] {with-test}
        ]
 install: [ make "install" ]
-depends: [ "coq-elpi" { (>= "1.14" & < "1.17~") | = "dev" } ]
+depends: [ "coq-elpi" { (>= "1.14" & < "1.18~") | = "dev" } ]
 conflicts: [ "coq-hierarchy-builder-shim" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """

tests/missing_join_error.v.out

@@ -1,4 +1,5 @@
 The command has indeed failed with message:
-You must declare the hierarchy bottom-up. There are two ways out: 
-- declare structure missing_join_error.A2B1 before structure missing_join_error.B2A1; 
-- declare an additional structure from which both inherit
+You must declare the hierarchy bottom-up or addd a missing join. 
+There are two ways out: 
+- declare structure A2B1 before structure B2A1 if B2A1 inherits from it; 
+- declare an additional structure that inherits from both A1 and A2 and from which A2B1 and/or B2A1 inherit.