Stream: Hierarchy Builder devs & users

Topic: HB logs


view this post on Zulip Aleksandar Nanevski (Sep 26 2023 at 16:50):

Hi.

I have been building an HB structure (see below), but I need to modify the default output that HB produces, to add annotations about universe polymorphism.

I was hoping that I could cut-and-paste the output of HB.structure called with the #[log] parameter, and then perform my
modifications.

However, it seems there is some disconnect between the log and what HB actually does. More concretely, I considered the following example.

From HB Require Import structures.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat eqtype seq path fintype.
Export Set Implicit Arguments.
Export Unset Strict Implicit.
Export Unset Printing Implicit Defensive.

Definition ordtype_axiom (T : eqType) (ord : rel T) :=
  [/\ irreflexive ord & transitive ord].

HB.mixin Record isOrdered T of Equality T := {
  ord : rel T;
  ordtype_subproof : ordtype_axiom ord}.

#[log]
#[short(type="ordType")]
HB.structure Definition Ordered :=
  {T of Equality T & isOrdered T}.

In this context, I can define

Definition unit_ord (x y : unit) := false.
Lemma unit_is_ordtype : ordtype_axiom unit_ord. Proof. by []. Qed.
HB.instance Definition _ := isOrdered.Build unit unit_is_ordtype.
Check (Ordered.clone unit _).

The last command typechecks, indicating that the ordered structure for unit type has been declared.

However, if I replace the structure definition what the #[log] that it produces, then

Check (Ordered.clone unit _).

stops working.

Is there some way to obtain the correct code implementing the HB.structure declaration?

Thanks,
Aleks

view this post on Zulip Enrico Tassi (Sep 26 2023 at 18:48):

Try #[log(raw)].
If it does not work, please open an issue.

view this post on Zulip Enrico Tassi (Sep 26 2023 at 19:24):

In general replacing one bit of HB with its "equivalent" Coq code won't work for what follows.
In particular all (maybe most of) the additions to Coq-Elpi databases are just comments, and subsequent calls to HB commands need these extra clauses (unless you replace them too with the equivalent Coq code).

If HB is not flexible enough, I recommend you open an issue and explain us what you need to change.

view this post on Zulip Karl Palmskog (Sep 26 2023 at 19:39):

so Plan B is effectively infeasible now? Maybe good to update https://github.com/math-comp/hierarchy-builder#plan-b

view this post on Zulip Cyril Cohen (Sep 27 2023 at 06:55):

Karl Palmskog said:

so Plan B is effectively infeasible now? Maybe good to update https://github.com/math-comp/hierarchy-builder#plan-b

Indeed plan B is out of the picture https://github.com/math-comp/hierarchy-builder/pull/389, thanks for pointing out the readme bit.

view this post on Zulip Enrico Tassi (Sep 27 2023 at 08:49):

We are going to remove it from CI. But planB has never been about mixing HB with non-HB. This would require much more infrastructure.
Just to give an example, HB.pack is a tactic that uses metadata stored in Elpi. If you declare your structures by hand, there is no Elpi clause telling you which is the constructor for the record to package the structure. Of course one could find it another way, after all it is a Coq inductive type, but we don't have such code. The log options are still very useful to explain how things work, we are keeping them.

Plan-B was to cope with the fact that maybe HB does not work for MC, so we drop it, and someone used it but cannot take over the maintainership, so he at least gets some code that compiles without HB via this planB thing. Now that HB is used in MC, we will maintain it.

view this post on Zulip Karl Palmskog (Sep 27 2023 at 08:55):

maybe this is worth flagging up explicitly in README - that (at least in my reading) adopting HB is practically all-or-nothing, not least for technical reasons, and log is only informative, not usable for copy-paste

view this post on Zulip Aleksandar Nanevski (Sep 27 2023 at 09:27):

Hi.

Indeed, I figured that the problem comes from what Enrico pointed out. If the structure isn't built with HB.structure, then the subsequent calls to HB.instance don't have access to the appropriate information in Elpi and can define the mixin, but don't declare the canonical instances.

In my example, the solution is to explicitly add the canonical declaration, as in

Definition unit_ord (x y : unit) := false.
Lemma unit_is_ordtype : ordtype_axiom unit_ord. Proof. by []. Qed.
HB.instance Definition unit_ord_mix := isOrdered.Build unit unit_is_ordtype.
Canonical unit_ordType : ordType :=
  Ordered.Pack (sort:=unit) (Ordered.Class unit_ord_mix).

That said, I wanted to modify HB code by hand in order to declare the structure polymorphic. Concretely, where the generated code is

Section type.
Record type  : Type := Pack { sort : Type; class : axioms_ sort; }.
End type.
Definition phant_clone := ....

I wanted to change it into

Section type.
Polymorphic Cumulative Record
  type : Type := Pack { sort : Type; _ : axioms_ sort; }.
End type.
Section PolymorphicClonePack.
Polymorphic Universe ou.
Polymorphic Variables (T : Type@{ou}) (cT : type@{ou}).
Polymorphic Definition phant_clone := ...

Maybe there's an option that could be passed to HB to do this automatically?

view this post on Zulip Enrico Tassi (Sep 27 2023 at 10:59):

Not yet, Elpi has access to the APIs for universe polymorphic stuff, but we did not manage to use them in a satisfactory way. https://github.com/math-comp/hierarchy-builder/tree/univ-poly

I cannot promise anything, but starting from November I may have the time to work again on this.
Our little experience was that just turning on universe polymorphism would result in too many universe arguments.
So the plan was to allow for something like HB.structure Definition s@{u1} := { T : Type@{u1} of M1... MN }, but this requires some work.

In the meanwhile, we could continue some experiments just tuning universe checking off. (never tried to fiddle with cumulativity).


Last updated: Apr 21 2024 at 01:02 UTC