Stream: CUDW 2020

Topic: WG: MetaCoq


view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 09:55):

To discuss MetaCoq-related projects? @Pierre Vial @Kenji Maillard I'm not sure we really have a specific point to discuss yet though. @Yannick Forster mentions that we need to have a proper story for subprojects. I'm thinking this could be related to how coq-community handles projects with dependencies.

view this post on Zulip Yannick Forster (Nov 30 2020 at 09:58):

Happy to discuss things whenever they come up, but I currently don't have a MetaCoq-project to work on. I'll ping @Christian Hagemeier @Marcel Ullrich @Daniel Spaniol @Lennard Gäher @Johannes Hostert @Fabian Fries and @Fabian Kunze since they are all working on or around MetaCoq plugings atm

view this post on Zulip Yannick Forster (Nov 30 2020 at 09:59):

And in particular, we can potentially use their plugins to test subprojects / CI

view this post on Zulip Kenji Maillard (Nov 30 2020 at 09:59):

Subprojects organisation is one direction of discussion, another one would be about higher-level interfaces to the object defined in Metacoq.

view this post on Zulip Yannick Forster (Nov 30 2020 at 10:01):

Good point Kenji! It's really annoying at the moment for instance to insert a match in a term, because you have to assemble the different parts manually. So smarter constructors that infer the inferable parts of a match for instance would be great

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 10:07):

That's a good point too, the higher-level interfaces. We could discuss the idea of trying out a PHOAS version as well. Let's wait for more input from MetaCoq users to see what emerges though?

view this post on Zulip Yannick Forster (Nov 30 2020 at 10:08):

Andrew told me some of his students (John and Joomy if I remember correctly) have a version of the AST with names that works well for them

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 10:10):

Interesting, we should have one of them join the discussion too.

view this post on Zulip Kenji Maillard (Nov 30 2020 at 10:11):

I was thinking of less ambitious possibilities as well. For instance I'm sure that a lot of inductive definitions fall in a much simpler class ("plain parametrized datatypes") than what Coq allows in full generality, and it would probably be useful to have a simpler representation for those together with functions doing the back and forth translation to Coq's full fledge inductive types.

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 10:14):

Sure, that's possible too

view this post on Zulip Pierre Vial (Dec 01 2020 at 14:34):

Yes, actually, pretty much anytime thursday or friday would work for me actually

view this post on Zulip Matthieu Sozeau (Dec 01 2020 at 15:42):

Let's try thursday then, maybe Yannick can gather a few students working on plugins as well.

view this post on Zulip Zoe Paraskevopoulou (Dec 01 2020 at 16:19):

@Yannick Forster @Matthieu Sozeau What are the MetaCoq plans for primitive object support?

view this post on Zulip Fabian Kunze (Dec 01 2020 at 19:52):

@Zoe Paraskevopoulou
Do you mean "use primitive objects in the implementation of the AST for faster AST transformation and TemplateCoq-programs" or "handle primitive objects in the metatheory described in metacoq"?

view this post on Zulip Fabian Kunze (Dec 01 2020 at 19:52):

I'm currently supervising a student who implements strings for TemplateCoq as primitive arrays of primitive integers, but I get the feeling that you were asking for the other interpretation.

view this post on Zulip Zoe Paraskevopoulou (Dec 01 2020 at 23:30):

Hi @Fabian Kunze, I mean supporting reification of primitive objects to PCUIC and erasure to λbox (my understanding is that this is currently not supported). I'd like to add support for compilation of primitive integers/floats in CertiCoq, and we’d need MetaCoq support for that.

view this post on Zulip Yannick Forster (Dec 02 2020 at 08:26):

As far as I know, nobody is working on representing primitive integers and floats in MetaCoq. Very likely, implementing them would not be too hard though. I think we're very open for people contributing a representation, but at least I myself don't have time for it atm :/

view this post on Zulip Bas Spitters (Dec 02 2020 at 10:45):

This was recently discussed in the context of our work on certified extraction/compilation with @Jakob Botsch Nielsen and @Danil Annenkov
https://www.cs.au.dk/~spitters/Concert2.pdf
I don't have the link now. Maybe we should create an issue to document the discussion.

view this post on Zulip Zoe Paraskevopoulou (Dec 02 2020 at 17:28):

I created an issue on github. I think that once MetaCoq supports primitive objects it wouldn't be hard to support them in CertiCoq too. More interestingly, one could verify the implementation of primitive objects in a target program logic.

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 11:44):

Shall we have a MetaCoq WG around 2.30pm? @Yannick Forster @Théo Winterhalter @Jakob Botsch Nielsen @Kenji Maillard @Pierre Vial @Enzo Crance ?

view this post on Zulip Jakob Botsch Nielsen (Dec 03 2020 at 11:48):

Works for me

view this post on Zulip Yannick Forster (Dec 03 2020 at 12:24):

Works for me! @Marcel Ullrich and @Lennard Gäher might be interested to join as well

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 12:31):

Yeah I can try to join

view this post on Zulip Fabian Kunze (Dec 03 2020 at 12:48):

I would also be interested, as there is some desire to add holes/_ to the TemplateCoq AST, for example to not have to give the type for every constructor when constructing lists.

view this post on Zulip Meven Lennon-Bertrand (Dec 03 2020 at 12:59):

Shall I join as well?

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 12:59):

Sure !

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 13:02):

Breakout room 1

view this post on Zulip Théo Winterhalter (Dec 03 2020 at 13:06):

It's still at 2:30 though right?

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 13:06):

Yes, right :)

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 13:07):

In the meantime we can populate the wiki page at https://github.com/coq/coq/wiki/BreakOut-2020-12-03-MetaCoq with topics for discussion

view this post on Zulip Yannick Forster (Dec 03 2020 at 13:22):

For the people who haven't joined a session yet, here's the link to the rooms: https://bbb-front.math.univ-paris-diderot.fr/recherche/the-sev-dee-jmp

view this post on Zulip Jakob Botsch Nielsen (Dec 03 2020 at 13:23):

@Danil Annenkov might want to join too :)

view this post on Zulip Danil Annenkov (Dec 03 2020 at 13:26):

Yes, I am in :)

view this post on Zulip Matthieu Sozeau (Dec 03 2020 at 21:29):

Following this afternoons discussion, I made https://github.com/MetaCoq/metacoq/pull/530 which allows to denote evars in addition to their quoting, and in particular allows to provide partial terms whose holes can be filled by Typing later on. It was relatively easy as I know the APIs :) Enjoy!

view this post on Zulip Matthieu Sozeau (Dec 04 2020 at 15:28):

We've also started with Fabian trying to integrate primitive floats and integers. Quoting and unquoting should work now, I'm in the process of adapting PCUIC (using models of both).


Last updated: Oct 16 2021 at 09:07 UTC