coqc infinite loop in type class resolution
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 35/100
- Tipo di issue
- Bug
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- compilers
Direzione di ricerca
Inizia compilando con coqc il programma minimo presente nell’issue e conferma che la risoluzione delle type class non termina. Analizza il percorso di risoluzione delle type class coinvolto nelle istanze Equivalence e Op; il lavoro è completato quando il riproduttore termina invece di entrare in un ciclo indefinito.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Description of the problem
Compiling this program makes coqc go into an infinite loop.
Note that there is a "bug" in the program because I commented out `(Equivalence F).
This will make coqc search forever for which Equivalence instance it should
use in foo.
Require Import Setoid.
Require Import RelationClasses. (* for Equivalence *)
Definition equ {T} {e} `(Equivalence T e) := e.
Notation "f == g" := (equ _ f g) (at level 80).
Class Op (A:Type) := op : A -> A -> A.
Class C F `(Op F) (* `(Equivalence F) *) :=
{
foo : forall a b , op a b == op a b;
}.
Coq Version
I installed v8.15.1 with nix.
[nix-shell]$ coqc --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.12.1
I also tried 8.14.1 and 8.13.1 with the same result.
And I just (July 16, 2022) tried it with master, i.e. 8.17+alpha 672b1443441df4e4777c4d2f7f6fb953bd97544a , and it still has the same problem.
- Lingua principale
- Rocq Prover
- Stelle
- 42
- Fork
- 40
- Merge medio
- 20h 23m
- PR unite (30g)
- 2
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di rocq-prover/stdlib
-
incl_dec and NoDup_dec should be Defined and not QedForse di nuovo libera Una pull request per questa issue è stata chiusa senza essere unita. Aperta
Difficoltà 1/5 1-3 ore Idoneità per principianti 65/100
rocq-prover/stdlib#25 ·
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)Forse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100
rocq-prover/stdlib#312 ·
-
Maintaining NaryFunctionsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#293 ·
-
`QArith`: Add more rounding modes to complement `Qfloor` and `Qceiling`Forse già presa @RyanGlScott l’ha presa 87 giorni fa. Aperta
Difficoltà 3/5 1-2 giorni Idoneità per principianti 52/100
rocq-prover/stdlib#283 · 2 commenti ·
-
Inconsistent OPAM packaging of rocq-stdlibForse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100
rocq-prover/stdlib#256 · 4 commenti · 3 reazioni ·
Tutte le issue di rocq-prover/stdlib
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 76/100
I maintainer di solito rispondono entro 1 giorno
-
erdos-status-sync
Difficoltà 2/5 1-3 ore Idoneità per principianti 65/100
google-deepmind/formal-conjectures#6920 ·
I maintainer di solito rispondono entro 1 giorno
-
area-web-js web-libraries
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
I maintainer di solito rispondono entro 4 giorni
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
objectionary/eo#9317 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 74/100
rubys/roundhouse#571 ·
I maintainer di solito rispondono entro 1 giorno