`Require Import Coq.Sorting.Permutation.` slows down `rewrite_strat` > 10x

Aperta
  • Qualcosa non va?
#21 7 commenti 0 reazioni 0 assegnatari Vedi su GitHub

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
Da chiarire
Stato di attività
Ferma
Ambito
performance, tooling

Direzione di ricerca

Inizia riproducendo l’esempio fornito di rewrite_strat con e senza Require Import Coq.Sorting.Permutation, quindi leggi l’issue #15596 e la pull request #15597 collegate. Analizza l’interazione tra rewrite_strat e la ricerca delle typeclass dei morfismi; il lavoro è concluso quando viene identificata la regressione e viene fornita una correzione che rimuova il rallentamento segnalato senza affidarsi al workaround.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

This is a followup on https://github.com/coq/coq/issues/15596, but this time focusing on Require Import, because the fix for https://github.com/coq/coq/issues/15596 only addressed Require.

Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Arith.PeanoNat.

(*
Require Import Coq.Sorting.Permutation.
*)

Local Hint Rewrite Nat.add_0_r : mydb.

Goal forall
    (l : list nat)
    (v v0 mscratch: nat)
    (maprep: Type)
    (m: maprep)
    (Array : (nat -> nat -> maprep -> Prop) ->
               nat -> list nat -> nat -> maprep -> Prop)
    (Scalar : nat -> nat -> maprep -> Prop)
    (atAddr : nat -> (nat -> maprep -> Prop) -> maprep -> Prop)
    (A : atAddr mscratch
                (Array Scalar 4
                       ([v0] ++ [v + 0] ++ l)) m),
      False.
Proof.
  intros.
  Time rewrite_strat (topdown (hints mydb)) in A.

Uncommenting the Require Import Coq.Sorting.Permutation. slows down rewrite_strat by > 10x, to ca 3 seconds.

A workaround is

Global Remove Hints Permutation.Permutation_cons Permutation.Permutation_app' :
  typeclass_instances.

However, if I try to minimize the slowness by replacing Require Import Coq.Sorting.Permutation. with just the signatures of the two trouble-making instances, there's no slowdown:

Require Import Coq.Classes.Morphisms.

Definition Permutation{A: Type}: list A -> list A -> Prop. Admitted.

Local Instance Permutation_cons A :
 Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A).
Admitted.

Local Instance Permutation_app' A :
 Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A).
Admitted.

There seems to be some interesting performance issue in the interaction between rewrite_strat and typeclass search looking for morphisms.

Lingua principale
Rocq Prover
Stelle
45
Fork
39
Merge medio
1g 13h
PR unite (30g)
3

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di rocq-prover/stdlib

Tutte le issue di rocq-prover/stdlib

Issue simili

Altre issue su Performance

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.