imported from gitter room coq/metacoq · MetaCoq

I don't think so. I had a "implement tmOpaque command" on my todo-list for a while, but forgot about it. That would probably be the most flexible to use

Matthieu Sozeau (Sep 26 2019 at 09:18):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:18):

Matthieu Sozeau (Sep 26 2019 at 09:19):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:22):

Is there a way to tell Program not to use typeclass inference to close obligations? Even if I set Global Obligation Tactic := idtac. inferrable goals are closed

Yannick Forster (Gitter import) (Sep 26 2019 at 09:22):

Matthieu Sozeau (Sep 26 2019 at 09:23):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:24):

Then it's probably quickest to add a boolean to tmDefinitionRed (and set it to false by default for tmDefinition)

Gregory Malecha (Sep 26 2019 at 11:11):

Gregory Malecha (Sep 26 2019 at 12:21):

What is the current status of the branches? E.g. 8.8 vs 8.9? It looks like 8.8 is still the main branch, but I need my feature on 8.9

Yannick Forster (Gitter import) (Sep 26 2019 at 12:23):

Copy pasting from the Slack chat from15 minutes ago:

Yannick Forster [2:06 PM]
 What do we want to do about the 8.9 branch? I tried naively merging in 8.8, but that fails (in PCUICSafeConversion.v) 
Matthieu Sozeau [2:08 PM]
I'll give it a try

Yannick Forster (Gitter import) (Sep 26 2019 at 12:23):

So ideally we'll have an opam relase for 8.8 and 8.9 with synced branches ready this afternoon

Gregory Malecha (Sep 26 2019 at 12:31):

Yannick Forster (Gitter import) (Sep 26 2019 at 12:33):

We are used to coordinating the "Coq Coq Correct" paper draft over slack, so stuff like this is discussed there occasionally as well. I think it's essentially undecided which channel we should use for public discussions :)

Matthieu Sozeau (Sep 26 2019 at 13:33):

I think gitter is simpler given that Coq is already here (and not sure slack can be used easily by others)

Théo Winterhalter (Sep 26 2019 at 13:33):

Gregory Malecha (Sep 26 2019 at 13:36):

since i'm already in the code, i'm wondering if it makes sense to also expose Local

Gregory Malecha (Sep 26 2019 at 13:36):

type internal_flag =
  | UserAutomaticRequest
  | InternalTacticRequest
  | UserIndividualRequest

Yannick Forster (Gitter import) (Sep 26 2019 at 13:37):

Exposing all options that are avaible in interactive mode for definitions, lemmas and axioms makes probably sense

Gregory Malecha (Sep 26 2019 at 13:37):

Gregory Malecha (Sep 26 2019 at 13:38):

Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

(** flag for internal message display *)
type internal_flag =
  | UserAutomaticRequest (* kernel action, a message is displayed *)
  | InternalTacticRequest  (* kernel action, no message is displayed *)
| UserIndividualRequest (* user action, a message is displayed *)```

Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

Gregory Malecha (Sep 26 2019 at 13:40):

Gregory Malecha (Sep 26 2019 at 13:41):

type import_status = ImportDefaultBehavior | ImportNeedQualified

type locality = Discharge | Global of import_status

Gregory Malecha (Sep 26 2019 at 13:42):

Matthieu Sozeau (Sep 26 2019 at 14:12):

Gregory Malecha (Sep 26 2019 at 14:13):

Matthieu Sozeau (Sep 26 2019 at 14:13):

Gregory Malecha (Sep 26 2019 at 14:13):

Matthieu Sozeau (Sep 26 2019 at 14:14):

Gregory Malecha (Sep 26 2019 at 14:14):

it seems like this interface may have changed because 8.9 seems to just have Global and Local as locality

Gregory Malecha (Sep 26 2019 at 14:14):

Matthieu Sozeau (Sep 26 2019 at 14:15):

Gregory Malecha (Sep 26 2019 at 14:15):

Matthieu Sozeau (Sep 26 2019 at 14:15):

Gregory Malecha (Sep 26 2019 at 17:23):

my co-worker running manjaro ran into an error running make in the template-coq directory

Gregory Malecha (Sep 26 2019 at 17:24):

Gregory Malecha (Sep 26 2019 at 17:55):

Gregory Malecha (Sep 26 2019 at 17:57):

Error: Illegal application:
The term "@eq_refl" of type "forall (A : Type@{Coq.Init.Logic.8}) (x : A), x = x"
cannot be applied to the terms
 "forall T : Type@{Top.10}, T -> T" : "Type@{Top.10+1}"
 "fun (T : Type@{Top.10}) (x : T) => x" : "forall T : Type@{Top.10}, T -> T"
The 1st term has type "Type@{Top.10+1}" which should be coercible to
 "Type@{Coq.Init.Logic.8}".

Gregory Malecha (Sep 26 2019 at 17:57):

Gregory Malecha (Sep 26 2019 at 17:58):

Matthieu Sozeau (Sep 27 2019 at 09:07):

Matthieu Sozeau (Sep 27 2019 at 10:32):

Shall we just reset the counters and call the alpha release of metacoq 1.0alpha ?

Matthieu Sozeau (Sep 27 2019 at 10:32):

Yannick Forster (Gitter import) (Sep 27 2019 at 10:33):

Théo Winterhalter (Sep 27 2019 at 11:17):

Matthieu Sozeau (Sep 27 2019 at 11:17):

Théo Winterhalter (Sep 27 2019 at 11:18):

After the release are we moving from coq8-8 to coq8-9 for good?
To know in which branch to start making new changes.

Matthieu Sozeau (Sep 27 2019 at 11:19):

Théo Winterhalter (Sep 27 2019 at 11:19):

Matthieu Sozeau (Sep 27 2019 at 11:19):

Yannick Forster (Gitter import) (Sep 27 2019 at 11:56):

What's the status of the forward-port? I tried yesterday, but there was the issue with st_ in PCUICSafeChecker.v

Matthieu Sozeau (Sep 27 2019 at 12:04):

Didn't try yet. I'll give it a go before making the alpha releases in case things need to change in 8.8 somehow

Matthieu Sozeau (Sep 27 2019 at 12:05):

Matthieu Sozeau (Sep 27 2019 at 12:24):

Matthieu Sozeau (Sep 27 2019 at 12:25):

We should be more robust though and have our own wrapper around whichever sed is available

Gregory Malecha (Sep 27 2019 at 12:29):

I can check with him. We got it working by manually running the sed script for the plug-in.

Matthieu Sozeau (Sep 27 2019 at 13:13):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:16):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:17):

You adapted the announcement, right? Will you post it on Coq club/ discourse once the PR is merged?

Matthieu Sozeau (Sep 27 2019 at 13:22):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:27):

Matthieu Sozeau (Sep 27 2019 at 13:30):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:30):

Matthieu Sozeau (Sep 27 2019 at 13:31):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:57):

Matthieu Sozeau (Sep 27 2019 at 13:57):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:58):

I would suggest that we move up installation through opam to the top of the installation section, maybe even move installation from sources to a dedicated INSTALLATION.md file

Yannick Forster (Gitter import) (Sep 27 2019 at 13:59):

Matthieu Sozeau (Sep 27 2019 at 14:09):

Yannick Forster (Gitter import) (Sep 27 2019 at 15:05):

I've been wondering whether we can implement a tWildcard feature for tmUnquote and tmUnquoteTyped. Sometimes it's annoying that you have to write out types when doing a definition in a metaprogram which could easily be inferred if you'd give the definition in Coq directly

Yannick Forster (Gitter import) (Sep 27 2019 at 15:06):

One option could be to extend the definition of terms, but that sounds wrong. An alternative might be to define an opaque constant tWildcard : term (as `tVar "_" for instance) and adapt the unquoting function in ocaml for at least the non-extractable monad to treat it like a wildcard would be treated

