This is the topic to ask questions on the talk "Hierarchy Builder".
The talk will start in 5 minutes
Enrico is totally OK to get questions interactively rather than at the end
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?
Is there a way to fill in the arguments for a structure in a more interactive way?
OK, thanks
@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?
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}.
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?
there is a "git extension pack" pulling everything in. The one providing the feature you saw is probably called "GitLens"
@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, ...
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
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
Hi, are there any plans to allow parametric definitions in HB (such as for modules over a ring)? Or are there any current workarounds?
@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
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
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.
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.
You have to look at the gallina sources, and the source code of Coq...
(I mean to know in general what gets imported with a module, outside the cope of HB)
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).
Yes, exactly.
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
@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 Import
ed)
The relevant part is that module HB
and NoHB
are supposed to be equivalent (in some form of syntactic equality)
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
Require
d)
I could if you really wish... but the equivalent is requiring the file and importing only HB
or NoHB
modules...
OK, I can do this only locally for my understanding, thanks
Karl Palmskog said:
OK, I can do this only locally for my understanding, thanks
I'm almost done.
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 ;)
https://github.com/math-comp/hierarchy-builder/tree/master/Coq2020_material/CoqWS_expansion
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 _)
Ok, you can even remove the unify notations and replace them with the unify
constant.
please PR what you do ;)
Thanks @Cyril Cohen the example is great, or better ugly, which proves our point ;-)
And there's not even a join...
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