Jason Gross (Mar 02 2023 at 06:24): Jason Gross (Mar 02 2023 at 06:24):I have 13 PRs open and waiting for review at https://github.com/MetaCoq/metacoq/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-desc+author%3AJasonGross+-is%3Adraft, at least some of which are pretty trivial and straightforward. Any chance I could get at least some of them reviewed / merged soon?
Matthieu Sozeau (Mar 02 2023 at 07:06):I’ll try to have a look today
Jason Gross (Mar 19 2023 at 03:12):Any updates?
Matthieu Sozeau (Mar 20 2023 at 11:43):Not yet, thanks for the reminder though, I’ll try to do a review tonight or tomorrow morning, it’s now at the top of my todo list
Jason Gross (Mar 21 2023 at 14:01):Thank you for going through all the PRs!
Jason Gross (Mar 23 2023 at 16:05):I think https://github.com/MetaCoq/metacoq/pull/863 is ready for merge
Jason Gross (Apr 03 2023 at 07:05):The following PRs are ready for review: #844 (adjust opam deps), #879 (rudimentary template monad debugging), #880 and #881 and #883 and #887 (minor changes needed by Gallina quotation), #838 (decidability for consistent_extension_on), #890 and #885 (minor nix changes of questionable utility), #892 (a target to update template-coq/_PluginProject.in when requested), #876 (a questionable implementation of tmTry)
#882 (add UniverseMap, UniverseMapFact) depends on #892 but is otherwise ready for review.
I've also created a draft PR for Gallina quotation, most of which is finished: #894
Matthieu Sozeau (Apr 03 2023 at 10:11):@Meven Lennon-Bertrand @Théo Winterhalter @Yannick Forster @nicolas tabareau do not hesitate to review and merge Jason's PRs, I have low bandwidth :)
Yannick Forster (Apr 03 2023 at 10:11):Ok
Théo Winterhalter (Apr 03 2023 at 11:16):I feel that I'm not knowledgable enough on the relevant bits to do it.
nicolas tabareau (Apr 03 2023 at 14:44):Ok, I am on it
Meven Lennon-Bertrand (Apr 03 2023 at 14:52):Same as Théo, I'd be happy to review PRs on the theory side, but I feel like I know nothing on the plugin side…
Jason Gross (Apr 03 2023 at 15:14):Thank you @nicolas tabareau (and everyone else for the counterfactual review offers)! I hope to have the quotation PR ready for review by later today or tomorrow (and I guess this one is more on the theory side than the plugin side?, though the theory is very shallow and the PR is heavy on TemplateMonad automation)
Jason Gross (Apr 07 2023 at 16:41):Could I trouble @nicolas tabareau (or anyone else) to review and merge #907 and #908 (minor performance improvements to quotation)? Once these are merged, I can rebase #898 and #909, and I expect these to be the end (or nearly the end) of the PRs about quotation to Ast.term. (I may or may not take a stab at PCUIC quotation and/or proving typing for the quotation functions, but this is all I have queued up currently.)
nicolas tabareau (Apr 08 2023 at 16:51):done
Jason Gross (Apr 08 2023 at 23:20):Thank you! #898, #909, #910, #912, and #914 are all ready for merge (and all relatively short)
Jason Gross (Apr 09 2023 at 05:40):And #915, #917, #918, #919, #920, #921, #923 too. (And hopefully #922, #924, #925, and #926 will pass CI soon)
Jason Gross (Apr 09 2023 at 05:42):(I decided to see how hard it would be to get Gallina quotation for PCUIC. It's a bit anonying, but not too bad, except for the fact that it's probably going to be way too slow to be viable because I can't figure out how to work around reduction in the template monad being slow.)
nicolas tabareau (Apr 09 2023 at 08:22):done
nicolas tabareau (Apr 09 2023 at 08:50):the CI fails on startup now
Jason Gross (Apr 10 2023 at 00:48):Thank you!
Jason Gross (Apr 10 2023 at 00:48):Any idea what's going on with the CI failure on startup?
Jason Gross (Apr 10 2023 at 00:50):I guess it's been starting with the merge of the PR that changed the CI, so maybe let's see what happens if we revert that?
Jason Gross (Apr 10 2023 at 00:51):I made a PR reverting it at https://github.com/MetaCoq/metacoq/pull/929, and it seems to maybe fix the problem? (At least some of its CI is running)
Jason Gross (Apr 10 2023 at 00:52):Maybe it doesn't like env.RUNNER_OS???
Jason Gross (Apr 10 2023 at 03:36):I've asked about it at https://github.com/orgs/community/discussions/52417. In the meantime, maybe we should merge https://github.com/MetaCoq/metacoq/pull/929, which seems to fix the problem?
Jason Gross (Apr 11 2023 at 03:07):Could someone merge #929 to fix the CI?
Yannick Forster (Apr 11 2023 at 03:09):Done!
Jason Gross (Apr 11 2023 at 03:22):Thank you!
Jason Gross (Apr 11 2023 at 06:12):PRs #927 and #928 are ready for review. I hope #930, #931, #932, and #934 will pass CI. Once #930 and #932 are merged, I can rebase #933 (better induction scheme for cumul0Spec).
Jason Gross (Apr 13 2023 at 06:44):Gallina quotation for PCUIC is almost ready. Could someone review the dependent PRs #933, #938, #939 (the last of these is still running on CI, but will hopefully pass soon)?
Théo Winterhalter (Apr 13 2023 at 06:49):#939 fails it seems… :/
#933 looks ok to me but I didn't touch these files so I'd rather someone else approved the merge.
Jason Gross (Apr 13 2023 at 07:28):#939 fails it seems… :/
Looks like something is going wrong in TC inference, I'll have to debug tomorrow
Jason Gross (Apr 13 2023 at 08:36):#939 should hopefully be fixed (apparently Notation interprets things as open_constr without typeclasses not constr nor normal open_constr, for tactics in terms), CI is re-running
Jason Gross (Apr 13 2023 at 20:16):#939 passes
Jason Gross (Apr 14 2023 at 01:08):Once #933, #939, and #942 are merged, I can undraft #940 (Gallina quotation for PCUIC terms).
#944, #943, and #941 are also ready for merge
Matthieu Sozeau (Apr 14 2023 at 09:48):I'm planning to do a release of MetaCoq for Coq 8.17, shall we wait for some particular PRs of yours and bump to 1.2 advertising your work Jason or simply continue on the 1.1 line and consider it experimental/WIP for now?
Jason Gross (Apr 14 2023 at 11:29):If you want to wait for #940 (just undrafted now) and bump, that seems great! (Should I also prepare a PR that adds a README to the directory, or that mentions the appropriate entry point (Quotation.To{Template,PCUIC}.All) in the opam file doc?)
PR #940 completes Gallina quotation for PCUIC terms. While there's still a bit of polishing to be done (mainly removing some dead commented code and figuring out if it's worth writing quotation functions for anything that is not a dependency of typing, maybe also replacing the use of Fixpoints in various places with proper dependent induction principles) and I'm not sure what the ideal set of exported quotation functions is, I think the quotation to terms without typing derivations is basically done and ready for release, and typing of these functions is probably not going to happen anytime soon.
I guess I might try to prove that these functions respect reduction or conversion or something, though that seems like a moderately big undertaking and something that is similarly far off.
Jason Gross (Apr 14 2023 at 11:30):(The other main question is if we want to call it "MetaCoq.Quotation" or rename it to something else)
Matthieu Sozeau (Apr 14 2023 at 11:43):I'm fine with MetaCoq.Quotation and I think a README would be good, starting from the opam package description you provided
Matthieu Sozeau (Apr 14 2023 at 11:55):I'll wait for that and release an 1.2 version for 8.16 and 8.17, that will also correspond to an article we'll put out soon
Jason Gross (Apr 14 2023 at 18:13):#945 adds README; if that looks good, then I think quotation is ready to go once its merged
Jason Gross (Apr 21 2023 at 20:09):If someone could take a look at #953 and #954, I'd appreciate it. (In particular, #955 depends on #954)
Jason Gross (Apr 24 2023 at 01:31):#955 is ready for review (but no rush)
Jason Gross (Jun 03 2023 at 23:50):Could someone review / merge #955 and #958
Last updated: Jun 04 2023 at 23:30 UTC