Yannick Forster (Gitter import) (Sep 27 2019 at 15:07):

Matthieu Sozeau (Sep 27 2019 at 15:08):

Yannick Forster (Gitter import) (Sep 27 2019 at 15:08):

Matthieu Sozeau (Sep 27 2019 at 15:09):

Yannick Forster (Gitter import) (Sep 27 2019 at 15:10):

But yes, if unquoting would just try to infer evars instead of failing when encountering one that would solve the problem in an even nicer way

Yannick Forster (Gitter import) (Sep 27 2019 at 15:11):

Because you might be able to use the same evar twice to enforce that the same type is inferred

Matthieu Sozeau (Sep 27 2019 at 15:26):

Matthieu Sozeau (Sep 27 2019 at 15:27):

Yannick Forster (Gitter import) (Sep 27 2019 at 15:32):

Yannick Forster (Gitter import) (Sep 27 2019 at 15:33):

I can fix them myself if you tell me what you think about the ones phrased as questions

Matthieu Sozeau (Sep 27 2019 at 15:41):

Matthieu Sozeau (Sep 27 2019 at 15:44):

Matthieu Sozeau (Sep 27 2019 at 15:45):

Matthieu Sozeau (Sep 27 2019 at 15:53):

Matthieu Sozeau (Sep 27 2019 at 16:03):

I fixed the typos and added the missing links to safechecker_test and erasure_test

Yannick Forster (Gitter import) (Sep 27 2019 at 16:07):

By the partial translation I mean the extraction to lambda calculus by me and Fabian covered in section 4.3 of the MetaCoq paper

Matthieu Sozeau (Sep 27 2019 at 16:08):

Yannick Forster (Gitter import) (Sep 27 2019 at 16:08):

I like the announcement as it is, the "A good place to start" sentence just moved up into the itemize, which it probable shouldn't

Yannick Forster (Gitter import) (Sep 27 2019 at 16:09):

Matthieu Sozeau (Sep 27 2019 at 16:12):

Matthieu Sozeau (Sep 27 2019 at 16:14):

Matthieu Sozeau (Sep 27 2019 at 16:18):

Matthieu Sozeau (Sep 27 2019 at 16:23):

Yannick Forster (Gitter import) (Sep 27 2019 at 16:29):

Matthieu Sozeau (Sep 27 2019 at 16:30):

I added a link to the paper directly and the example, people can find their way I guess :)

Matthieu Sozeau (Sep 27 2019 at 16:34):

So, 8.9 opam packages work too, only remains to push them as a PR on the Coq repo, and wait 3 hours :)

Gregory Malecha (Sep 27 2019 at 17:07):

