Matthieu Sozeau (Nov 30 2020 at 09:55): 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.
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
Yannick Forster (Nov 30 2020 at 09:59):And in particular, we can potentially use their plugins to test subprojects / CI
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.
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
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?
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
Matthieu Sozeau (Nov 30 2020 at 10:10):Interesting, we should have one of them join the discussion too.
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.
Matthieu Sozeau (Nov 30 2020 at 10:14):Sure, that's possible too
Pierre Vial (Dec 01 2020 at 14:34):Yes, actually, pretty much anytime thursday or friday would work for me actually
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.
Zoe Paraskevopoulou (Dec 01 2020 at 16:19):@Yannick Forster @Matthieu Sozeau What are the MetaCoq plans for primitive object support?
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"?
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.
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.
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 :/
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.
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.
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 ?
Jakob Botsch Nielsen (Dec 03 2020 at 11:48):Works for me
Yannick Forster (Dec 03 2020 at 12:24):Works for me! @Marcel Ullrich and @Lennard Gäher might be interested to join as well
Théo Winterhalter (Dec 03 2020 at 12:31):Yeah I can try to join
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.
Meven Lennon-Bertrand (Dec 03 2020 at 12:59):Shall I join as well?
Matthieu Sozeau (Dec 03 2020 at 12:59):Sure !
Matthieu Sozeau (Dec 03 2020 at 13:02):Breakout room 1
Théo Winterhalter (Dec 03 2020 at 13:06):It's still at 2:30 though right?
Matthieu Sozeau (Dec 03 2020 at 13:06):Yes, right :)
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
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
Jakob Botsch Nielsen (Dec 03 2020 at 13:23):@Danil Annenkov might want to join too :)
Danil Annenkov (Dec 03 2020 at 13:26):Yes, I am in :)
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!
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: Jun 11 2023 at 00:30 UTC