Karl Palmskog

For the record, the `@{Type Type|_ _}` version works just fine in 8.20: ```coq From Coq Require Import ssreflect Arith. Definition some_evenT_ssr_have_upoly : { n : nat & Nat.EvenT n}....

> The problem is that `ssr_have_upoly@{Prop Type|_ _}` (the one encountered in the example) should extract to `fun x => x` (the lemma is in Prop so got erased) and...

Unfortunately Zenodo's DOI system is not all that flexible (one general DOI and one for each new upload). If you do a different upload for each package pick of a...

But the "artifact" on Zenodo here would be the tarball/zip of the Platform repo, right? So what a version DOI points to is not arbitrary, but more like: "has the...

@MSoegtropIMC I don't have any good solution. I still think you should upload "Platform release 20XX.YY.Z" as a single artifact in a repository like Zenodo, and then we can cite...

Right. For example, you could use the one on GitHub (e.g., https://github.com/coq/platform/archive/refs/tags/2022.09.1.tar.gz) or generate one of your own tarballs from the Git tag. If I understand correctly, the source code...

Better reproducibility is really nice to have, but I don't think it should be a blocker for uploading Coq Platform releases to a service like Zenodo to make them citeable....

@spitters according to the analysis by Gaëtan on Zulip, this should be something that only affects CertiCoq, and since verified extraction doesn't use anything from CertiCoq, I don't see how...

For the record, the plan is for Alectryon to be ported away from SerAPI during spring of 2025. This leaves one major planned Coq version without Alectryon (chronologically 8.21.0). @ejgallego...

@ndcroos in all but the most active projects, we don't really do GitHub assignments for issues. Typically, an OK from the maintainers (@spitters or @Lysxia) is enough. For example, it's...