@Yannick Forster regarding wildcards. They would be awesome to support! But I think that care about be taken. I would personally prefer a new type to an opaque constant, and I would expose a monadic operation `tmElaborate : pre_term -> term. This also makes it possible to implement some forms of elaboration in the monad.

Gregory Malecha (Sep 27 2019 at 17:09):

The connection with tEvar is interesting, it seems like they should be the same...so maybe there is something slightly off about the current setup? Maybe term represents pre_term and there is a subset type that represents real terms.

Gregory Malecha (Sep 27 2019 at 17:10):

That said, I don't think enough information is persisted in terms to reconstruct everything about evars.

Théo Winterhalter (Sep 27 2019 at 17:15):

Gregory Malecha (Sep 27 2019 at 17:18):

After looking, it looks like tEVar has enough information, we might not need to add anything.

Matthieu Sozeau (Sep 27 2019 at 17:19):

Damn I used curl http:?/ | sha256sum which sums the http request stuff, have to copy the fixed hash again everywhere :/ Hopefully we can use opam-publish in the future

Gregory Malecha (Sep 27 2019 at 17:22):

Matthieu Sozeau (Sep 27 2019 at 17:50):

Matthieu Sozeau (Sep 27 2019 at 17:53):

Regarding tEvar we could associate arbitrary things to them, so I think they could be the right interface. Indeed right now we represent pre-terms (in the sense of econstr), but without the support of an evar-map (that will come though)

Matthieu Sozeau (Sep 27 2019 at 17:54):

Gregory Malecha (Sep 28 2019 at 01:50):

I think tEvar is the right interface. Do you have thoughts on how to handle the evar map though? In particular, i assume that every time that you run tmQuote you will get a fresh evar map

Gregory Malecha (Sep 30 2019 at 01:04):

could it be possible to use metacoq to construct a module inside a section (assuming that it is pre-"cooked", i.e. none of the definitions mention any section variables)

Théo Winterhalter (Sep 30 2019 at 07:24):

Well, as metacoq doesn’t handle modules or sections, I’m not sure. For each definition, putting it inside a section is just the identity if it doesn’t mentions tVars no?

Gregory Malecha (Sep 30 2019 at 11:32):

That's right. The top-level prevents you from opening a module at all within a section, but I was thinking that if we could simply generate the kernel object directly, we wouldn't need to worry about that. The reason that I'm wondering about this is because there is a more efficient representation of sealed functions using modules.

Matthieu Sozeau (Sep 30 2019 at 12:32):

Gregory Malecha (Sep 30 2019 at 13:39):

Matthieu Sozeau (Sep 30 2019 at 14:36):

Gregory Malecha (Sep 30 2019 at 16:58):

Gregory Malecha (Sep 30 2019 at 16:59):

Matthieu Sozeau (Sep 30 2019 at 17:42):

Yannick Forster (Gitter import) (Oct 07 2019 at 15:33):

I just found myself writing "The command is implemented in MetaCoq (which explains the Run TemplateProgram prefix)" and took this as a hint to rethink wether "Run TemplateProgram" is the most telling vernacular name possible. In line with MetaCoq Check, we might want to call it MetaCoq Run? (and rename Quote into MetaCoq Quote?) That way outsiders who find it in code have an idea where its coming from

Théo Winterhalter (Oct 07 2019 at 15:33):

Théo Winterhalter (Oct 07 2019 at 15:34):

Matthieu Sozeau (Oct 07 2019 at 15:34):

Yannick Forster (Gitter import) (Oct 07 2019 at 15:44):

I have to touch ML code tomorrow anyways, I'll file a pull request in case nobody objects until then

Jason Gross (Oct 08 2019 at 20:27):

Théo Winterhalter (Oct 08 2019 at 20:58):

Hi, when you say names you mean identifiers? I don’t really understand what you’re trying to do. Since you have a list of identity functions I assume you want the name of the binder each time?
So as input you would take for instance [ fun O => O ; fun S => S ] and forall N, N -> (N -> N) -> N?
Why not just take forall (N : Type) (O : N) (S : N -> N), N?

Anyway, if the three can be done separately, then can probably be composed into one thing.
You cannot create vernacular commands from metacoq though, you’ll have to do some Run TemplateProgram.

Jason Gross (Oct 08 2019 at 20:59):

Sure, I could compose them and take the names just from the eliminator, that's a fine starting point. And having to do Run TemplateProgram seems fine.

Jason Gross (Oct 08 2019 at 21:00):

The question is if I can make a template program that emits an inductive, then calls an Ltac tactic to emit a definition, and then issues a Strategy command

Théo Winterhalter (Oct 08 2019 at 21:05):

Ok, so the first part I would say yes. I’m not sure about the Ltac tactic though. I mean, we can open an obligation and let the user input the tactic then. Or even set the tactic obligation to the one you want, but that’s not very nice if you use other things that generate obligations.
If the ltac tactic is simple enough, it can be written in metacoq instead maybe.

As for Strategy, as far as I know it’s not reified as of now. I suppose it could be added without too much effort.

Jason Gross (Oct 08 2019 at 21:09):

I don't suppose a template program can set the obligation tactic and then revert the setting after? (The tactic takes arguments, though, which include the names of the inductives just emitted... I'm not super-enthusiastic about porting the tactic code from Ltac to MetaCoq at the moment; it's currently 2200 loc and does a number of hacks with evars and partial instantiation across multiple goals to transmit information between them, and also relies on emitting constants at particular times for good performance, and running particular reduction strategies on terms in various places. It also calls an Ltac reification procedure in the middle of things.)

Matthieu Sozeau (Oct 08 2019 at 22:26):

Shouldn't be too hard to call an ltac, passing arguments to them is a headache though

Théo Winterhalter (Oct 09 2019 at 06:40):

Yes I see, on what is the tactic run? Maybe it can be embedded in a different goal with extra information (with let bidings for instance that would just go away with simpl) so that the tactic can be called without arguments.

Théo Winterhalter (Oct 09 2019 at 06:40):

But otherwise, metacoq doesn’t allow you to change the obligation tactic either.

Jason Gross (Oct 09 2019 at 16:04):

Yes, I suppose I could embed the arguments in the goal structure as arguments to a definition that the tactic will then just unfold or something. So I could do it with a tactic that takes no arguments

Jason Gross (Oct 11 2019 at 06:21):

Would I be correct in assuming that Not_found anomalies in program definition (https://github.com/coq/coq/issues/10879) would also show up in trying to embed Ltac in MetaCoq?

Yannick Forster (Gitter import) (Oct 11 2019 at 07:31):

I think running Ltac is also possible by a combination of InferInstance and Hint Extern, ignoring obligations altogether. Passing arguments is also no issue I think. You could imagine a typeclass

Class RunLtac (tactic_name : string) {argument_type : Type} (args : argument_type) (return_type : Type) := mk_RunLtac : return_type.

together with hints of the form Hint Extern 0 (RunLtac "tac" ?a ?R) => tac a.

Yannick Forster (Gitter import) (Oct 11 2019 at 07:33):

We don't support Strategy right now, but there's also no reason why we shouldn't implement tmStrategy as a monadic operation, it should be essentially a copy-paste of the implementation of the Strategy vernacular

Matthieu Sozeau (Oct 11 2019 at 09:01):

Jason Gross (Oct 11 2019 at 15:42):

Unfortunately, typeclasses are subject to the same issues with Not_found, see https://github.com/coq/coq/issues/10879#issuecomment-541114794. Though if you add tmStrategy to a version of MetaCoq that works with 8.9/8.10, I will strongly consider switching from OCaml to MetaCoq for my automation here.

matrixbot (Gitter import) (Oct 11 2019 at 18:28):

pedroabreu What are the benefits to implement app with a list of arguments instead of only one argument and currying the result?

Matthieu Sozeau (Oct 12 2019 at 08:54):

It’s an implementation choice, to make heads of applications accessible in constant time and have a compact representation of argument lists. The PCUIC version of the language has standard binary apps

Matthieu Sozeau (Oct 12 2019 at 08:54):

Yannick Forster (Gitter import) (Oct 23 2019 at 13:11):

Yannick Forster (Gitter import) (Oct 23 2019 at 13:12):

Require Import String.
From MetaCoq Require Import Template.All.
Export MonadNotation.

Definition getName (x : nat -> nat) :=
  x <- tmEval cbv x;;
  t <- tmQuote x ;; match t with tLambda (nNamed na) _ _ => ret na | _ => ret "" end.


Notation name_of n := (ltac:(let k x := exact x in run_template_program (getName (fun n : nat => 0)) k)).

Compute (name_of n).
     (* = "n" *)
     (* : string *)

Matthieu Sozeau (Oct 23 2019 at 13:22):

Jason Gross (Oct 23 2019 at 18:28):

This seems like the same trick I use to pass identifiers from Ltac to OCaml in the plugin I wrote recently. Why do you need the cbv here?

Jason Gross (Oct 23 2019 at 18:42):

I'm also curious where you encountered it (and am trying to recall where I got it from ... I feel like after spending many hours struggling with bugs in fresh trying to write name-preserving reification to PHOAS, storing names in binders of dummy functions seemed like the obvious way to pass names between Ltac and Gallina?)

Jason Gross (Oct 23 2019 at 18:44):

Also, if you are interested in a confusing gotcha, I think if you replace cbv with vm_compute, your code will produce the wrong name in many cases.

Théo Winterhalter (Oct 23 2019 at 19:44):

This is just because vm_compute isn’t working directly with the coq ast and so the names aren’t preserved right?

Jason Gross (Oct 23 2019 at 19:45):

Yeah, the round-trip through vm_compute's representation doesn't preserve names

matrixbot (Gitter import) (Oct 24 2019 at 18:20):

Matthieu Sozeau (Oct 24 2019 at 20:16):

You need to use a translation from inductive bodies to inductive entries I guess

Matthieu Sozeau (Oct 24 2019 at 20:17):

Danil Annenkov (Oct 25 2019 at 11:33):

Hi @pedrotst , Quote Recursively returns a list of global definitions and a term. So, you should project the term first:

Make Definition list_from_syntax :=
  ltac:(let t := eval cbv in (snd list_syntax) in exact t).

Danil Annenkov (Oct 25 2019 at 11:34):

This does not give you a new inductive though. The result is a definition list_from_syntax = list : Type -> Type

Yannick Forster (Gitter import) (Oct 25 2019 at 12:26):

@Jason Gross I don't think I saw it somewhere explicitly. I was discussing notations using names as arguments in functions in relation to Coq issue #10894, and then it felt natural to do it this way

Jason Gross (Oct 31 2019 at 00:12):

Does metacoq have an implementation of autorewrite / rewrite_strat (or even just rewrite, but one that goes under binders)?

Gregory Malecha (Oct 31 2019 at 08:20):

Gregory Malecha (Oct 31 2019 at 08:21):

you could implement it, but it would require implementing some aggressive unification

Jason Gross (Oct 31 2019 at 20:31):

Gregory Malecha (Oct 31 2019 at 20:33):

it probably wouldn't be difficult to implement a very simple thing for what you want to do

Gregory Malecha (Oct 31 2019 at 20:33):

Gregory Malecha (Oct 31 2019 at 20:34):

most of the pieces are probably there, but you would have to put them together. that said, it would probably be very useful to the project overall

Jason Gross (Oct 31 2019 at 20:35):

I have a definition Let_In {A B} (f : A -> B) (x : A) := f x which is Opaque, and then I have a term like Let_In (x + x + 0) (fun y => Let_In (y + y +0) (fun z => Let_In (z + z + 0) (fun w => ...))), and I have the appropriate Proper lemma for Let_In, and I want to rewrite with the lemma that forall x, x + 0 = x in all the places. (I have other slightly more complicated examples, which involve interleaving cbn [nat_rect] with rewriting like this, but this is basically the extent of what I'm looking at.) How complicated would this be to have?

Gregory Malecha (Oct 31 2019 at 20:35):

Jason Gross (Oct 31 2019 at 20:36):

Gregory Malecha (Oct 31 2019 at 20:36):

Jason Gross (Oct 31 2019 at 20:36):

Jason Gross (Oct 31 2019 at 20:37):

Could you help me get this example working in MirrorCore (or MetaCoq) or whatever?

Gregory Malecha (Oct 31 2019 at 20:37):

as far as metacoq goes, i think you could make it work, what is the timeline that you have for this?

Gregory Malecha (Oct 31 2019 at 20:37):

Jason Gross (Oct 31 2019 at 20:38):

Suzanne Dupéron (Gitter import) (Feb 15 2020 at 23:31):

Hi :wave:. Just wondering, is there a way in MetaCoq to quote a term with holes ? I'd like to quote a term like @cons _ true _ and later programmatically fill in both _.

Kenji Maillard (Feb 16 2020 at 00:05):

Théo Winterhalter (Feb 16 2020 at 13:46):

@Kenji Maillard I think it’s a bit different because the question here is to quote terms with holes. In the case of @cons _ true _ I think, it will be hard to bypass unification, I don’t see how it won’t become bool.
For the other one, if you manage to quote it, it should come with a tEvar that you could replace with a function. The question is also at what level you want to do this @Suzanne Dupéron: inside a goal? or outside?

Théo Winterhalter (Feb 16 2020 at 13:47):

But yeah since we don’t really deal with evars I’m not sure it would work well.

Matthieu Sozeau (Mar 01 2020 at 23:14):

Kenji Maillard (Mar 02 2020 at 01:16):

Suzanne Dupéron (Gitter import) (Mar 02 2020 at 17:31):

@Théo Winterhalter I'm trying to use this to do metaprogramming, so that Definition foo := macro(some_gallina_here). can have macro rewrite and/or infer some _ as it wants. Using a Notation + ltac:(…) + uconstr(…) it's possible to do this to some extent with LTac, but ironically LTac's representation of terms is not very nice to manipulate. Good to know metacoq doesn't really deal with evars, this is knid of a showstopper :) ! Thanks!

Théo Winterhalter (Mar 02 2020 at 18:17):

I mean you can still inspect a term with evars and try to fill them, but I don’t think you will have access to the constraints set on the hole, I might be wrong though, I’m not an expert on evars.
In principle what you want to do should be possible, but it’s always a bit painful to fordib Coq to infer stuff.

Matthieu Sozeau (Mar 02 2020 at 18:20):

@Suzanne Dupéron indeed you can still quote "open" terms but you'll be on your own solving the evars if you want to send the term back to Coq.

Suzanne Dupéron (Gitter import) (Mar 02 2020 at 18:40):

Hm, interesting. I would hope to fill make some transformations and/or fill in in some relevant parts, then let the usual unification do its job. How would you quote an open term, though?

Matthieu Sozeau (Mar 02 2020 at 18:45):

All the quotation mechanisms allow "open_constr", e.g. you can call tmQuote from the template monad on an open term. If you tmPrint it you'll see tEvar constructors for the holes

Danil Annenkov (Mar 04 2020 at 14:55):

Hi guys, do you know where I can look at examples of how to use the certified erasure in the template monad (not as an extracted plugin)? It seems that erasure/tests-suite/Test.v is outdated.

Danil Annenkov (Mar 04 2020 at 15:56):

Danil Annenkov (Mar 04 2020 at 15:57):

Takes 1 min to compute and as a result I see some huge term with nested "match" and stuff :)

Yannick Forster (Gitter import) (Mar 04 2020 at 16:00):

Danil Annenkov (Mar 04 2020 at 16:12):

It seems I'm using an old version of MetaCoq distribution: 1.0~alpha+8.9. I'll try the 2.0-beta.

Yannick Forster (Gitter import) (Mar 04 2020 at 17:27):

I'm afraid for an actually working live erasure you'll either have to wait for the new alpha to be released in the next couple of days (then for 8.9, 8.10 and 8.11) or use the code from github

Danil Annenkov (Mar 04 2020 at 19:47):

I have another question: I want to implement a pretty printer to something OCaml-like form the erased AST. But terms contain redundant abstractions and application of boxes. Currently, I am interested only in prenex-polymorphic fragment, so, I guess it should not be too hard to strip away these redundant abstractions and box applications. One issue is that lambdas are not annotated with types anymore and I don't know where they type abstractions or "regular" lambdas.

Danil Annenkov (Mar 04 2020 at 19:47):

Matthieu Sozeau (Mar 05 2020 at 08:48):

It has not been done yet, but type abstraction lambdas bind variables that are not used in the body. I guess a better setup would be to mark binders for erasable types though during erasure

Danil Annenkov (Mar 05 2020 at 08:50):

Yes, marking of binders would be very helpful. Then it would be clear which abstractions to remove.

Danil Annenkov (Mar 05 2020 at 09:44):

Danil Annenkov (Mar 05 2020 at 09:45):

Matthieu Sozeau (Mar 13 2020 at 12:24):

Danil Annenkov (Mar 14 2020 at 18:56):

Basically, I annotate binders for lambda abstractions (lets can be annotated in the same way) with a boolean flag. The flag is true if the type of the binder reduces to arity (I use the same is_arity as in is_erasable). Is this right?

I adjusted the pretty-printing by adding print_term_deboxed function, which is almost the same as print_term but ignores abstractions marked as "dummy" and removes applications of boxes. It is easy to do it at the pretty-printing phase, but seems a bit hacky. Do you think it's worth implementing a "debox" function taking a term and removing dummy abstractions and boxes? It would be a bit more annoyng, because we have to adjust de Bruijn indices when removing abstractions. Especially annoing if the abstractions are mixed, e.g. something like this (fun (X : Set) (x : X -> unit) (Y : Set) (x0 : X) (Z : Type) => x x0).

Matthieu Sozeau (Mar 14 2020 at 19:23):

Cool. The is_arity test sounds right. I think doing deboxing/simplification should be done after erasure but will require some thinking. Eg removing boxes in constructor applications should involve a change in the corresponding inductive declaration

Yannick Forster (Gitter import) (Mar 14 2020 at 19:28):

I think there are thoughts on that in Pierre Letouzey's thesis. Removing type abstractions should be fine. Removing binders for proofs is fine in many cases, but there are examples (definitely in Pierre's thesis) where that introduces problems

Yannick Forster (Gitter import) (Mar 14 2020 at 19:28):

Deboxing also sounds interesting, I never thought of that (and I think neither did Pierre)

Danil Annenkov (Mar 14 2020 at 19:31):

Danil Annenkov (Mar 14 2020 at 19:32):

Matthieu Sozeau (Mar 15 2020 at 10:09):

Matthieu Sozeau (Mar 15 2020 at 10:10):

Danil Annenkov (Mar 15 2020 at 10:14):

Ah, I see. Could you point me at which intermidiate representation in CertiCoq this is done?

Danil Annenkov (Mar 15 2020 at 10:46):

Danil Annenkov (Mar 15 2020 at 21:01):

It seems the OCaml extraction does eta-expansion, at least eta_args_sign is used there.
What if all the constructors are applied to all type arguments? Would eta-expansion be still required? Just trying to understand why eta-expansion is necessary.

Danil Annenkov (Mar 17 2020 at 17:07):

I want to use the erasure plugin in my own plugin. How can I do that? I've tried to just extract the erasure function with all the dependencies and import it. But this requires basically to do the same steps as in the erasure building script (and even more, because it depends on pcuic and template-coq). Is there a better way?

Danil Annenkov (Mar 17 2020 at 17:09):

Matthieu Sozeau (Mar 17 2020 at 19:11):

Matthieu Sozeau (Mar 17 2020 at 19:12):

There’s no better way than doing your whole copy of eveything, extraction messes up name clash management which renders separate compilation very brittle

Matthieu Sozeau (Mar 17 2020 at 19:12):

Matthieu Sozeau (Mar 17 2020 at 19:13):

Matthieu Sozeau (Mar 17 2020 at 19:16):

I’m not so familiar with the phases of coq’s extraction, but for partial applications I don’t think you can just remove all parameters blindly

Danil Annenkov (Mar 17 2020 at 19:38):

Thanks for your answers! I'll try to reuse the setup for erasure to rebuild in in the folder with my development.

Danil Annenkov (Mar 17 2020 at 19:40):

Ok, that sounds reasonable. I'll do the naive version for now with a check that the constructors are fully applied.

Bas Spitters (Mar 18 2020 at 09:14):

Bas Spitters (Mar 18 2020 at 09:16):

Danil Annenkov (Mar 20 2020 at 17:57):

Danil Annenkov (Mar 20 2020 at 18:02):

I think I need to distinguish between different reasons for boxing terms. Something like kill_reason in the OCaml extraction. I want to remove only boxed coming from types and not for props, because I don't remove abstractions corresponding to proofs, since this might be bad. Would such a more informative box would be useful in general? I mean, I can add this stuff and make a pull request if it makes sense.

Matthieu Sozeau (Mar 20 2020 at 19:17):

Danil Annenkov (Mar 20 2020 at 19:20):

Bohdan Liesnikov (Mar 27 2020 at 15:55):

Hi everyone!
I'm currently looking for a lemma that would assert existence of a type of type, something along the lines of Sigma ;;; Gamma |- t : T -> exists s, Sigma ;;; Gamma |- T : tSort s.
But Sigma above can't stay the same since in some cases we have to declare a new universe.

I looked for it in the repo, but couldn't find anything resembling this. Did I miss it or is it indeed currently not there?
And if not, what do you think would be the best way to state it/prove it?

Théo Winterhalter (Mar 27 2020 at 15:56):

Théo Winterhalter (Mar 27 2020 at 15:57):

Théo Winterhalter (Mar 27 2020 at 15:58):

It’s in PCUIC and not in TemplateCoq where there isn’t much of the meta-theory done.

Théo Winterhalter (Mar 27 2020 at 15:59):

Bohdan Liesnikov (Mar 27 2020 at 16:09):

Thanks! I talked with Yannick about this before and he aslo pointed me in direction of that lemma.
However, what I don't quite get is if arities are iterated products\letins, wouldn't it be possible to assign a type (sort) to a valid arity?

Théo Winterhalter (Mar 27 2020 at 16:10):

Unfortunately no, there are so-called algebraic universes (like max(i,j), i+1) that can only appear on the right-hand side of the colon.

Bohdan Liesnikov (Mar 27 2020 at 16:18):

Yep, but then couldn't you declare a new universe with a constraint that it's strictly bigger than whatever algebraic universe appears on the right-hand side?
A side question would be where can I read up on that? I saw "Type checking with universes" by Harper and Pollack, but maybe there is more recent work?

Théo Winterhalter (Mar 27 2020 at 16:18):

Théo Winterhalter (Mar 27 2020 at 16:19):

Bohdan Liesnikov (Mar 27 2020 at 16:20):

Théo Winterhalter (Mar 27 2020 at 16:21):

I’m sorry I can’t really explain this point because I’m not an expert, I’d rather have @Matthieu Sozeau do it.

Karl Palmskog (Mar 28 2020 at 15:14):

so one thing I'd have liked at various point in verified program development using sigma-types is the ability to remove Props automatically inside Coq from various functions

Karl Palmskog (Mar 28 2020 at 15:15):

is there a way to accomplish something like this using MetaCoq, or what needs to be done first?

Théo Winterhalter (Mar 28 2020 at 15:38):

Théo Winterhalter (Mar 28 2020 at 15:39):

Would you like to replace all proofs of propositions with opaque constants, like abstract would do?

Karl Palmskog (Mar 28 2020 at 15:40):

basically, I want to go from a function: nat -> { a : A | P a } to a function nat -> A

Karl Palmskog (Mar 28 2020 at 15:40):

Théo Winterhalter (Mar 28 2020 at 15:41):

I mean you would have to work out the translation but I expect it could be done with metacoq.

Karl Palmskog (Mar 28 2020 at 15:41):

Karl Palmskog (Mar 28 2020 at 15:42):

Karl Palmskog (Mar 28 2020 at 15:43):

Matthieu Sozeau (Mar 28 2020 at 15:43):

@B. L. The problem is we don't know how to do type inference efficiently if we allow arbitrary max(i, j) <= max(k, l) constraints, hence we restrict the type system so that only max(i,j) <= k constraints can be generated. In practice it means Type@{max(i,j)} does not have a type, but indeed a different version of the system where the typing rule of Type becomes : i < j |- Type@{i} < Type@{j} would allow to get rid of the special case for arities.

Matthieu Sozeau (Mar 28 2020 at 15:43):

Hugo Herbelin has a not about algebraic universes where this is explained (it appeared at TYPES IIRC)

Matthieu Sozeau (Mar 28 2020 at 15:46):

@Karl Palmskog If what you want is to allow during a proof script execution to solve a conversion [A = B] using (erase(A) = erase(B)) for A, B : nat then MetaCoq + CertiCoq ought to provide that.

Matthieu Sozeau (Mar 28 2020 at 15:47):

Matthieu Sozeau (Mar 28 2020 at 15:49):

@B. L. about such a lemma, indeed I think it is provable, with an extended Sigma, using validity. What you want to prove is that isWfArity_or_Type Sigma Gamma T -> exists s, Sigma + s and a constraint ;;; Gamma |- T : tSort s basically.

Karl Palmskog (Mar 28 2020 at 15:50):

@Matthieu Sozeau you mean they (metacoq + certicoq) provide this right now? yeah basically I want to develop using sigma types, but then get "regular" functions with some companion lemma

Matthieu Sozeau (Mar 30 2020 at 10:41):

Not yet, we’ll need a way to extend the conversion algorithms in the kernel so we can call the certicoq based evaluator first, or find a way around that

Bohdan Liesnikov (Mar 30 2020 at 12:14):

Bohdan Liesnikov (Mar 30 2020 at 12:22):

Matthieu Sozeau (Apr 01 2020 at 13:06):

Danil Annenkov (Apr 07 2020 at 13:29):

I am reading Pierre Letouzey's thesis. He discusses simplifications such as removing abstractions and boxes in Chapter 4.3. It's safe to remove boxes for fully applied constants and constructors. The tricky part comes when constants and constructors are partially applied (but for global definitions all dummy abstractions are removed and only the application sides are adjusted). Interestingly, boxes coming from propositions and type schemes are treated in the same way. I understand why removing all abstractions for propositions might be a problem (seems like False_rect and Acc, mainly), but why it is not safe to remove all abstractions corresponding to type schemes, I don't understand. Maybe you have some ideas @Yannick Forster ?

Matthieu Sozeau (Apr 09 2020 at 14:36):

@Danil Annenkov It is curious if we cannot remove all type abstractions. It would seem to go against parametricity

Danil Annenkov (Apr 09 2020 at 14:41):

Yes, it should be possible. I'm wondering why this is not mentioned as a possibility for optimisation. I found the following footnote in Pierre's thesis "In fact, these residues can also come from type schemes and not only from logical parts, but we will merge here these two situations by simply speaking of "residues"."

Danil Annenkov (Apr 09 2020 at 14:43):

Definition p_ex1 (A : Type) (a : A) (B : Type) (C : Type):= a.

Definition p_ex2 :=
  let f := p_ex1 nat 0 in
  (fun _ : unit => f nat bool).

Extraction p_ex2.

Danil Annenkov (Apr 09 2020 at 14:43):

let p_ex2 =
  let f = fun _ _ -> p_ex1 O in (fun _ -> f __ __)

Danil Annenkov (Apr 09 2020 at 14:45):

Matthieu Sozeau (Apr 09 2020 at 15:22):

Danil Annenkov (Apr 09 2020 at 15:24):

I think it's for partial applications, because for fully applied p_ext1 it extracts to

let p_ex2 =
  let f = p_ex1 O in (fun _ -> f)

Danil Annenkov (Apr 09 2020 at 15:25):

It behaves the same way for partial application of types as for partial applications of logical arguments.

Cyril Cohen (Apr 15 2020 at 14:08):

Hi, I am in the process of exporting gitter channels (public) data to zulip, (it can be done only once, during the creation of the zulip chatroom), do you wish that I export the data of this channel too?

Matthieu Sozeau (Apr 15 2020 at 14:08):

matrixbot (Gitter import) (Apr 16 2020 at 15:34):

Danil Annenkov (Apr 16 2020 at 15:39):

@pedrotst I think, it depends why it fails. I don't know the best way, but first, I look at the template Coq AST, if it's not too big.

Danil Annenkov (Apr 16 2020 at 15:40):

matrixbot (Gitter import) (Apr 16 2020 at 15:42):

pedroabreu inspect_term: cannot recognize (huge term) (maybe you forgot to reduce it?)

matrixbot (Gitter import) (Apr 16 2020 at 15:43):

pedroabreu basically what I'm trying to do is quote and unquote the lemma and_cancel_l, It seems to me that it is not quoting quite correctly

matrixbot (Gitter import) (Apr 16 2020 at 15:43):

matrixbot (Gitter import) (Apr 16 2020 at 15:45):

pedroabreu * basically what I'm trying to do is quote and unquote the lemma and_cancel_l, basically it is not being quoted as I expected

Danil Annenkov (Apr 16 2020 at 18:31):

Could you please tell me how you quote and_cancel_l? Using Quote Definition?

Quote Definition z := (and_cancel_l).
Make Definition zzz := z.
Print zzz.
(* zzz =
and_cancel_l
     : forall A B C : Prop,
       (B -> A) -> (C -> A) -> (A /\ B <-> A /\ C) <-> (B <-> C)
*)

Danil Annenkov (Apr 16 2020 at 18:33):

This seems to work fine, but Quote Definition z := (and_cancel_l). just quotes it as a constant.
It's hard to do better, I guess, because and_cancel_l is opaque.

Danil Annenkov (Apr 16 2020 at 18:35):

If you use Quote Recursively Definition z := (and_cancel_l). Then you need to take a second projection to unquote. Because the first component is global environment with all the definitions that and_cancel_l depends on.

Danil Annenkov (Apr 16 2020 at 19:27):

The body of the and_cancel_l is accessible in the global environment (when you do Quote Recursively).
You can print it like this:

Compute lookup_env z.1 "Coq.Init.Logic.and_cancel_l".

matrixbot (Gitter import) (Apr 17 2020 at 03:38):

pedroabreu Yeah, I was getting the term with Quote Recursively I didn't know about the lookup_env function, so I was walking through the list until the position I wanted.

matrixbot (Gitter import) (Apr 17 2020 at 03:40):

pedroabreu But anyways, I upgraded the version of Metacoq to see if I see the same behaviour and apparently I cannot get Unquote to work. The demo files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

matrixbot (Gitter import) (Apr 17 2020 at 03:40):

matrixbot (Gitter import) (Apr 17 2020 at 03:41):

pedroabreu * But anyways, I upgraded the version of Metacoq to see if I see the same behaviour and apparently I cannot get Unquote to work. The demo.v files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

matrixbot (Gitter import) (Apr 17 2020 at 03:41):

pedroabreu * But anyways, I upgraded the version of Metacoq to 8.11 to see if I see the same behaviour and apparently I cannot get Unquote to work. The demo.v files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

matrixbot (Gitter import) (Apr 17 2020 at 03:41):

pedroabreu * But anyways, I upgraded the version of Metacoq to 8.11 to see if I get the same behaviour and apparently I cannot get Unquote to work. The demo.v files says I should do Metacoq Unquote Definition bar := foo, but I get Error: Syntax error: illegal begin of toplevel:vernac_toplevel.

Danil Annenkov (Apr 17 2020 at 08:07):

I use MetaCoq for Coq 8.11 from opam before the last update of the vernacular syntax. Maybe the problem is not in the MetaCoq version, but what you are trying to unquote? The global environment contains global declarations, not terms. You need to unwrap them before you unquote. The following code works in my installation (for Coq 8.11):

Definition lookup_const (g : global_env) (cst : ident) :=
  match (lookup_env g "Coq.Init.Logic.and_cancel_l") with
  | Some (ConstantDecl d) =>
    match d.(cst_body) with
    | Some b => b
    | None => tVar "decl without a body"
    end
  | Some _ => tVar "not a constant"
  | None => tVar "decl not found"
  end.

Quote Recursively Definition z := (and_cancel_l).
Make Definition zzz := (lookup_const z.1 "Coq.Init.Logic.and_cancel_l").

Danil Annenkov (Apr 17 2020 at 08:09):

lookup_const uses lookup_env and unwraps global_decl into a term, if possible. Otherwise returns a dummy tVar.

Danil Annenkov (Apr 17 2020 at 08:11):

Danil Annenkov (Apr 17 2020 at 12:35):

If you use TemplateMonad then you can use tmQuoteConstant to quote a constant directly. Passing true as a second argument would allow to get bodies for opaque definitions.

matrixbot (Gitter import) (Apr 17 2020 at 13:08):

pedroabreu awesome, Make Definition was the syntax I was missing, thanks! Everything is working as expected now thanks for you time Danil Annenkov (Gitter)

Danil Annenkov (Apr 17 2020 at 13:09):

matrixbot (Gitter import) (Apr 17 2020 at 14:04):

matrixbot (Gitter import) (Apr 17 2020 at 14:05):

pedroabreu I was assuming that we shouldn't reference unnamed variables (which in hindsight is not a fair assumption). Which means the following should work
```Definition nat_id_syntax :=
tLambda nAnon
(tInd
{|
inductive_mind := "Coq.Init.Datatypes.nat";
inductive_ind := 0 |} []) (tRel 0).
Make Definition unquote_nat_id := nat_id_syntax.

