Stream: MetaCoq

Topic: 8.17 version / Coq Platform 2022.03 beta


view this post on Zulip 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).

view this post on Zulip Matthieu Sozeau (Mar 31 2023 at 11:22):

I can release one next week, would that be ok with your schedule?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Apr 13 2023 at 12:12):

You are not the last - I am still waiting for QuickChick ...

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Apr 14 2023 at 10:51):

See also https://github.com/QuickChick/QuickChick/issues/318.

view this post on Zulip Michael Soegtrop (Apr 14 2023 at 10:52):

But it is getting a bit off topic for MetaCoq ...

view this post on Zulip Matthieu Sozeau (Apr 21 2023 at 16:22):

Finally here: https://github.com/coq/opam-coq-archive/pull/2554

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Matthieu Sozeau (Apr 22 2023 at 07:16):

I don’t know.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Apr 24 2023 at 19:20):

Sure, will do


Last updated: Jul 23 2024 at 21:01 UTC