Ali Caglayan (Feb 17 2022 at 14:07): Ali Caglayan (Feb 17 2022 at 14:07):@Cyril Cohen Here
Ali Caglayan (Feb 17 2022 at 14:07):Let's discuss the Stdlib here
Cyril Cohen (Feb 17 2022 at 14:07):Thanks!
Ali Caglayan (Feb 17 2022 at 15:06):Here is an example of quotient types in Coq:
(** * Quotients in Coq *)
Local Unset Elimination Schemes.
Module Export Quotient.
Private Inductive Quotient@{i j u}
{A : Type@{i}} (R : A -> A -> Type@{j}) : Type@{u} :=
| class : A -> Quotient R.
Arguments class {A R} a.
Axiom glue
: forall {A : Type} {R : A -> A -> Type} {a b : A},
R a b -> (@class A R a) = (class b).
Definition Quotient_rect {A : Type} {R : A -> A -> Type}
(P : Quotient R -> Type)
(class' : forall a, P (class a))
(glue' : forall a b (s : R a b), eq_rect _ _ (class' a) _ (glue s) = class' b)
: forall x, P x := fun x =>
match x with
| class a => class' a
end.
Axiom Quotient_rect_beta_glue
: forall {A : Type} {R : A -> A -> Type}
(P : Quotient R -> Type)
(class' : forall a, P (class a))
(glue' : forall a b (s : R a b), eq_rect _ _ (class' a) _ (glue s) = class' b)
(a b: A) (s : R a b),
f_equal_dep _ (Quotient_rect P class' glue') (glue s) = glue' a b s.
End Quotient.
Arguments class {A R} a.
Arguments Quotient A%type_scope R.
Notation "[ x ]" := (class x).
Require Import ZArith.
Local Open Scope Z_scope.
Definition IsRational : Z * Z -> Z * Z -> Type :=
fun '(a, b) '(c, d) => a * d = b * c.
Definition Q := Quotient IsRational.
Notation "a / b" := (@class _ IsRational (a, b)).
Lemma foo : 10 / 2 = 5 / 1.
Proof.
cbv.
apply glue.
reflexivity.
Defined.
I got disconnected
Tomás Díaz (Feb 17 2022 at 15:46):Posting it here because the talk in the video moved on lol.
I can give my comment as a newcomer - I haven't found information (be it text, diagrams, etc.) on the overall architecture of coq, it's pipelines, processes, etc. So I'm wondering how developers handle the information (are there groups who are "island" experts, with a huge truck factor, or does everyone knows everything, etc?), and plan for next steps. I imagine it could be useful to design the expected overall architecture, to understand the different subdomains, their interfaces, etc. and use that as a reference to guide the development of coq towards something "better" (beyond particular features)
Tomás Díaz (Feb 17 2022 at 15:46):I don't know whether this have been discussed or anything, but that's my first impression coming here
Tomás Díaz (Feb 17 2022 at 15:47):and I guess it relates to @Maxime Dénès comment on people having different priorities, having fragmented designs/development
Kenji Maillard (Feb 17 2022 at 15:49):@Tomás Díaz I share similar difficulties to "enter" the coq codebase. To the best of my knowledge there is some documentation in the dev directory in coq sources (see this README), and also in the ocaml sources.
Tomás Díaz (Feb 17 2022 at 15:50):Also, to me this relates with many of the things I've heard in the talks, that it's hard to maintain many things/add things, so idk if there are plans/project on redesigning the overall architecture to one that allows easier extensions/mantention (thinking solely on the engineering side), and actually having a (time/effort) slot to drive it that way
Tomás Díaz (Feb 17 2022 at 15:57):Some first steps (if they don't exist yet lol) could actually be just laying out the current dependencies, pipelines/processes, e.g. taking code examples and making diagrams of the different modules and how they communicate with each other, just to get an overview of how things flow xd
Tomás Díaz (Feb 17 2022 at 15:59):I ran this (dune-deps) to get a dependency graph, which to me doesn't make much sense rn :laughing: , but I guess even things like this could help (at least for newcomers).
tdeps.png
Tomás Díaz (Feb 17 2022 at 15:59):(for instance, why does vernac depends on tactics :shrug: )
Hanneli Tavante (Feb 17 2022 at 16:02):If you are not on BBB now, Arthur shared the slides http://www.chargueraud.org/temp/2022_02_17_hackathon_chargueraud.pdf
Hugo Herbelin (Feb 17 2022 at 21:06):Tomás Díaz said:
Also, to me this relates with many of the things I've heard in the talks, that it's hard to maintain many things/add things, so idk if there are plans/project on redesigning the overall architecture to one that allows easier extensions/mantention (thinking solely on the engineering side), and actually having a (time/effort) slot to drive it that way
There was and there is still difficult ongoing work on deeply clarifying the overall architecture that the core developers can be proud of. It is not an easy task. For instance, there are sometimes redundant codepaths which are not easy to factorize. Ask them and they'll be intarrissable on the subject.
Did you look at dev/doc in the archive. There are some documents, not always actively maintained but for instance, even if not updated for several years, the file dev/doc/coq-src-description.txt gives an idea of the overall architecture. Two noticeable new directories not listed there are engine for the existential-variable-based unification/proof engines (mostly forked out of pretyping), and vernac for the high-level commands (forked out of toplevel).
Gregory Malecha (Feb 18 2022 at 14:09):I'm sorry I missed the discussion, @Arthur Charguéraud. The slides were a good read. I agree with many of your points.\
Last updated: Jun 11 2023 at 00:30 UTC