From: Claudio Sacerdoti Coen Date: Thu, 24 Apr 2008 12:56:14 +0000 (+0000) Subject: Working and broken URIs. X-Git-Tag: make_still_working~5291 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb4be1b7829ac9aeaea3b97c5a97c89e52322c7b;p=helm.git Working and broken URIs. --- diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST new file mode 100644 index 000000000..c4df65de5 --- /dev/null +++ b/helm/software/components/ng_kernel/TEST @@ -0,0 +1,195 @@ +BellLabs +Cachan +Dyade +Eindhoven +IdealX +Montevideo +Nancy +Paris +Utrecht + +++++++++++++++++ +CoRN: calcolo grafi da caricare troppo lento +Coq: calcolo grafi da caricare troppo lento +Sophia-Antipolis: calcolo grafi da caricare troppo lento + +Suresnes: nuovo nucleo + +Rocq/AILS: type-checking vecchio nucleo troppo lento +Rocq/COC: type-checking vecchio nucleo troppo lento +nijmegen: type-checking vecchio nucleo troppo lento +Rocq/TreeAutomata vecchio nucleo troppo lento +orsay: type-checking vecchio nucleo troppo lento + +Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo + +Altre Rocq: bug vari nuovo nucleo, compresi universi! +matita: nuovo nucleo universi e altro +lyon.ok: vecchio nucleo, variabili +marseille: vecchio nucleo, guarded by constructors +muenchen: nuovo nucleo, guarded by +cachan: nuovo nucleo, guarded by cic:/Coq/Init/Wf/Acc_ind.con + +lannion: nuovo nucleo impredicative set +lyon.impredicative_set: nuovo nucleo impredicative set. Altro? + +============= IMPREDICATIVE SET ====================== +Lannion/Continuations +Lyon/GraphBasics +Lyon/Multiplier +Lyon/CoinductiveExamples +Lyon/Streams +Rocq/Paradoxes: Hurkens e Russell +Rocq/HistoricalExamples +Rocq/HigmanNW + +============= BUG VECCHIO NUCLEO ======================= +Problema con permutazione ens? +cic:/Rocq/ALGEBRA/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon/Adj_FunFreeMon_FunForget.con + +============= CONVERSIONE FIX GENERATIVI ================ +cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con +Appl: wrong application of le_S_n: the parameter H1 has type +le (S (S n0)) (length (prod ad A) (cons (prod ad A) (pair ad A a y) l0)) +but it should have type +le (S (S n0)) (S (alist_nth_ad_semantics___1(0) A l0)) + +cic:/Suresnes/MiniC/Utilitaires/BlockDecl/bdecl_mapkSpec.con +Appl: wrong application of ... + (eq (prod (list Key) Data) (pair (list Key) Data lk d) + (pair (list Key) Data x0 x)) + (In___1(0) (prod (list Key) Data) (pair (list Key) Data x0 x) lm), found or + (eq (prod (list Key) Data) (pair (list Key) Data lk d) + (pair (list Key) Data x0 x)) + (bdecl_mapkSpec___1(0) Key Data (pair (list Key) Data x0 x) lm) + +cic:/Dyade/Otway-Rees/inv1rel5/POinv1rel5.con +Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1)))) + (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB)) + (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type +or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1)))) + (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB)) +but it should have type +In C (B2C (K2B (KeyAB d0 d1))) + (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyAB)) + +cic:/Dyade/Otway-Rees/invprel5/POinvprel5.con +Appl: wrong application of AlreadyIn1: the parameter or_introl (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1)))) + (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab)) + (refl_equal C (B2C (K2B (KeyAB d0 d1)))) has type +or (eq C (B2C (K2B (KeyAB d0 d1))) (B2C (K2B (KeyAB d0 d1)))) + (POinv1rel5___1(0) (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab)) +but it should have type +In C (B2C (K2B (KeyAB d0 d1))) + (cons C (B2C (K2B (KeyAB d0 d1))) (app C l rngDDKKeyABminusKab)) + +cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con +Branch for constructor xI := +λp0:positive. + λn:nat. refl_equal nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n))) +has type ∀p0: positive. + ∀n: nat. + eq nat (plus n (Pmult_nat (Pplus_carry p p0) (plus n n))) + (plus n (Pmult_nat (Pplus_carry p p0) (plus n n))) +not convertible with positive + → (λp0:positive. + ∀n: nat. + eq nat (Pmult_nat (Pplus_carry (xI p) p0) n) + (plus n (Pmult_nat (Pplus (xI p) p0) n))) (xI __1) + +cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con +has type ∀p0: positive. + ∀m: nat. + eq nat (Pmult_nat (Pplus_carry p p0) (plus m m)) + (plus (plus m (Pmult_nat p (plus m m))) + (plus m (Pmult_nat p0 (plus m m)))) +not convertible with positive + → (λp0:positive. + ∀n: nat. + eq nat (Pmult_nat (Pplus (xI p) p0) n) + (plus (Pmult_nat (xI p) n) (Pmult_nat p0 n))) (xI __1) + +cic:/Coq/NArith/BinPos/Pplus_carry_spec.con +has type ∀p0: positive. eq positive (xI (Pplus_carry p p0)) (xI (Pplus_carry p p0)) +not convertible with positive + → (λp0:positive. + eq positive (Pplus_carry (xI p) p0) (Psucc (Pplus (xI p) p0))) + (xI __1) + +cic:/Coq/NArith/BinPos/Pplus_comm.con +has type ∀p0: positive. eq positive (xO (Pplus_carry p p0)) (xO (Pplus_carry p0 p)) +not convertible with positive + → (λp0:positive. eq positive (Pplus (xI p) p0) (Pplus p0 (xI p))) + (xI __1) + +cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con +has type ∀p0: positive. + eq positive (xI (Pplus p (Psucc p0))) (xI (Pplus_carry p p0)) +not convertible with positive + → (λp0:positive. + eq positive (Pplus (xI p) (Psucc p0)) (Psucc (Pplus (xI p) p0))) + (xI __1) + +cic:/Coq/NArith/BinPos/Pplus_assoc.con + eq positive (xI (Pplus x1 (Pplus_carry y0 z0))) + (xI (Pplus (Pplus_carry x1 y0) z0)) +not convertible with positive + → (λp:positive. + eq positive (Pplus (xI x1) (Pplus (xI y0) p)) + (Pplus (Pplus (xI x1) (xI y0)) p)) (xI __1) + +cic:/Coq/NArith/BinPos/Pplus_reg_r.con +has type ∀y1: positive. + ∀H: eq positive (xO (Pplus_carry x1 z0)) (xO (Pplus_carry y1 z0)). + eq positive (xI x1) (xI y1) +not convertible with positive + → (λp:positive. + eq positive (Pplus (xI x1) (xI z0)) (Pplus p (xI z0)) + → eq positive (xI x1) p) (xI __1) + +cic:/Coq/NArith/BinPos/ZL10.con +has type ∀q: positive. + ∀H: eq positive_mask (Pdouble_plus_one_mask (Pminus_mask p q)) (IsPos xH). + eq positive_mask (Pdouble_mask (Pminus_mask p q)) IsNul +not convertible with positive + → (λp0:positive. + eq positive_mask (Pminus_mask (xI p) p0) (IsPos xH) + → eq positive_mask (Pminus_mask_carry (xI p) p0) IsNul) (xO __1) + End: cic:/Coq/NArith/BinPos/ZL10.con + +cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con +has type ∀q: positive. + ∀H: eq comparison (Pcompare p q Eq) Gt. + ex positive + (λh:positive. + and (eq positive_mask (Pdouble_mask (Pminus_mask p q)) (IsPos h)) + (and + (eq positive + match h return λp0:positive. positive + [ xI ⇒ λy':positive. xO (Pplus_carry q y') + | xO ⇒ λy':positive. xI (Pplus q y') + | xH ⇒ xO (Psucc q)] (xI p)) + (or (eq positive h xH) + (eq positive_mask (Pdouble_plus_one_mask (Pminus_mask_carry p q)) + (IsPos (Ppred h)))))) +not convertible with positive + → (λp0:positive. + eq comparison (Pcompare (xI p) p0 Eq) Gt + → ex positive + (λh:positive. + and (eq positive_mask (Pminus_mask (xI p) p0) (IsPos h)) + (and (eq positive (Pplus p0 h) (xI p)) + (or (eq positive h xH) + (eq positive_mask (Pminus_mask_carry (xI p) p0) + (IsPos (Ppred h))))))) (xI __1) + +cic:/Coq/NArith/BinPos/Pplus_diag.con +∀x0: positive. + ∀IHx: eq positive (Pplus x0 x0) (xO x0). + eq positive (xO (Pplus_carry x0 x0)) (xO (xI x0)) +but it should have type +∀p: positive. + eq positive (Pplus p p) (xO p) + → eq positive (Pplus (xI p) (xI p)) (xO (xI p)) + +