The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

In the meantime, you can circumvent this issue about Vector.t by simply
avoiding any direct reference to VectorDef in your code. For instance,
adapt your Vnth notation into "Notation Vnth := Vector.nth", and same for
Vmap. This way, only Vector.t gets extracted, not VectorDef.t. This
is clearly a workaround (but I doubt VectorDef is meant to be refered to
by the final user of the Vector library).

This leads me to the second part of your report, which is far more severe:
something informative (in Coq's type "sum") is suddenly considered as
logical by the system (i.e. acceptable in sort "Prop"), and hence discarded
by the extraction, leading to this faulty "match __ with ...". This is
normally impossible in the good old theory of Coq, but this theory around
universes has been so much tweaked in the recent years (Hugo) and months
(Matthieu) that the very foundational principles of extraction need to be
re-asserted, and probably adapted, as shown by this bug. Once again, I'll
let you know when I know more.

Best regards,
Pierre Letouzey

----- Mail original -----
> 
> I confirm, there is currently a mess in the extraction of stdlib's Vector.t.
> VectorDef.t and Vector.t aren't seen as equal as they should be (since
> Vector.v contains an Include of VectorDef), leading to your two distinct
> types t1 and t2. Probably that the Include of module-as-v-file isn't
> well supported by extraction, unlike inner modules (Module...End inside
> a .v file). I'll let you know when that's fixed.
> 
> Sorry for the inconvenience...
> Pierre Letouzey
> 
> PS: for this kind of report, please favor the coq bugtracker instead
> of plain mail to coq-club
> 
> ----- Mail original -----
> > Hello.
> > 
> > I have uploaded my code to github, see
> > 
> > https://github.com/dasuxullebt/deflate
> > 
> > In the main file "deflate.v", I try to extract several things. The
> > extraction of quicksort_nat works. The extraction of fc1 fails somehow:
> > 
> > The type of lists is extracted twice, as "t0" and "t1". If I replace t1
> > with t0 everywhere in the extracted code, then the code segfaults. A
> > minimal reduction of the part that fails is:
> > 
> > let __ = let rec f _ = Obj.repr f in Obj.repr f;;
> > type ('a, 'b) sum =
> > | Inl of 'a
> > | Inr of 'b;;
> > type sumbool =
> > | Left
> > | Right;;
> > match Obj.magic __ with
> > | Inl x -> Left
> > | Inr x -> Right;;
> > 
> > The proofs all should work in the current git-version (at least the
> > version from 1 week ago). Do you have any clue of what is going wrong?
> > 
> > Best Regards,
> > Christoph-Simon Senjak
> > 
>