matrixbot (Gitter import) (Apr 17 2020 at 14:06):

pedroabreu So I guess my question is how does coq/metacoq deal with naming unnamed variables like this?

Théo Winterhalter (Apr 17 2020 at 14:07):

You should see names as printing hints, nothing more.
It’s true that we often write _ in a binder (on paper) to mean that the variable isn’t used, but here it just means that it’s up to Coq to figure out how to name it.

Danil Annenkov (Apr 24 2020 at 12:52):

Hej guys, is there any way for quoting recursively but not fetching bodies of opaque definitions? Otherwise, any definition involving a proof from the standard library will quote half of the standard library :) Some times I it just takes forever, so I had to terminate the process. We hit this problem before when working on the forcing translation. Loïc had to reimplement proof about natural numbers, otherwise, it took too long to quote dependencies.

Matthieu Sozeau (Apr 25 2020 at 10:45):

You could try to program it using the non-recursive quoting I guess, turning opaque proofs into axioms in the reified environment ?

Danil Annenkov (Apr 25 2020 at 10:48):

tmQuoteConstant actually takes a flag whether it should bypass opacity or not. I'll try to use this one. But then the problem is that I'll have to manage dependencies manually.

Danil Annenkov (Apr 30 2020 at 15:16):

@Matthieu Sozeau there are two versions of the erasure function: one in SafeErasureFunction.v and one in ErasureFunction.v. As far as I understand, the difference is that the first one takes a well-typed term. How this typing information is used during erasure? The extracted plugin is based on the safe version, if I understand correctly. What would be the downsides of using the version from ErasureFunction.v for the plugin?

