Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Stdlib discussion


view this post on Zulip Ali Caglayan (Feb 17 2022 at 14:07):

@Cyril Cohen Here

view this post on Zulip Ali Caglayan (Feb 17 2022 at 14:07):

Let's discuss the Stdlib here

view this post on Zulip Cyril Cohen (Feb 17 2022 at 14:07):

Thanks!

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

view this post on Zulip Cyril Cohen (Feb 17 2022 at 15:39):

I got disconnected

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

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

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

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

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

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

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

view this post on Zulip Tomás Díaz (Feb 17 2022 at 15:59):

(for instance, why does vernac depends on tactics :shrug: )

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

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

view this post on Zulip 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: Jan 29 2023 at 14:02 UTC