[M1] Hierarchy Builder · Coq workshop 2020

Stream: Coq workshop 2020

Topic: [M1] Hierarchy Builder

Théo Zimmermann (Jun 24 2020 at 11:20):

This is the topic to ask questions on the talk "Hierarchy Builder".

Emilio Jesús Gallego Arias (Jul 06 2020 at 07:55):

The talk will start in 5 minutes

Emilio Jesús Gallego Arias (Jul 06 2020 at 07:56):

Enrico is totally OK to get questions interactively rather than at the end

Guillaume Melquiond (Jul 06 2020 at 08:17):

Does HB support the case of a structure that meets several structures plus a mixin and/or glue? Or do we still need to do it in two separate steps?

Michael Soegtrop (Jul 06 2020 at 08:18):

Is there a way to fill in the arguments for a structure in a more interactive way?

Michael Soegtrop (Jul 06 2020 at 08:19):

OK, thanks

Michael Soegtrop (Jul 06 2020 at 08:21):

@Enrico Tassi An unrleated question: you seem to have a VSCode plugin which shows who changed which line (I guess via GIT). Can you please point me to it?

Cyril Cohen (Jul 06 2020 at 08:21):

Guillaume Melquiond said:

Does HB support the case of a structure that meets several structures plus a mixin and/or glue? Or do we still need to do it in two separate steps?

You need to define the additional mixin/glue with HB.mixin, but then you can write HB.structure Definition s := {T of everything you want}.

Karl Palmskog (Jul 06 2020 at 08:22):

are there any fully worked examples where one can see both the code with HB (HB.Instance, etc.) and what the "exact same" manually written code without HB would look like?

Enrico Tassi (Jul 06 2020 at 08:23):

there is a "git extension pack" pulling everything in. The one providing the feature you saw is probably called "GitLens"

Enrico Tassi (Jul 06 2020 at 08:25):

@Karl Palmskog The FSCD paper has one almost complete example. From Coq you can Print Module CMonoid for example and see some stuff, but not everything since Print Module does not print "metadata" such as notations, canonical structures, ...

Cyril Cohen (Jul 06 2020 at 08:25):

Karl Palmskog said:

are there any fully worked examples where one can see both the code with HB (HB.Instance, etc.) and what the "exact same" manually written code without HB would look like?

This is how we started, but I am not sure the example is up to date... so I don't think we have this... it would be feasible but lenghty

Karl Palmskog (Jul 06 2020 at 08:28):

unfortunately, I don't think Print Module would be a substitute for seeing the actual manual code... I hope you will consider doing an example (not necessarily super lengthy) where one can actually do the file diff to understand the semantics

Daniel Kirk (Jul 06 2020 at 08:29):

Hi, are there any plans to allow parametric definitions in HB (such as for modules over a ring)? Or are there any current workarounds?

Enrico Tassi (Jul 06 2020 at 08:31):

@Daniel Kirk the master branch already contains the code for parameters. We did not release it yet because we want to test it more, in particular on Math Comp. See for example https://github.com/math-comp/hierarchy-builder/blob/master/demo5/hierarchy_0.v that contains a hierarchy with modules

Cyril Cohen (Jul 06 2020 at 08:31):

Daniel Kirk said:

Hi, are there any plans to allow parametric definitions in HB (such as for modules over a ring)? Or are there any current workarounds?

This is in the current master, it is done in theory, in practice there are still many bugs that we are hunting these days

Cyril Cohen (Jul 06 2020 at 08:38):

Karl Palmskog said:

unfortunately, I don't think Print Module would be a substitute for seeing the actual manual code... I hope you will consider doing an example (not necessarily super lengthy) where one can actually do the file diff to understand the semantics

I will try.

Enrico Tassi (Jul 06 2020 at 08:41):

I believe we should try to improve Print Module, even outside the context of HB I guess it would be nice to know that one gets exactly when he imports a module. Today you have to look at the sources, AFAIK.

Maxime Dénès (Jul 06 2020 at 08:41):

You have to look at the gallina sources, and the source code of Coq...

Maxime Dénès (Jul 06 2020 at 08:47):

(I mean to know in general what gets imported with a module, outside the cope of HB)