Théo Winterhalter (Apr 30 2020 at 16:45):

Théo Winterhalter (Apr 30 2020 at 16:46):

The Safe one is the proven correct modulo normalisation. But it should extract more or less to the desired implementation.

Danil Annenkov (Apr 30 2020 at 18:50):

Hi @Théo Winterhalter, thank for you answer!
I've checked erase from ErasureFunction.v:

erase :
forall Σ : global_env_ext,
∥ wf_ext Σ ∥ ->
forall Γ : context, ∥ wf_local Σ Γ ∥ -> term -> typing_result E.term

Danil Annenkov (Apr 30 2020 at 18:50):

Danil Annenkov (Apr 30 2020 at 18:51):

Danil Annenkov (Apr 30 2020 at 18:55):

In the "safe" version is_erasable calls type_of and in the other one it calls make_graph_and_infer

Danil Annenkov (Apr 30 2020 at 18:57):

And is_erasable from ErasureFunction.v returns also welltyped Sigma Gamma t if the term is not erasable (and the call to is_erasable succeeds).

Théo Winterhalter (Apr 30 2020 at 19:16):

I see. I mean, it would be better for @Yannick Forster or @Matthieu Sozeau to answer here because I didn’t work on erasure at all.

Gregory Malecha (May 01 2020 at 01:25):

