Stream: math-comp users

Topic: Porting Deriving to math-comp 2.0.0


view this post on Zulip Arthur Azevedo de Amorim (Jun 21 2023 at 14:17):

I've been porting the Deriving library (https://github.com/arthuraa/deriving) to math-comp 2.0.0. I managed to get the code to a state where everything compiles. However, I ended up using some private parts definitions of HB to do so, and I feel that the code still needs some polishing before it is released. I am compiling here some points that need attention, in case anybody has some insight on how to proceed.

I'll add other issues here as I stumble upon them.

CC @Enrico Tassi @Cyril Cohen .

view this post on Zulip Enrico Tassi (Jun 21 2023 at 14:42):

About your first point, this one works (but generates an uglier term...)

diff --git a/theories/base.v b/theories/base.v
index dabdfa8..6b6a052 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -516,7 +516,7 @@ Unset Universe Polymorphism.
 Fixpoint fin_eqClass n : Equality (fin n) :=
   match n return Equality (fin n) with
   | 0 => Equality.on void
-  | n.+1 => Equality.on (option (Equality.pack_ (fin_eqClass n)))
+  | n.+1 => Equality.on (option (HB.pack_for Equality.type (fin n) (fin_eqClass n)))
   end.

 (* FIXME: Choice.pack_ is an internal function *)

view this post on Zulip Enrico Tassi (Jun 21 2023 at 14:46):

About 3, I think it would be possible to have HB add HintUnfold for structures to a db called, say, hb_unfold_structures.

view this post on Zulip Bas Spitters (Sep 01 2023 at 14:38):

@Arthur Azevedo de Amorim has there been any progress on this? It looks like MC 2.0 is generally progressing quite fast.

view this post on Zulip Arthur Azevedo de Amorim (Sep 01 2023 at 15:06):

@Bas Spitters I've been able to make some progress on the above issues, but not all. Nevertheless, the library compiles, and I think that we can already run code that depends on it. I am tempted to just test if extructures works with the 2.0 branch and do a release. What do you think?

view this post on Zulip Karl Palmskog (Sep 01 2023 at 15:10):

I think we generally have too few rather than too many releases of Coq projects. You can always do another release if you notice some problem...

view this post on Zulip Bas Spitters (Sep 01 2023 at 15:17):

I think that would be the best way forward. Thanks!

from my phone

view this post on Zulip Bas Spitters (Sep 19 2023 at 11:27):

@Arthur Azevedo de Amorim will you let us know when you get to it?
https://github.com/arthuraa/extructures/releases

view this post on Zulip Arthur Azevedo de Amorim (Sep 19 2023 at 15:27):

@Bas Spitters Yes. I was planning on working on it last week, but got preempted.

view this post on Zulip Arthur Azevedo de Amorim (Sep 25 2023 at 18:42):

@Bas Spitters OK, the new Deriving and Extructures versions are out!

view this post on Zulip Pierre Roux (Sep 27 2023 at 09:41):

Deriving is now tested on top of MathComp 2 in Coq's CI, same for Extructures in MathComp's CI.

view this post on Zulip Julien Puydt (Sep 29 2023 at 08:09):

There's still no official release of deriving for MC2 - it's one of the packages I'm waiting for before Coq 8.18 and MC 2 get in Debian

view this post on Zulip Karl Palmskog (Sep 29 2023 at 08:10):

@Julien Puydt https://github.com/coq/opam/blob/master/released/packages/coq-deriving/coq-deriving.0.2.0/opam#L13

view this post on Zulip Théo Zimmermann (Sep 29 2023 at 08:12):

(BTW, @Julien Puydt please consider adding coq-lsp and vscoqtop to Debian packages for Coq 8.18, if that's not already the case. They are not in the Coq Platform yet, but should join it in the 8.18-based release.)

view this post on Zulip Julien Puydt (Sep 29 2023 at 08:15):

If I remember well, coq-lsp needs coq-serapi, and since I didn't get a notification, my licensing issue to package it are still current.

view this post on Zulip Julien Puydt (Sep 29 2023 at 08:16):

here

view this post on Zulip Karl Palmskog (Sep 29 2023 at 08:20):

rather than going more off-topic here, I pinged Emilio in the serapi issue


Last updated: Jul 15 2024 at 21:02 UTC