Michael Soegtrop (Mar 31 2023 at 10:47): Michael Soegtrop (Mar 31 2023 at 10:47):I wonder if there will be a 8.17 compatible version soon, or if I shall publish the Coq Platform 2022.03 beta without MetaCoq (since it is in the extended section I would be fine with that).
Matthieu Sozeau (Mar 31 2023 at 11:22):I can release one next week, would that be ok with your schedule?
Michael Soegtrop (Mar 31 2023 at 12:32):I might release a beta before, but it will definitely be OK for the .0 release. Since it is "extended" I have no issue skipping the beta phase for MetaCoq.
Matthieu Sozeau (Apr 13 2023 at 10:17):It took a bit more time than expected but it is almost there https://github.com/MetaCoq/metacoq/actions/runs/4688062275/jobs/8308125558
Michael Soegtrop (Apr 13 2023 at 12:12):You are not the last - I am still waiting for QuickChick ...
Bas Spitters (Apr 14 2023 at 09:49):@Michael Soegtrop Is it connected to this issue?
https://coq.zulipchat.com/#narrow/stream/256336-jsCoq/topic/Quickchick/near/273131235
Michael Soegtrop (Apr 14 2023 at 09:53):I am not sure - I don't know the details but afaik it was more related to hint database changes - but it might several issues. Anyway - QuickChick just did a release!
Bas Spitters (Apr 14 2023 at 10:18):Do you understand the version numbering? https://github.com/QuickChick/QuickChick/tags
I.e. why 1.6.5 instead of 2.0
Michael Soegtrop (Apr 14 2023 at 10:51):Initially they planned to do a 2.0 release but then ran out of time (I think) to finish it.
Michael Soegtrop (Apr 14 2023 at 10:51):See also https://github.com/QuickChick/QuickChick/issues/318.
Michael Soegtrop (Apr 14 2023 at 10:52):But it is getting a bit off topic for MetaCoq ...
Matthieu Sozeau (Apr 21 2023 at 16:22):Finally here: https://github.com/coq/opam-coq-archive/pull/2554
Matthieu Sozeau (Apr 21 2023 at 16:23):However we have a bit of an issue with the opam CI, it seems to go out of memory with some of the ocaml compilers.
Jason Gross (Apr 21 2023 at 20:08):Is there any way to determine what line the issue is at / how much memory is being used? On my machine, tip of coq-8.16 branch, template-coq/theories/uGraph.vo takes (real: 19.84, user: 19.56, sys: 0.24, mem: 1409052 ko) (Coq 8.16.1, OCaml 4.14.0)
Matthieu Sozeau (Apr 22 2023 at 07:16):I don’t know.
Matthieu Sozeau (Apr 22 2023 at 12:45):It seems unavoidable to hit those in the gitlab CI as it is using small instances with barely 3G memory. Using medium instances of runners seems to work better.
Matthieu Sozeau (Apr 22 2023 at 12:46):@Michael Soegtrop you now have 1.2 packages for both 8.16 and 8.17 released in the opam archive
Karl Palmskog (Apr 23 2023 at 10:30):is MetaCoq still at "extended level" in the Platform? To me at least, having MetaCoq as part of "default"/full Platform would be a kind of milestone where we can actually say to would-be plugin authors: if there is any possibility of using MetaCoq to implement what you want, use it to make your code not bitrot into oblivion
Yannick Forster (Apr 23 2023 at 10:31):It would be great to put coq-metacoq-template (the part used to implement plugins) to default - it's very quick to compile. The rest, which is slower, could stay at extended level for now
Karl Palmskog (Apr 23 2023 at 10:32):ping @Michael Soegtrop to check if coq-metacoq-template might have a chance of moving to full level now or in next Platform release
Michael Soegtrop (Apr 24 2023 at 07:17):@Karl Palmskog @Matthieu Sozeau : the question if coq-metacoq-template can move to the full level mostly depends on two questions, both of which I can't answer:
Matthieu Sozeau (Apr 24 2023 at 07:20):The API is relatively stable, it can change with Coq kernel changes, so it's Coq-version-specific. Until now we also managed to make backward compatible changes (e.g. generalizations of monad actions got special cased to implement the previous behavior), so I would say yes to 1. 2 is definitely the case as we're in Coq's CI, it's only a matter of making a package when we branch Coq
Michael Soegtrop (Apr 24 2023 at 07:25):@Matthieu Sozeau : thanks for the clarification. In this case can you please create a corresponding issue in Coq Platform, where you state that you want it to be moved from "extended" to "full" level.
Matthieu Sozeau (Apr 24 2023 at 19:20):Sure, will do
Last updated: Oct 13 2024 at 01:02 UTC