I was toying with some performance tuning today and built a simple bytestring library. would people be interested in using that instead of ascii for storing strings?

Danil Annenkov (May 04 2020 at 15:56):

@Gregory Malecha we use strings in Coq for pretty-printing a lot. So far they were not the bottleneck, but it would be interesting to try bytestrings instead.

Gregory Malecha (May 04 2020 at 15:57):

i recall there being something a bit annoying when you tried to quote a quoted term @Jason Gross brought this up a long time ago, not sure if he's still interested in it

Matthieu Sozeau (May 05 2020 at 11:12):

@Danil Annenkov the main difference is in the use of retyping which is less costly than typing IIRC.

Matthieu Sozeau (May 05 2020 at 11:13):

Danil Annenkov (May 05 2020 at 12:46):

@Matthieu Sozeau by retyping you mean type_of? What is the difference with make_graph_and_infer?

Jason Gross (May 06 2020 at 01:52):

I'm not actively working on anything around it currently, but I am still at least vaguely interested. It came up when trying to formalize Lob's theorem in Coq using Template Coq / MetaCoq, because there are a bunch of places where you need a doubly-quoted thing. (For example, one of the things needed is a Gallina function from AST -> (quote AST), and then I also need a quoted version of this function, I believe.)

Jason Gross (May 06 2020 at 01:54):

