Stream: Coq workshop 2020

Topic: [M1] Hierarchy Builder


view this post on Zulip Théo Zimmermann (Jun 24 2020 at 11:20):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 07:55):

The talk will start in 5 minutes

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 07:56):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Jul 06 2020 at 08:19):

OK, thanks

view this post on Zulip 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?

view this post on Zulip 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}.

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip 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, ...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Jul 06 2020 at 08:41):

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

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip Maxime Dénès (Jul 06 2020 at 08:57):

Yes, exactly.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Jul 06 2020 at 16:20):

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

view this post on Zulip 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.

view this post on Zulip 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 ;)

view this post on Zulip Cyril Cohen (Jul 06 2020 at 16:24):

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

view this post on Zulip 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 _)

view this post on Zulip Cyril Cohen (Jul 06 2020 at 16:30):

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

view this post on Zulip Cyril Cohen (Jul 06 2020 at 16:30):

please PR what you do ;)

view this post on Zulip Enrico Tassi (Jul 06 2020 at 17:53):

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

view this post on Zulip Enrico Tassi (Jul 06 2020 at 17:54):

And there's not even a join...

view this post on Zulip 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: Feb 06 2023 at 05:03 UTC