Feature Request: Support for Coq 8.10' SProp

[rafoo]

Currently, Coqine's opam file requires a fixed version of Coq (8.8.2). The current stable version of Coq is 8.11.1. Are there plans to update the dependency?

[francoisthire]

One issue is probably the version 8.10 which introduces sprop. Maybe it is easy to fix, but clearly it will change the encoding. Moreover, one should investigate the sprop property that if A : sprop and a a' : A then a is convertible to a'.

[rafoo]

I thought the encoding was already designed as part of your Types 2019 paper "Proof Irrelevance and Predicate Subtyping in Dedukti".

[francoisthire]

I thought the encoding was already designed as part of your Types 2019 paper "Proof Irrelevance and Predicate Subtyping in Dedukti".

It was not implemented because at that time Coq 8.10 was not released.

[rafoo]

Ok, it makes sense.

[amelieled]

Hi! :)
So, if I understand correctly, it's better for now to use Coq 8.8.0 with CoqIne, all right?

[amelieled]

It's very sad because @Gaspi has done a good job, and currently, there are only 6 errors/warnings:

File "src/modules.mli", line 13, characters 73-99:
Error: The type constructor Declarations.constant_body expects 1 argument(s),
       but is here applied to 0 argument(s)

File "src/error.ml", line 6, characters 9-29:
Error: Unbound value CErrors.make_anomaly

File "src/inductives.ml", line 98, characters 66-87:
Error: This expression has type template_arity
       The field template_param_levels does not belong to type Declarations.template_arity

File "src/cname.ml", line 26, characters 61-90:
Error (warning 3): deprecated: VarRef
Use Names.GlobRef.VarRef

File "src/tsorts.ml", line 80, characters 12-29:
Error: Unbound value Term.kind_of_type

File "src/terms.ml", line 68, characters 8-25:
Error: Unbound value Term.kind_of_type1

Good luck! :)

[francoisthire]

A good task for a new commer I guess. More seriously, probably someone should take over the burden of maintenance of CoqInE. <https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> Garanti sans virus. www.avast.com <https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> <#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2> Le lun. 9 nov. 2020 à 21:14, amelieled <notifications@github.com> a écrit :

…

It's very sad because @Gaspi <https://github.com/Gaspi> has done a good job, and currently, there are only 6 errors/warnings: File "src/modules.mli", line 13, characters 73-99: Error: The type constructor Declarations.constant_body expects 1 argument(s), but is here applied to 0 argument(s) File "src/error.ml", line 6, characters 9-29: Error: Unbound value CErrors.make_anomaly File "src/inductives.ml", line 98, characters 66-87: Error: This expression has type template_arity The field template_param_levels does not belong to type Declarations.template_arity File "src/cname.ml", line 26, characters 61-90: Error (warning 3): deprecated: VarRef Use Names.GlobRef.VarRef File "src/tsorts.ml", line 80, characters 12-29: Error: Unbound value Term.kind_of_type File "src/terms.ml", line 68, characters 8-25: Error: Unbound value Term.kind_of_type1 Good luck! :) — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#9 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AATJVK4Q2GRWM4USDNZCT2TSPBESRANCNFSM4NBNIVPA> .

[Gaspi]

I thought the encoding was already designed as part of your Types 2019 paper "Proof Irrelevance and Predicate Subtyping in Dedukti".

Sadly, no. The results of this paper are only used to have the irrelevance of annotating sorts inside the encoding for now. It seems doable to extend it to sprop.

[amelieled]

A good task for a new commer I guess. More seriously, probably someone
should take over the burden of maintenance of CoqInE.

Je veux bien aider @Gaspi pour reprendre la main sur la maintenance par la suite.
C'est potentiellement ambitieux, mais il faut bien commencer quelque part :)

[Gaspi]

C'est très courageux de ta part :) Je suis sur que tu seras à la hauteur !
Une première étape serait de réussir à faire fonctionner l'outil chez toi sur la version de Coq pour laquelle il a été conçu (8.8.2 semble-t-il).
Ensuite je te conseille de "remonter" les versions progressivement. A chaque montée de version la compilation va casser en générant plein (ça peut être des centaines) d'erreurs/warning dus aux petites (ou grandes) variations dans le kernel de Coq : types inductifs légèrement différents, fonctions qui deviennent deprecated ou disparaissent, etc.
Le gros du boulot c'est de comprendre et réparer ces petites erreurs. Parfois ça nécessite de bien comprendre la théorie de Coq.
Bon courage et si tu es complètement bloquée n'hésite pas partager le bug, ça pourra peut-être m'évoquer quelque chose.

[rafoo]

Super ! -- Raphaël Cauderlier