And regarding bytestrings, I'm assuming you mean using https://github.com/coq/coq/blob/master/theories/Init/Byte.v and making a list of them. Note that if you make a custom inductive type that is a list of these, much like string is a specialized list of ascii, you can have them pretty-printed as strings automatically. (Allowing this with list byte and list ascii is still a work in progress on string notations, but should hopefully be coming in the next couple of Coq versions)

Gregory Malecha (May 06 2020 at 01:56):

Gregory Malecha (May 06 2020 at 01:57):

i think that i might implement C-style escapes for it though so that "\n" parses to (String x13 EmptyString)

Gregory Malecha (May 06 2020 at 01:59):

specializing the inductive achieves two things: 1/ it is a drop-in replacement for string in more cases; 2/ it avoids the extra Byte.byte parameter to every cons

Stream: MetaCoq

Topic: imported from gitter room coq/metacoq

Gregory Malecha (Sep 26 2019 at 02:47):

Matthieu Sozeau (Sep 26 2019 at 09:10):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:11):

Matthieu Sozeau (Sep 26 2019 at 09:18):

Matthieu Sozeau (Sep 26 2019 at 09:18):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:18):

Matthieu Sozeau (Sep 26 2019 at 09:19):

Matthieu Sozeau (Sep 26 2019 at 09:19):