Enrico Tassi (Jul 06 2020 at 08:57):

Maxime Dénès said:

You have to look at the gallina sources, and the source code of Coq...

I guess you mean that some extra logical things (eg hints, coercions...) have a scope that is not very well documented (read surprising).

Maxime Dénès (Jul 06 2020 at 08:57):

Yes, exactly.

Cyril Cohen (Jul 06 2020 at 16:13):

Cyril Cohen said:

Karl Palmskog said:

are there any fully worked examples where one can see both the code with HB (HB.Instance, etc.) and what the "exact same" manually written code without HB would look like?

This is how we started, but I am not sure the example is up to date... so I don't think we have this... it would be feasible but lenghty

@Karl Palmskog I stopped after two structures, because if was already exhausting!
~~https://github.com/math-comp/hierarchy-builder/blob/master/Coq2020_material/CoqWS_expansion.v~~
https://github.com/math-comp/hierarchy-builder/tree/master/Coq2020_material/CoqWS_expansion

Karl Palmskog (Jul 06 2020 at 16:16):

@Cyril Cohen looks good, but any chance you could put the HB / non-HB versions in separate files? (and then the separate files would be "equal" when viewed as Coq modules, e.g., when Imported)

Cyril Cohen (Jul 06 2020 at 16:16):

The relevant part is that module HB and NoHB are supposed to be equivalent (in some form of syntactic equality)

Cyril Cohen (Jul 06 2020 at 16:19):

Karl Palmskog said:

Cyril Cohen looks good, but any chance you could put the HB / non-HB versions in separate files? (and then the separate files would be "equal" when viewed as Coq modules, e.g., when Required)

I could if you really wish... but the equivalent is requiring the file and importing only HB or NoHB modules...

Karl Palmskog (Jul 06 2020 at 16:20):

OK, I can do this only locally for my understanding, thanks

Cyril Cohen (Jul 06 2020 at 16:21):

Karl Palmskog said:

OK, I can do this only locally for my understanding, thanks

I'm almost done.

Cyril Cohen (Jul 06 2020 at 16:22):

Cyril Cohen said:

Karl Palmskog said:

OK, I can do this only locally for my understanding, thanks

I'm almost done.

And actually it revealed a bug in the NoHB that was using HB by accident ;)

Cyril Cohen (Jul 06 2020 at 16:24):

https://github.com/math-comp/hierarchy-builder/tree/master/Coq2020_material/CoqWS_expansion

Karl Palmskog (Jul 06 2020 at 16:29):

ah, it appears withoutHB.v can be completely standalone:

diff --git a/Coq2020_material/CoqWS_expansion/withoutHB.v b/Coq2020_material/CoqWS_expansion/withoutHB.v
index 1912996..c46f143 100644
--- a/Coq2020_material/CoqWS_expansion/withoutHB.v
+++ b/Coq2020_material/CoqWS_expansion/withoutHB.v
@@ -1,7 +1,11 @@
 (* Accompanying material to Coq workshop presentation *)
-From Coq Require Import ssreflect ssrfun ZArith.
-From HB Require Import structures.
+From Coq Require Import ssreflect ssrfun ZArith String.
 Set Warnings "-redundant-canonical-projection".
+Import String.StringSyntax.
+
+Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option (string * Type)) :=
+  phantom T1 t1 -> phantom T2 t2.
+Definition id_phant {T} {t : T} (x : phantom T t) := x.

 (* Helpers *)
 Notation "[unify t1 'with' t2 ]" := (unify t1 t2 _)

Cyril Cohen (Jul 06 2020 at 16:30):

Ok, you can even remove the unify notations and replace them with the unify constant.

Cyril Cohen (Jul 06 2020 at 16:30):

please PR what you do ;)

Enrico Tassi (Jul 06 2020 at 17:53):

Thanks @Cyril Cohen the example is great, or better ugly, which proves our point ;-)

Enrico Tassi (Jul 06 2020 at 17:54):

And there's not even a join...

Enrico Tassi (Jul 06 2020 at 17:58):

IIRC it is when you put something on top of a diamond that the code grows non linearly

Last updated: Jun 01 2023 at 11:01 UTC