TL;DR: We will meet from Tuesday April 6th to Friday April 9th to do the port. Please make sure you can read this mail in detail and complete the "homework" before that.
In the current state of the mathcomp library, we reached a critical point where it is hard to add a structure on top of the hierarchy and
| From 2924bed46a7576c4e0d8a6a1ff0a18d0c9cf717a Mon Sep 17 00:00:00 2001 | |
| From: gonthier <gonthier@305884b8-be16-0410-aa53-a3be2363cef1> | |
| Date: Mon, 19 Mar 2012 21:21:11 +0000 | |
| Subject: [PATCH] This revision was meant to be a local improvement to falgbra | |
| <-> galois, but it uncovered a major inefficiency of the processing of packed | |
| class declarations by the Coq kernel, which could only be mitigated by | |
| adjusting the packed class idiom. The problem arises from the interference | |
| of several questionable design choices in the Coq kernel, in particular the | |
| blind maximal sharing of "reductions" (which turn out to be full expansions | |
| here). The diagnosis was prompted by the anomalous behaviour of line 302 of |
| these derivations will be built: | |
| /nix/store/gnbnkdr021hsfgnh4awsvp9jp29a4mmk-ocaml4.09.1-elpi-1.11.0.drv | |
| building '/nix/store/gnbnkdr021hsfgnh4awsvp9jp29a4mmk-ocaml4.09.1-elpi-1.11.0.drv'... | |
| unpacking sources | |
| unpacking source archive /nix/store/65h09410f0nhbssijpgqkcgnz27hyvhc-source | |
| source root is source | |
| patching sources | |
| configuring | |
| no configure script, doing nothing | |
| building |
| these derivations will be built: | |
| /nix/store/73q5m4rrvyhdy2zq0vs33r6zkkzp7lgd-ocaml4.09.1-elpi-1.11.0.drv | |
| building '/nix/store/73q5m4rrvyhdy2zq0vs33r6zkkzp7lgd-ocaml4.09.1-elpi-1.11.0.drv'... | |
| unpacking sources | |
| unpacking source archive /nix/store/65h09410f0nhbssijpgqkcgnz27hyvhc-source | |
| source root is source | |
| patching sources | |
| configuring | |
| no configure script, doing nothing | |
| building |
| zulip@cc-VirtualBox:~/deployments/current$ ./manage.py import all-coq converted_gitter_data | |
| Processing dump: /home/zulip/deployments/2020-05-01-02-14-56/converted_gitter_data ... | |
| 2020-05-01 00:49:23.667 INFO [] Importing realm dump /home/zulip/deployments/2020-05-01-02-14-56/converted_gitter_data | |
| 2020-05-01 00:49:23.673 INFO [] Importing realm data from /home/zulip/deployments/2020-05-01-02-14-56/converted_gitter_data/realm.json | |
| 2020-05-01 00:49:23.742 INFO [] Successfully imported <class 'zerver.models.Stream'> from zerver_stream. | |
| 2020-05-01 00:49:24.424 INFO [] Successfully imported <class 'zerver.models.DefaultStream'> from zerver_defaultstream. | |
| 2020-05-01 00:49:24.425 INFO [] Successfully imported <class 'zerver.models.RealmEmoji'> from zerver_realmemoji. | |
| 2020-05-01 00:49:24.450 INFO [] Successfully imported <class 'zerver.models.RealmDomain'> from zerver_realmdomain. | |
| 2020-05-01 00:49:24.451 INFO [] Successfully imported <class 'zerver.models.RealmFilter'> from zerver_realmfilter. | |
| 2020-05-01 00:49:24.489 |
| zulip@cc-VirtualBox:~/deployments/current$ ./manage.py import just-coq coq | |
| Processing dump: /home/zulip/deployments/2020-05-01-02-14-56/coq ... | |
| 2020-05-01 00:19:54.951 INFO [] Importing realm dump /home/zulip/deployments/2020-05-01-02-14-56/coq | |
| 2020-05-01 00:19:55.219 INFO [] Importing realm data from /home/zulip/deployments/2020-05-01-02-14-56/coq/realm.json | |
| 2020-05-01 00:19:55.263 INFO [] Successfully imported <class 'zerver.models.Stream'> from zerver_stream. | |
| 2020-05-01 00:20:17.525 INFO [] Successfully imported <class 'zerver.models.DefaultStream'> from zerver_defaultstream. | |
| 2020-05-01 00:20:17.526 INFO [] Successfully imported <class 'zerver.models.RealmEmoji'> from zerver_realmemoji. | |
| 2020-05-01 00:20:17.550 INFO [] Successfully imported <class 'zerver.models.RealmDomain'> from zerver_realmdomain. | |
| 2020-05-01 00:20:17.552 INFO [] Successfully imported <class 'zerver.models.RealmFilter'> from zerver_realmfilter. | |
| 2020-05-01 00:20:17.582 INFO [] Successfully imported <class 'zerver.models.Recipient'> from ze |
| Require Import generic_quotient. | |
| Module Type Enumeration_signature. | |
| Parameter type : choiceType -> Type. | |
| Section Operations. | |
| Context {T : choiceType}. | |
| Parameter of_seq : seq T -> type T. | |
| Parameter seq : type T -> seq_eqclass T. | |
| Axiom eq : forall e1 e2, seq e1 =i seq e2 -> e1 = e2. | |
| Axiom mem : forall s, seq (of_seq s) =i s. |