Matthieu Sozeau (Sep 26 2019 at 09:19):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:22):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:22):

Matthieu Sozeau (Sep 26 2019 at 09:23):

Yannick Forster (Gitter import) (Sep 26 2019 at 09:24):

Gregory Malecha (Sep 26 2019 at 11:11):

Gregory Malecha (Sep 26 2019 at 12:21):

Yannick Forster (Gitter import) (Sep 26 2019 at 12:23):

Yannick Forster (Gitter import) (Sep 26 2019 at 12:23):

Gregory Malecha (Sep 26 2019 at 12:31):

Yannick Forster (Gitter import) (Sep 26 2019 at 12:33):

Matthieu Sozeau (Sep 26 2019 at 13:33):

Théo Winterhalter (Sep 26 2019 at 13:33):

Gregory Malecha (Sep 26 2019 at 13:36):

Gregory Malecha (Sep 26 2019 at 13:36):

Yannick Forster (Gitter import) (Sep 26 2019 at 13:37):

Gregory Malecha (Sep 26 2019 at 13:37):

Gregory Malecha (Sep 26 2019 at 13:38):

Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

Yannick Forster (Gitter import) (Sep 26 2019 at 13:39):

Gregory Malecha (Sep 26 2019 at 13:40):

Gregory Malecha (Sep 26 2019 at 13:40):

Gregory Malecha (Sep 26 2019 at 13:41):

Gregory Malecha (Sep 26 2019 at 13:41):

Gregory Malecha (Sep 26 2019 at 13:42):

Matthieu Sozeau (Sep 26 2019 at 14:12):

Matthieu Sozeau (Sep 26 2019 at 14:12):

Gregory Malecha (Sep 26 2019 at 14:13):

Matthieu Sozeau (Sep 26 2019 at 14:13):

Matthieu Sozeau (Sep 26 2019 at 14:13):

Matthieu Sozeau (Sep 26 2019 at 14:13):

Gregory Malecha (Sep 26 2019 at 14:13):

Gregory Malecha (Sep 26 2019 at 14:13):

Matthieu Sozeau (Sep 26 2019 at 14:14):

Gregory Malecha (Sep 26 2019 at 14:14):

Gregory Malecha (Sep 26 2019 at 14:14):

Matthieu Sozeau (Sep 26 2019 at 14:15):

Gregory Malecha (Sep 26 2019 at 14:15):

Matthieu Sozeau (Sep 26 2019 at 14:15):

Gregory Malecha (Sep 26 2019 at 17:23):

Gregory Malecha (Sep 26 2019 at 17:24):

Gregory Malecha (Sep 26 2019 at 17:24):

Gregory Malecha (Sep 26 2019 at 17:55):

Gregory Malecha (Sep 26 2019 at 17:55):

Gregory Malecha (Sep 26 2019 at 17:57):

Gregory Malecha (Sep 26 2019 at 17:57):

Gregory Malecha (Sep 26 2019 at 17:58):

Matthieu Sozeau (Sep 27 2019 at 09:07):

Matthieu Sozeau (Sep 27 2019 at 10:32):

Matthieu Sozeau (Sep 27 2019 at 10:32):

Yannick Forster (Gitter import) (Sep 27 2019 at 10:33):

Théo Winterhalter (Sep 27 2019 at 11:17):

Matthieu Sozeau (Sep 27 2019 at 11:17):

Théo Winterhalter (Sep 27 2019 at 11:18):

Matthieu Sozeau (Sep 27 2019 at 11:19):

Théo Winterhalter (Sep 27 2019 at 11:19):

Matthieu Sozeau (Sep 27 2019 at 11:19):

Yannick Forster (Gitter import) (Sep 27 2019 at 11:56):

Matthieu Sozeau (Sep 27 2019 at 12:04):

Matthieu Sozeau (Sep 27 2019 at 12:05):

Matthieu Sozeau (Sep 27 2019 at 12:24):

Matthieu Sozeau (Sep 27 2019 at 12:25):

Gregory Malecha (Sep 27 2019 at 12:29):

Matthieu Sozeau (Sep 27 2019 at 13:13):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:16):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:17):

Matthieu Sozeau (Sep 27 2019 at 13:22):

Yannick Forster (Gitter import) (Sep 27 2019 at 13:27):

Matthieu Sozeau (Sep 27 2019 at 13:30):