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.
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
And in particular, we can potentially use their plugins to test subprojects / CI
Subprojects organisation is one direction of discussion, another one would be about higher-level interfaces to the object defined in Metacoq.
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
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?
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
Interesting, we should have one of them join the discussion too.
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.
Sure, that's possible too
Yes, actually, pretty much anytime thursday or friday would work for me actually
Let's try thursday then, maybe Yannick can gather a few students working on plugins as well.
@Yannick Forster @Matthieu Sozeau What are the MetaCoq plans for primitive object support?
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"?
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.
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.
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 :/
This was recently discussed in the context of our work on certified extraction/compilation with @Jakob Botsch Nielsen and @Danil Annenkov
I don't have the link now. Maybe we should create an issue to document the discussion.
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.
Shall we have a MetaCoq WG around 2.30pm? @Yannick Forster @Théo Winterhalter @Jakob Botsch Nielsen @Kenji Maillard @Pierre Vial @Enzo Crance ?
Works for me
Works for me! @Marcel Ullrich and @Lennard Gäher might be interested to join as well
Yeah I can try to join
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.
Shall I join as well?
Breakout room 1
It's still at 2:30 though right?
Yes, right :)
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
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
@Danil Annenkov might want to join too :)
Yes, I am in :)
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!
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