text:
# Finitely graded posets

```agda
module order-theory.finitely-graded-posets where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.inequality-standard-finite-types
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.natural-numbers

open import foundation.binary-relations
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equality-dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.transport
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import order-theory.bottom-elements-posets
open import order-theory.posets
open import order-theory.preorders
open import order-theory.top-elements-posets
open import order-theory.total-orders

open import univalent-combinatorics.standard-finite-types
```

</details>

## Idea

A **finitely graded poset** consists of a family of types indexed by
`Fin (succ-ℕ k)` equipped with an ordering relation from `Fin (inl i)` to
`Fin (succ-Fin (inl i))` for each `i : Fin k`.

```agda
Finitely-Graded-Poset : (l1 l2 : Level) (k : ℕ) → UU (lsuc l1 ⊔ lsuc l2)
Finitely-Graded-Poset l1 l2 k =
  Σ ( Fin (succ-ℕ k) → Set l1)
    ( λ X →
      (i : Fin k) → type-Set (X (inl-Fin k i)) →
      type-Set (X (succ-Fin (succ-ℕ k) (inl-Fin k i))) → Prop l2)

module _
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    (i : Fin (succ-ℕ k))
    where

    face-Finitely-Graded-Poset-Set : Set l1
    face-Finitely-Graded-Poset-Set = pr1 X i

    face-Finitely-Graded-Poset : UU l1
    face-Finitely-Graded-Poset =
      type-Set face-Finitely-Graded-Poset-Set

    is-set-face-Finitely-Graded-Poset :
      is-set face-Finitely-Graded-Poset
    is-set-face-Finitely-Graded-Poset =
      is-set-type-Set face-Finitely-Graded-Poset-Set

  module _
    (i : Fin k) (y : face-Finitely-Graded-Poset (inl-Fin k i))
    (z : face-Finitely-Graded-Poset (succ-Fin (succ-ℕ k) (inl-Fin k i)))
    where

    adjacent-Finitely-Graded-Poset-Prop : Prop l2
    adjacent-Finitely-Graded-Poset-Prop = pr2 X i y z

    adjacent-Finitely-Graded-Poset : UU l2
    adjacent-Finitely-Graded-Poset =
      type-Prop adjacent-Finitely-Graded-Poset-Prop

    is-prop-adjacent-Finitely-Graded-Poset :
      is-prop adjacent-Finitely-Graded-Poset
    is-prop-adjacent-Finitely-Graded-Poset =
      is-prop-type-Prop adjacent-Finitely-Graded-Poset-Prop

  set-Finitely-Graded-Poset : Set l1
  set-Finitely-Graded-Poset =
    Σ-Set (Fin-Set (succ-ℕ k)) face-Finitely-Graded-Poset-Set

  type-Finitely-Graded-Poset : UU l1
  type-Finitely-Graded-Poset = type-Set set-Finitely-Graded-Poset

  is-set-type-Finitely-Graded-Poset : is-set type-Finitely-Graded-Poset
  is-set-type-Finitely-Graded-Poset =
    is-set-type-Set set-Finitely-Graded-Poset

  element-face-Finitely-Graded-Poset :
    {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset i →
    type-Finitely-Graded-Poset
  element-face-Finitely-Graded-Poset {i} x = pair i x

  shape-Finitely-Graded-Poset :
    type-Finitely-Graded-Poset → Fin (succ-ℕ k)
  shape-Finitely-Graded-Poset (pair i x) = i

  face-type-Finitely-Graded-Poset :
    (x : type-Finitely-Graded-Poset) →
    face-Finitely-Graded-Poset (shape-Finitely-Graded-Poset x)
  face-type-Finitely-Graded-Poset (pair i x) = x

  module _
    {i : Fin (succ-ℕ k)} (x : face-Finitely-Graded-Poset i)
    where
```

If chains with jumps are never used, we'd like to call the following chains.

```agda
    data
      path-faces-Finitely-Graded-Poset :
        {j : Fin (succ-ℕ k)} (y : face-Finitely-Graded-Poset j) →
        UU (l1 ⊔ l2)
        where
        refl-path-faces-Finitely-Graded-Poset :
          path-faces-Finitely-Graded-Poset x
        cons-path-faces-Finitely-Graded-Poset :
          {j : Fin k} {y : face-Finitely-Graded-Poset (inl-Fin k j)}
          {z : face-Finitely-Graded-Poset (succ-Fin (succ-ℕ k) (inl-Fin k j))} →
          adjacent-Finitely-Graded-Poset j y z →
          path-faces-Finitely-Graded-Poset y →
          path-faces-Finitely-Graded-Poset z

  tr-refl-path-faces-Finitely-Graded-Poset :
    {i j : Fin (succ-ℕ k)} (p : Id j i) (x : face-Finitely-Graded-Poset j) →
    path-faces-Finitely-Graded-Poset
      ( tr face-Finitely-Graded-Poset p x)
      ( x)
  tr-refl-path-faces-Finitely-Graded-Poset refl x =
    refl-path-faces-Finitely-Graded-Poset

  concat-path-faces-Finitely-Graded-Poset :
    {i1 i2 i3 : Fin (succ-ℕ k)}
    {x : face-Finitely-Graded-Poset i1}
    {y : face-Finitely-Graded-Poset i2}
    {z : face-Finitely-Graded-Poset i3} →
    path-faces-Finitely-Graded-Poset y z →
    path-faces-Finitely-Graded-Poset x y →
    path-faces-Finitely-Graded-Poset x z
  concat-path-faces-Finitely-Graded-Poset
    refl-path-faces-Finitely-Graded-Poset K = K
  concat-path-faces-Finitely-Graded-Poset
    ( cons-path-faces-Finitely-Graded-Poset x H) K =
    cons-path-faces-Finitely-Graded-Poset x
      ( concat-path-faces-Finitely-Graded-Poset H K)

  path-elements-Finitely-Graded-Poset :
    (x y : type-Finitely-Graded-Poset) → UU (l1 ⊔ l2)
  path-elements-Finitely-Graded-Poset (pair i x) (pair j y) =
    path-faces-Finitely-Graded-Poset x y

  refl-path-elements-Finitely-Graded-Poset :
    (x : type-Finitely-Graded-Poset) →
    path-elements-Finitely-Graded-Poset x x
  refl-path-elements-Finitely-Graded-Poset x =
    refl-path-faces-Finitely-Graded-Poset

  concat-path-elements-Finitely-Graded-Poset :
    (x y z : type-Finitely-Graded-Poset) →
    path-elements-Finitely-Graded-Poset y z →
    path-elements-Finitely-Graded-Poset x y →
    path-elements-Finitely-Graded-Poset x z
  concat-path-elements-Finitely-Graded-Poset x y z =
    concat-path-faces-Finitely-Graded-Poset

  leq-type-path-faces-Finitely-Graded-Poset :
    {i1 i2 : Fin (succ-ℕ k)} (x : face-Finitely-Graded-Poset i1)
    (y : face-Finitely-Graded-Poset i2) →
    path-faces-Finitely-Graded-Poset x y → leq-Fin (succ-ℕ k) i1 i2
  leq-type-path-faces-Finitely-Graded-Poset {i1} x .x
    refl-path-faces-Finitely-Graded-Poset = refl-leq-Fin (succ-ℕ k) i1
  leq-type-path-faces-Finitely-Graded-Poset {i1} x y
    ( cons-path-faces-Finitely-Graded-Poset {i3} {z} H K) =
    transitive-leq-Fin
      ( succ-ℕ k)
      ( i1)
      ( inl-Fin k i3)
      ( succ-Fin (succ-ℕ k) (inl-Fin k i3))
      ( leq-succ-Fin k i3)
      ( leq-type-path-faces-Finitely-Graded-Poset x z K)
```

### Antisymmetry of path-elements-Finitely-Graded-Poset

```agda
eq-path-elements-Finitely-Graded-Poset :
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  (x y : type-Finitely-Graded-Poset X) →
  (p : Id (shape-Finitely-Graded-Poset X x)
          (shape-Finitely-Graded-Poset X y)) →
  path-elements-Finitely-Graded-Poset X x y → Id x y
eq-path-elements-Finitely-Graded-Poset {k} X (pair i1 x) (pair .i1 .x) p
  refl-path-faces-Finitely-Graded-Poset = refl
eq-path-elements-Finitely-Graded-Poset {k = succ-ℕ k} X (pair i1 x)
  (pair .(succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2)) y) p
  (cons-path-faces-Finitely-Graded-Poset {i2} {z} H K) =
  ex-falso
    ( has-no-fixed-points-succ-Fin
      { succ-ℕ (succ-ℕ k)}
      ( inl-Fin (succ-ℕ k) i2)
      ( λ (q : is-one-ℕ (succ-ℕ (succ-ℕ k))) →
        is-nonzero-succ-ℕ k (is-injective-succ-ℕ q))
      ( antisymmetric-leq-Fin
        ( succ-ℕ (succ-ℕ k))
        ( succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2))
        ( inl-Fin (succ-ℕ k) i2)
        ( transitive-leq-Fin
          ( succ-ℕ (succ-ℕ k))
          ( skip-zero-Fin (succ-ℕ k) i2)
          ( i1)
          ( inl i2)
          ( leq-type-path-faces-Finitely-Graded-Poset X x z K)
          ( tr
            ( leq-Fin
              ( succ-ℕ (succ-ℕ k))
              ( succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2)))
            ( inv p)
            ( refl-leq-Fin
              ( succ-ℕ (succ-ℕ k))
              ( succ-Fin (succ-ℕ (succ-ℕ k)) (inl-Fin (succ-ℕ k) i2)))))
        ( leq-succ-Fin (succ-ℕ k) i2)))

module _
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  where

  abstract
    eq-path-faces-Finitely-Graded-Poset :
      {i : Fin (succ-ℕ k)} (x y : face-Finitely-Graded-Poset X i) →
      path-faces-Finitely-Graded-Poset X x y → Id x y
    eq-path-faces-Finitely-Graded-Poset {i} x y H =
      map-left-unit-law-Σ-is-contr
        ( is-proof-irrelevant-is-prop
          ( is-set-Fin (succ-ℕ k) i i)
          ( refl))
        ( refl)
        ( pair-eq-Σ
          ( eq-path-elements-Finitely-Graded-Poset X
            ( element-face-Finitely-Graded-Poset X x)
            ( element-face-Finitely-Graded-Poset X y)
            ( refl)
            ( H)))

  antisymmetric-path-elements-Finitely-Graded-Poset :
    (x y : type-Finitely-Graded-Poset X) →
    path-elements-Finitely-Graded-Poset X x y →
    path-elements-Finitely-Graded-Poset X y x →
    Id x y
  antisymmetric-path-elements-Finitely-Graded-Poset (pair i x) (pair j y) H K =
    eq-path-elements-Finitely-Graded-Poset X (pair i x) (pair j y)
      ( antisymmetric-leq-Fin (succ-ℕ k)
        ( shape-Finitely-Graded-Poset X (pair i x))
        ( shape-Finitely-Graded-Poset X (pair j y))
        ( leq-type-path-faces-Finitely-Graded-Poset X x y H)
        ( leq-type-path-faces-Finitely-Graded-Poset X y x K))
      ( H)
```

### Poset structure on the underlying type of a finitely graded poset

```agda
module _
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    (x y : type-Finitely-Graded-Poset X)
    where

    leq-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
    leq-Finitely-Graded-Poset-Prop =
      trunc-Prop (path-elements-Finitely-Graded-Poset X x y)

    leq-Finitely-Graded-Poset : UU (l1 ⊔ l2)
    leq-Finitely-Graded-Poset = type-Prop leq-Finitely-Graded-Poset-Prop

    is-prop-leq-Finitely-Graded-Poset : is-prop leq-Finitely-Graded-Poset
    is-prop-leq-Finitely-Graded-Poset =
      is-prop-type-Prop leq-Finitely-Graded-Poset-Prop

  refl-leq-Finitely-Graded-Poset :
    is-reflexive leq-Finitely-Graded-Poset
  refl-leq-Finitely-Graded-Poset x =
    unit-trunc-Prop (refl-path-elements-Finitely-Graded-Poset X x)

  transitive-leq-Finitely-Graded-Poset :
    is-transitive leq-Finitely-Graded-Poset
  transitive-leq-Finitely-Graded-Poset x y z H K =
    apply-universal-property-trunc-Prop H
      ( leq-Finitely-Graded-Poset-Prop x z)
      ( λ L →
        apply-universal-property-trunc-Prop K
          ( leq-Finitely-Graded-Poset-Prop x z)
          ( λ M →
            unit-trunc-Prop
              ( concat-path-elements-Finitely-Graded-Poset X x y z L M)))

  antisymmetric-leq-Finitely-Graded-Poset :
    is-antisymmetric leq-Finitely-Graded-Poset
  antisymmetric-leq-Finitely-Graded-Poset x y H K =
    apply-universal-property-trunc-Prop H
      ( Id-Prop (set-Finitely-Graded-Poset X) x y)
      ( λ L →
        apply-universal-property-trunc-Prop K
          ( Id-Prop (set-Finitely-Graded-Poset X) x y)
          ( λ M →
            antisymmetric-path-elements-Finitely-Graded-Poset X x y L M))

  preorder-Finitely-Graded-Poset : Preorder l1 (l1 ⊔ l2)
  pr1 preorder-Finitely-Graded-Poset = type-Finitely-Graded-Poset X
  pr1 (pr2 preorder-Finitely-Graded-Poset) = leq-Finitely-Graded-Poset-Prop
  pr1 (pr2 (pr2 preorder-Finitely-Graded-Poset)) =
    refl-leq-Finitely-Graded-Poset
  pr2 (pr2 (pr2 preorder-Finitely-Graded-Poset)) =
    transitive-leq-Finitely-Graded-Poset

  poset-Finitely-Graded-Poset : Poset l1 (l1 ⊔ l2)
  pr1 poset-Finitely-Graded-Poset = preorder-Finitely-Graded-Poset
  pr2 poset-Finitely-Graded-Poset = antisymmetric-leq-Finitely-Graded-Poset
```

### Least and largest elements in finitely graded posets

We make sure that the least element is a face of type zero-Fin, and that the
largest element is a face of type neg-one-Fin.

```agda
module _
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    (x : face-Finitely-Graded-Poset X (zero-Fin k))
    where

    is-bottom-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
    is-bottom-element-Finitely-Graded-Poset-Prop =
      is-bottom-element-Poset-Prop
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-bottom-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)
    is-bottom-element-Finitely-Graded-Poset =
      is-bottom-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-prop-is-bottom-element-Finitely-Graded-Poset :
      is-prop is-bottom-element-Finitely-Graded-Poset
    is-prop-is-bottom-element-Finitely-Graded-Poset =
      is-prop-is-bottom-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

  has-bottom-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)
  has-bottom-element-Finitely-Graded-Poset =
    Σ ( face-Finitely-Graded-Poset X (zero-Fin k))
      ( is-bottom-element-Finitely-Graded-Poset)

  all-elements-equal-has-bottom-element-Finitely-Graded-Poset :
    all-elements-equal has-bottom-element-Finitely-Graded-Poset
  all-elements-equal-has-bottom-element-Finitely-Graded-Poset
    ( pair x H)
    ( pair y K) =
    eq-type-subtype
      ( is-bottom-element-Finitely-Graded-Poset-Prop)
      ( apply-universal-property-trunc-Prop
        ( H (element-face-Finitely-Graded-Poset X y))
        ( Id-Prop (face-Finitely-Graded-Poset-Set X (zero-Fin k)) x y)
        ( eq-path-faces-Finitely-Graded-Poset X x y))

  is-prop-has-bottom-element-Finitely-Graded-Poset :
    is-prop has-bottom-element-Finitely-Graded-Poset
  is-prop-has-bottom-element-Finitely-Graded-Poset =
    is-prop-all-elements-equal
      all-elements-equal-has-bottom-element-Finitely-Graded-Poset

  has-bottom-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
  pr1 has-bottom-element-Finitely-Graded-Poset-Prop =
    has-bottom-element-Finitely-Graded-Poset
  pr2 has-bottom-element-Finitely-Graded-Poset-Prop =
    is-prop-has-bottom-element-Finitely-Graded-Poset

  module _
    (x : face-Finitely-Graded-Poset X (neg-one-Fin k))
    where

    is-top-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
    is-top-element-Finitely-Graded-Poset-Prop =
      is-top-element-Poset-Prop
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-top-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)
    is-top-element-Finitely-Graded-Poset =
      is-top-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

    is-prop-is-top-element-Finitely-Graded-Poset :
      is-prop is-top-element-Finitely-Graded-Poset
    is-prop-is-top-element-Finitely-Graded-Poset =
      is-prop-is-top-element-Poset
        ( poset-Finitely-Graded-Poset X)
        ( element-face-Finitely-Graded-Poset X x)

  has-top-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)
  has-top-element-Finitely-Graded-Poset =
    Σ ( face-Finitely-Graded-Poset X (neg-one-Fin k))
      ( is-top-element-Finitely-Graded-Poset)

  all-elements-equal-has-top-element-Finitely-Graded-Poset :
    all-elements-equal has-top-element-Finitely-Graded-Poset
  all-elements-equal-has-top-element-Finitely-Graded-Poset
    (pair x H) (pair y K) =
    eq-type-subtype
      ( is-top-element-Finitely-Graded-Poset-Prop)
      ( apply-universal-property-trunc-Prop
        ( K (element-face-Finitely-Graded-Poset X x))
        ( Id-Prop (face-Finitely-Graded-Poset-Set X (neg-one-Fin k)) x y)
        ( eq-path-faces-Finitely-Graded-Poset X x y))

  is-prop-has-top-element-Finitely-Graded-Poset :
    is-prop has-top-element-Finitely-Graded-Poset
  is-prop-has-top-element-Finitely-Graded-Poset =
    is-prop-all-elements-equal
      all-elements-equal-has-top-element-Finitely-Graded-Poset

  has-top-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
  pr1 has-top-element-Finitely-Graded-Poset-Prop =
    has-top-element-Finitely-Graded-Poset
  pr2 has-top-element-Finitely-Graded-Poset-Prop =
    is-prop-has-top-element-Finitely-Graded-Poset

  has-bottom-and-top-element-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2)
  has-bottom-and-top-element-Finitely-Graded-Poset-Prop =
    prod-Prop
      has-bottom-element-Finitely-Graded-Poset-Prop
      has-top-element-Finitely-Graded-Poset-Prop

  has-bottom-and-top-element-Finitely-Graded-Poset : UU (l1 ⊔ l2)
  has-bottom-and-top-element-Finitely-Graded-Poset =
    type-Prop has-bottom-and-top-element-Finitely-Graded-Poset-Prop

  is-prop-has-bottom-and-top-element-Finitely-Graded-Poset :
    is-prop has-bottom-and-top-element-Finitely-Graded-Poset
  is-prop-has-bottom-and-top-element-Finitely-Graded-Poset =
    is-prop-type-Prop has-bottom-and-top-element-Finitely-Graded-Poset-Prop
```

## Finitely graded subposets

```agda
module _
  {l1 l2 l3 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  (S : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l3)
  where

  module _
    (i : Fin (succ-ℕ k))
    where

    face-set-Finitely-Graded-Subposet : Set (l1 ⊔ l3)
    face-set-Finitely-Graded-Subposet =
      Σ-Set
        ( face-Finitely-Graded-Poset-Set X i)
        ( λ x → set-Prop (S x))

    face-Finitely-Graded-Subposet : UU (l1 ⊔ l3)
    face-Finitely-Graded-Subposet = type-Set face-set-Finitely-Graded-Subposet

    is-set-face-Finitely-Graded-Subposet : is-set face-Finitely-Graded-Subposet
    is-set-face-Finitely-Graded-Subposet =
      is-set-type-Set face-set-Finitely-Graded-Subposet

    eq-face-Finitely-Graded-Subposet :
      (x y : face-Finitely-Graded-Subposet) → Id (pr1 x) (pr1 y) → Id x y
    eq-face-Finitely-Graded-Subposet x y = eq-type-subtype S

    emb-face-Finitely-Graded-Subposet :
      face-Finitely-Graded-Subposet ↪ face-Finitely-Graded-Poset X i
    emb-face-Finitely-Graded-Subposet = emb-subtype S

    map-emb-face-Finitely-Graded-Subposet :
      face-Finitely-Graded-Subposet → face-Finitely-Graded-Poset X i
    map-emb-face-Finitely-Graded-Subposet =
      map-emb emb-face-Finitely-Graded-Subposet

    is-emb-map-emb-face-Finitely-Graded-Subposet :
      is-emb map-emb-face-Finitely-Graded-Subposet
    is-emb-map-emb-face-Finitely-Graded-Subposet =
      is-emb-map-emb emb-face-Finitely-Graded-Subposet

  module _
    (i : Fin k) (y : face-Finitely-Graded-Subposet (inl-Fin k i))
    (z : face-Finitely-Graded-Subposet (succ-Fin (succ-ℕ k) (inl-Fin k i)))
    where

    adjacent-Finitely-Graded-subPoset-Prop : Prop l2
    adjacent-Finitely-Graded-subPoset-Prop =
      adjacent-Finitely-Graded-Poset-Prop X i (pr1 y) (pr1 z)

    adjacent-Finitely-Graded-Subposet : UU l2
    adjacent-Finitely-Graded-Subposet =
      type-Prop adjacent-Finitely-Graded-subPoset-Prop

    is-prop-adjacent-Finitely-Graded-Subposet :
      is-prop adjacent-Finitely-Graded-Subposet
    is-prop-adjacent-Finitely-Graded-Subposet =
      is-prop-type-Prop adjacent-Finitely-Graded-subPoset-Prop

  element-set-Finitely-Graded-Subposet : Set (l1 ⊔ l3)
  element-set-Finitely-Graded-Subposet =
    Σ-Set (Fin-Set (succ-ℕ k)) face-set-Finitely-Graded-Subposet

  type-Finitely-Graded-Subposet : UU (l1 ⊔ l3)
  type-Finitely-Graded-Subposet =
    type-Set element-set-Finitely-Graded-Subposet

  emb-type-Finitely-Graded-Subposet :
    type-Finitely-Graded-Subposet ↪ type-Finitely-Graded-Poset X
  emb-type-Finitely-Graded-Subposet =
    tot-emb emb-face-Finitely-Graded-Subposet

  map-emb-type-Finitely-Graded-Subposet :
    type-Finitely-Graded-Subposet → type-Finitely-Graded-Poset X
  map-emb-type-Finitely-Graded-Subposet =
    map-emb emb-type-Finitely-Graded-Subposet

  is-emb-map-emb-type-Finitely-Graded-Subposet :
    is-emb map-emb-type-Finitely-Graded-Subposet
  is-emb-map-emb-type-Finitely-Graded-Subposet =
    is-emb-map-emb emb-type-Finitely-Graded-Subposet

  is-injective-map-emb-type-Finitely-Graded-Subposet :
    is-injective map-emb-type-Finitely-Graded-Subposet
  is-injective-map-emb-type-Finitely-Graded-Subposet =
    is-injective-is-emb is-emb-map-emb-type-Finitely-Graded-Subposet

  is-set-type-Finitely-Graded-Subposet :
    is-set type-Finitely-Graded-Subposet
  is-set-type-Finitely-Graded-Subposet =
    is-set-type-Set element-set-Finitely-Graded-Subposet

  leq-Finitely-Graded-Subposet-Prop :
    (x y : type-Finitely-Graded-Subposet) → Prop (l1 ⊔ l2)
  leq-Finitely-Graded-Subposet-Prop x y =
    leq-Finitely-Graded-Poset-Prop X
      ( map-emb-type-Finitely-Graded-Subposet x)
      ( map-emb-type-Finitely-Graded-Subposet y)

  leq-Finitely-Graded-Subposet :
    (x y : type-Finitely-Graded-Subposet) → UU (l1 ⊔ l2)
  leq-Finitely-Graded-Subposet x y =
    type-Prop (leq-Finitely-Graded-Subposet-Prop x y)

  is-prop-leq-Finitely-Graded-Subposet :
    (x y : type-Finitely-Graded-Subposet) →
    is-prop (leq-Finitely-Graded-Subposet x y)
  is-prop-leq-Finitely-Graded-Subposet x y =
    is-prop-type-Prop (leq-Finitely-Graded-Subposet-Prop x y)

  refl-leq-Finitely-Graded-Subposet :
    (x : type-Finitely-Graded-Subposet) → leq-Finitely-Graded-Subposet x x
  refl-leq-Finitely-Graded-Subposet x =
    refl-leq-Finitely-Graded-Poset X
      ( map-emb-type-Finitely-Graded-Subposet x)

  transitive-leq-Finitely-Graded-Subposet :
    (x y z : type-Finitely-Graded-Subposet) →
    leq-Finitely-Graded-Subposet y z → leq-Finitely-Graded-Subposet x y →
    leq-Finitely-Graded-Subposet x z
  transitive-leq-Finitely-Graded-Subposet x y z =
    transitive-leq-Finitely-Graded-Poset X
      ( map-emb-type-Finitely-Graded-Subposet x)
      ( map-emb-type-Finitely-Graded-Subposet y)
      ( map-emb-type-Finitely-Graded-Subposet z)

  antisymmetric-leq-Finitely-Graded-Subposet :
    (x y : type-Finitely-Graded-Subposet) →
    leq-Finitely-Graded-Subposet x y → leq-Finitely-Graded-Subposet y x → Id x y
  antisymmetric-leq-Finitely-Graded-Subposet x y H K =
    is-injective-map-emb-type-Finitely-Graded-Subposet
      ( antisymmetric-leq-Finitely-Graded-Poset X
        ( map-emb-type-Finitely-Graded-Subposet x)
        ( map-emb-type-Finitely-Graded-Subposet y)
        ( H)
        ( K))

  preorder-Finitely-Graded-Subposet : Preorder (l1 ⊔ l3) (l1 ⊔ l2)
  pr1 preorder-Finitely-Graded-Subposet =
    type-Finitely-Graded-Subposet
  pr1 (pr2 preorder-Finitely-Graded-Subposet) =
    leq-Finitely-Graded-Subposet-Prop
  pr1 (pr2 (pr2 preorder-Finitely-Graded-Subposet)) =
    refl-leq-Finitely-Graded-Subposet
  pr2 (pr2 (pr2 preorder-Finitely-Graded-Subposet)) =
    transitive-leq-Finitely-Graded-Subposet

  poset-Finitely-Graded-Subposet : Poset (l1 ⊔ l3) (l1 ⊔ l2)
  pr1 poset-Finitely-Graded-Subposet =
    preorder-Finitely-Graded-Subposet
  pr2 poset-Finitely-Graded-Subposet =
    antisymmetric-leq-Finitely-Graded-Subposet
```

### Inclusion of finitely graded subposets

```agda
module _
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    {l3 l4 : Level}
    (S : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l3)
    (T : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l4)
    where

    inclusion-Finitely-Graded-Subposet-Prop : Prop (l1 ⊔ l3 ⊔ l4)
    inclusion-Finitely-Graded-Subposet-Prop =
      Π-Prop
        ( Fin (succ-ℕ k))
        ( λ i →
          Π-Prop
            ( face-Finitely-Graded-Poset X i)
            ( λ x → hom-Prop (S x) (T x)))

    inclusion-Finitely-Graded-Subposet : UU (l1 ⊔ l3 ⊔ l4)
    inclusion-Finitely-Graded-Subposet =
      type-Prop inclusion-Finitely-Graded-Subposet-Prop

    is-prop-inclusion-Finitely-Graded-Subposet :
      is-prop inclusion-Finitely-Graded-Subposet
    is-prop-inclusion-Finitely-Graded-Subposet =
      is-prop-type-Prop inclusion-Finitely-Graded-Subposet-Prop

  refl-inclusion-Finitely-Graded-Subposet :
    {l3 : Level}
    (S : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l3) →
    inclusion-Finitely-Graded-Subposet S S
  refl-inclusion-Finitely-Graded-Subposet S i x = id

  transitive-inclusion-Finitely-Graded-Subposet :
    {l3 l4 l5 : Level}
    (S : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l3)
    (T : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l4)
    (U : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l5) →
    inclusion-Finitely-Graded-Subposet T U →
    inclusion-Finitely-Graded-Subposet S T →
    inclusion-Finitely-Graded-Subposet S U
  transitive-inclusion-Finitely-Graded-Subposet S T U g f i x =
    (g i x) ∘ (f i x)

  Finitely-Graded-subposet-Preorder :
    (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
  pr1 (Finitely-Graded-subposet-Preorder l) =
    {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l
  pr1 (pr2 (Finitely-Graded-subposet-Preorder l)) =
    inclusion-Finitely-Graded-Subposet-Prop
  pr1 (pr2 (pr2 (Finitely-Graded-subposet-Preorder l))) =
    refl-inclusion-Finitely-Graded-Subposet
  pr2 (pr2 (pr2 (Finitely-Graded-subposet-Preorder l))) =
    transitive-inclusion-Finitely-Graded-Subposet
```

### Chains in finitely graded posets

```agda
module _
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    {l3 : Level}
    (S : {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l3)
    where

    is-chain-Finitely-Graded-Subposet-Prop : Prop (l1 ⊔ l2 ⊔ l3)
    is-chain-Finitely-Graded-Subposet-Prop =
      is-total-Poset-Prop (poset-Finitely-Graded-Subposet X S)

    is-chain-Finitely-Graded-Subposet : UU (l1 ⊔ l2 ⊔ l3)
    is-chain-Finitely-Graded-Subposet =
      type-Prop is-chain-Finitely-Graded-Subposet-Prop

    is-prop-is-chain-Finitely-Graded-Subposet :
      is-prop is-chain-Finitely-Graded-Subposet
    is-prop-is-chain-Finitely-Graded-Subposet =
      is-prop-type-Prop is-chain-Finitely-Graded-Subposet-Prop

  chain-Finitely-Graded-Poset : (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l)
  chain-Finitely-Graded-Poset l = Σ _ (is-chain-Finitely-Graded-Subposet {l})

  module _
    {l : Level} (C : chain-Finitely-Graded-Poset l)
    where

    subtype-chain-Finitely-Graded-Poset :
      {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l
    subtype-chain-Finitely-Graded-Poset = pr1 C

module _
  {l1 l2 l3 l4 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  (C : chain-Finitely-Graded-Poset X l3) (D : chain-Finitely-Graded-Poset X l4)
  where

  inclusion-chain-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l3 ⊔ l4)
  inclusion-chain-Finitely-Graded-Poset-Prop =
    inclusion-Finitely-Graded-Subposet-Prop X
      ( subtype-chain-Finitely-Graded-Poset X C)
      ( subtype-chain-Finitely-Graded-Poset X D)

  inclusion-chain-Finitely-Graded-Poset : UU (l1 ⊔ l3 ⊔ l4)
  inclusion-chain-Finitely-Graded-Poset =
    inclusion-Finitely-Graded-Subposet X
      ( subtype-chain-Finitely-Graded-Poset X C)
      ( subtype-chain-Finitely-Graded-Poset X D)

  is-prop-inclusion-chain-Finitely-Graded-Poset :
    is-prop inclusion-chain-Finitely-Graded-Poset
  is-prop-inclusion-chain-Finitely-Graded-Poset =
    is-prop-inclusion-Finitely-Graded-Subposet X
      ( subtype-chain-Finitely-Graded-Poset X C)
      ( subtype-chain-Finitely-Graded-Poset X D)
```

### Maximal chains in preorders

```agda
module _
  {l1 l2 : Level} {k : ℕ} (X : Finitely-Graded-Poset l1 l2 k)
  where

  module _
    {l3 : Level} (C : chain-Finitely-Graded-Poset X l3)
    where

    is-maximal-chain-Finitely-Graded-Poset-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3)
    is-maximal-chain-Finitely-Graded-Poset-Prop =
      Π-Prop
        ( chain-Finitely-Graded-Poset X l3)
        ( λ D → inclusion-chain-Finitely-Graded-Poset-Prop X D C)

    is-maximal-chain-Finitely-Graded-Poset : UU (l1 ⊔ l2 ⊔ lsuc l3)
    is-maximal-chain-Finitely-Graded-Poset =
      type-Prop is-maximal-chain-Finitely-Graded-Poset-Prop

    is-prop-is-maximal-chain-Finitely-Graded-Poset :
      is-prop is-maximal-chain-Finitely-Graded-Poset
    is-prop-is-maximal-chain-Finitely-Graded-Poset =
      is-prop-type-Prop is-maximal-chain-Finitely-Graded-Poset-Prop

  maximal-chain-Finitely-Graded-Poset :
    (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l)
  maximal-chain-Finitely-Graded-Poset l =
    Σ _ (is-maximal-chain-Finitely-Graded-Poset {l})

  module _
    {l3 : Level} (C : maximal-chain-Finitely-Graded-Poset l3)
    where

    chain-maximal-chain-Finitely-Graded-Poset :
      chain-Finitely-Graded-Poset X l3
    chain-maximal-chain-Finitely-Graded-Poset = pr1 C

    is-maximal-chain-maximal-chain-Finitely-Graded-Poset :
      is-maximal-chain-Finitely-Graded-Poset
        chain-maximal-chain-Finitely-Graded-Poset
    is-maximal-chain-maximal-chain-Finitely-Graded-Poset = pr2 C

    subtype-maximal-chain-Finitely-Graded-Poset :
      {i : Fin (succ-ℕ k)} → face-Finitely-Graded-Poset X i → Prop l3
    subtype-maximal-chain-Finitely-Graded-Poset =
      subtype-chain-Finitely-Graded-Poset X
        chain-maximal-chain-Finitely-Graded-Poset
```

repository: UniMath/agda-unimath

gha_language: Agda

repo_name: UniMath/agda-unimath


text:
---
layout: page
title: Media
---

[IC Ph.D. student Katie Cunningham receives NSF fellowship](https://www.cc.gatech.edu/news/589186/ic-phd-student-katie-cunningham-receives-nsf-fellowship). David Mitchell, Georgia Tech College of Computing News. March 23, 2017.

# Articles profiling the CSin3 program:
*(formerly CSIT-In-3)*

[Students on Computer Science Fast Track](http://edsource.org/2014/fast-track-to-a-career-in-computer-science/66294#.U_zTJoUoyu6). Michelle Maitre, EdSource. Aug 14, 2014.

[Uber Hails Salinas Student for Internship](http://www.thecalifornian.com/story/news/education/2015/03/18/uber-hails-salinas-student-internship/24994539/). Roberto M. Robledo, The Californian. March 18, 2015.

[From Fields to Code, College Program Helps Farmworkers Make the Leap](http://ww2.kqed.org/news/2014/03/20/from-fields-to-computer-science/). Ana Tintocalis and Jeremy Raff, KQED (NPR station). March 21, 2014.

# Articles describing CSU Monterey Bay and Hartnell College's Innovation Award grant:

[California State University Monterey Bay is double winner in innovation](http://www.cafwd.org/reporting/entry/california-state-university-monterey-bay-is-double-winner-in-innovation). Ed Coghlan, CAFWD. March 30, 2015.

license: MIT

branch_name: refs/heads/master

extension: md

gha_language: CSS

license_type: permissive


text:
---
name: New Trigger / Event Source
about: Need to run a workflow on a specific event, like every time a new PR is opened
  on Github? Request it here!
title: "[TRIGGER]"
labels: enhancement, good first issue, help wanted, trigger / source
assignees: ''

---

**Describe the event source. What app is this for, and what event does the trigger correspond to?**

**Please provide a link to the relevant API docs for the specific service / operation this trigger is tied to.**

gha_license_id: MIT


text:
### [CVE-2007-6750](https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2007-6750)
![](https://img.shields.io/static/v1?label=Product&message=n%2Fa&color=blue)
![](https://img.shields.io/static/v1?label=Version&message=n%2Fa&color=blue)
![](https://img.shields.io/static/v1?label=Vulnerability&message=n%2Fa&color=brighgreen)

### Description

The Apache HTTP Server 1.x and 2.x allows remote attackers to cause a denial of service (daemon outage) via partial HTTP requests, as demonstrated by Slowloris, related to the lack of the mod_reqtimeout module in versions before 2.2.15.

### POC

#### Reference
No PoCs from references.

#### Github
- https://github.com/3vil-Tux/Pentesting-Resources
- https://github.com/ARPSyndicate/cvemon
- https://github.com/Aledangelo/THM_Kiba_Writeup
- https://github.com/Brindamour76/THM---PickleRick
- https://github.com/DButter/whitehat_public
- https://github.com/Dokukin1/Metasploitable
- https://github.com/Drew-Alleman/PeztioQ2
- https://github.com/Eutectico/Steel-Mountain
- https://github.com/GiJ03/ReconScan
- https://github.com/Iknowmyname/Nmap-Scans-M2
- https://github.com/MrFrozenPepe/Pentest-Cheetsheet
- https://github.com/NikulinMS/13-01-hw
- https://github.com/PierreChrd/py-projet-tut
- https://github.com/RoliSoft/ReconScan
- https://github.com/SebSundin/THM-Nmap
- https://github.com/SecureAxom/strike
- https://github.com/SexyBeast233/SecBooks
- https://github.com/Zhivarev/13-01-hw
- https://github.com/adamziaja/vulnerability-check
- https://github.com/binglansky/Slowloris-DOS-Attack
- https://github.com/bioly230/THM_Skynet
- https://github.com/giusepperuggiero96/Network-Security-2021
- https://github.com/h0ussni/pwnloris
- https://github.com/issdp/test
- https://github.com/kasem545/vulnsearch
- https://github.com/le37/slowloris
- https://github.com/marcocastro100/Intrusion_Detection_System-Python
- https://github.com/matoweb/Enumeration-Script
- https://github.com/murilofurlan/trabalho-seguranca-redes
- https://github.com/vshaliii/Basic-Pentesting-1-Vulnhub-Walkthrough
- https://github.com/vshaliii/Basic-Pentesting-2-Vulnhub-Walkthrough
- https://github.com/vshaliii/Cengbox1-Vulnhub-walkthrough
- https://github.com/vshaliii/DC-3-Vulnhub-Walkthrough
- https://github.com/vshaliii/FristiLeaks-Vulnhub-Walkthrough
- https://github.com/vshaliii/Investigator_1-vulnhub-writeup
- https://github.com/xxehacker/strike
- https://github.com/zzzWTF/db-13-01

repository: trickest/cve

branch_name: refs/heads/main

gha_language: HTML

repo_name: trickest/cve


text:
# DemoBank

## The assignment

- Create a new http client for the mythical "[Demo Bank](https://verify-demo-bank.herokuapp.com/)" that we have setup
- Create a public repository for the project on GitHub. When you are done, share the repository link with us
- http client should be created as a gem, we can easily install and use it.

## Grading

We feel this work sample is a great way to measure many things, only one of which is your ability to develop software. We will be looking at the following when evaluating your work sample:

- Ability to follow specific instructions
- Ability to follow existing software patterns
- Thoroughness
- Comfort working with the complete development stack (version control, test frameworks, etc...)

## Specification

We expect your library to have following methods:

- `login` - accepts `credentials` in the form of an email and a password. It returns a Boolean depending on the login result. Method should not take more than **20 seconds** to return a result.
- `accounts` - returns the list of bank accounts in the following format:

```ruby
[
  { type: :current, balance: 100, currency: 'USD' }
]
```

Balance should be represented as an integer in the smallest currency units. For example, $10 USD balance is represented as 1000 (i.e. 1000 cents).

We expect you to build a pure http client, without resorting to the use of a browser automation solution (e.g. Capybara, Puppeteer, PhantomJS, etc).

## Installation

Add this line to your application's Gemfile:

```ruby
gem 'demo_bank'
```

And then execute:

    $ bundle

Or install it yourself as:

    $ gem install demo_bank

## Usage

```ruby
# create a client to interact with DemoBank
client = DemoBank::Client.new

# login with you credentials
client.login(email, password)

# get accounts list
client.accounts
```

## Development

After checking out the repo, run `bin/setup` to install dependencies. Then, run `rake spec` to run the tests. You can also run `bin/console` for an interactive prompt that will allow you to experiment.

To install this gem onto your local machine, run `bundle exec rake install`. To release a new version, update the version number in `version.rb`, and then run `bundle exec rake release`, which will create a git tag for the version, push git commits and tags, and push the `.gem` file to [rubygems.org](https://rubygems.org).

## Contributing

Bug reports and pull requests are welcome on GitHub at https://github.com/vasiliqa/demo_bank.

## License

The gem is available as open source under the terms of the [MIT License](https://opensource.org/licenses/MIT).


text:
# _buttons.scss
_File includes mixins which helps create consistently styled buttons_

### List of content:

- [Mixin button-variant](#mixin-button-variant) (bootstrap 4.0.0)
- [Mixin button-outline-variant](#mixin-button-outline-variant) (bootstrap 4.0.0)
- [Mixin button-size](#mixin-button-size) (bootstrap 4.0.0)

### Default variables
_Default variables which are required in mixins located in file. They are set with most common values._

```scss
$color-black: #242222 !default;
$color-white: #fff !default;
$enable-rounded: false !default;
$btn-focus-width: 2px !default;
$enable-shadows: false !default;
$btn-active-box-shadow: inset 0 3px 5px rgba($color-black, .125) !default;
$btn-box-shadow: inset 0 1px 0 rgba($color-white, .15), 0 1px 1px rgba($color-black, .075) !default;
```

## Mixin button-variant

### Description
_Mixin which helps to create button with specified border and background color when it's hovered_

### Parameters
- `$background` - defines button's text and background color (**required**)
- `$border` - defines button's border color (**required**)
- `$hover-background` - defines button's text and background color when hovered (**default `darken($background, 7.5%)`**)
- `$hover-border` - defines button's border color when hovered (**default `darken($border, 10%)`**)
- `$active-background` - defines button's text and background color when active `$end-color` (**default `darken($background, 10%)`**)
- `$active-border` - defines button's border color when active (**default `darken($border, 12.5%)`**)

### Usage:
Assign $color-red as background color and $color-red-dark as border color of button.

```scss
.exampleGradient {
    @include button-variant($color-red, $color-red-dark);
}
```

## Mixin button-outline-variant

### Description
_Mixin which helps to create button with specified border and background color when it's hovered_

### Parameters
- `$color` - defines button's text and border color (**required**)
- `$color-hover:` - defines button's color when hovered (**default `color-yiq($color)`**)
- `$active-background` - defines button's color when active (**default `$color`**)
- `$active-border` - defines button's border when active (**default `$color`**)

### Usage:
Assign $color-red as button's text and border color and $color-red-dark as border color while active.

```scss
.exampleSizedButton {
    @include button-outline-variant($color-red, $active-border: $color-red-dark);
}
```

## Mixin button-size

### Description
_Mixin which helps to keep consistent size of button_

### Parameters
- `$padding-y` - defines vertical padding of button (**required**)
- `$padding-x` - defines horizontal padding of button (**required**)
- `$font-size` - defines font size of button (**required**)
- `$line-height` - defines line height of button (**required**)
- `$border-radius` - defines border radius properties of button (**required**)

### Usage:
Assigned button with 10px of top and bottom padding, 20px of right and left padding, 16px font size, 20px line height
 and 5px border-radius

```scss
.exampleSizedButton {
    @include button-size(10px, 20px, 16px, 20px, 5px);
}
```

branch_name: refs/heads/develop


text:
Dynamic Tandem Calendar
=========

Let's say:

- Your organization has a [Tandem](https://www.tandemcal.com/) calendar.
- You'd like to include this calendar view in a website that you manage.
- This website that you manage uses a CMS that does not allow you to embed script tags.
- You'd still like to have your Tandem calendar automatically scoped to the current month and year and don't want to manually update the calendar's query string parameters.

If the above describes your situation, the dynamic-tandem-calendar script is for you.

### Usage

Given your predicament, one thing you might do is host a basic html page externally (on an AWS S3 bucket configured for public website hosting, for example) that consumes this script, and then iframe that external site into a page managed by your CMS.

First, create a directory and make an `index.html` (or some kind of `.html`).

Move `dist/dynamic-tandem-calendar.min.js` and `dist/dynamic-tandem-calendar.map.js` into the above directory.

Construct your `.html` file to look something like this:

```html
<html>
	<head>
		<meta charset="utf-8">
		<title>My Org's Monthly Calendar</title>
		<script src="./dynamic-tandem-calendar.min.js"></script>
	</head>
	<body onload="setIframe('tandemcal-subdomain', 'Your Organization Name', 'Numerical Filter Code', 'Desired View: year, month, week, day, or list', 'my-monthly-cal')">
		<div id="my-monthly-cal">
		</div>
	</body>
</html>
```

Feel free to use inline styling to size and style the containing div in the body according to whatever will look best when iframed into your CMS-managed website.

Once you're satisfied with the look, feel free to deploy the above html, along with `dynamic-tandem-calendar.min.js` and `dynamic-tandem-calendar.map.js` to your external location of choice.

### Contributing

If you'd like to contribute, make sure to lint (via `npm test`) and compile (via `npm run build`) before submitting a pull request.

### Real World Usage

- [Mark Twain Elementary PTSA - Home Page](http://twainptsa.org/Home) (weekly calendar view)
- [Mark Twain Elementary PTSA - Monthly Calendar](http://twainptsa.org/Page/Calendar/Calendar)

repository: TheMetalCode/dynamic-tandem-calendar

repo_name: TheMetalCode/dynamic-tandem-calendar


text:
# Real Time Tone Analysis Lab

Welcome to our (abbreviated) 'Real Time Tone Analysis' lab. This workshop was designed to help immerse you in Bluemix, Watson, and Node.js ... to offer a taste of life developing in the cloud. Since we only have a limited amount of time, we are going to just cover the highlights.

## Goals

The following are our goals for you, the developer, to achieve by the end of this workshop:

1. Understand the workflow for Bluemix/Cloud Foundry
2. Experience Node.js development in the Cloud
3. Create and utilize cognitive, natural language services

## Provision a Watson Service

1. Go to the IBM Bluemix catalog and find the [Watson Speech to Text service][stt_service_url]

2. Set the configurations as follows:
	* Service name: Name it `rtt-speech-to-text`
	* Credentials name: Name them `rtt-speech-to-text-creds`
	* Space: Select the space where you want to host your app
	* App: Choose the "Leave unbound" option

3. Create the service

4. Once you are brought to the service console, navigate to the Service Credentials tab and copy the credentials you created. These will be needed in the next step.

## Creating the App Locally

We're going to begin with a basic app that utilizes speech-to-text. We'll make the app run locally on our machines first.

1. Start with the code in the [1 Hour Lab folder](https://github.com/IBM-Bluemix/real-time-tone-analysis/tree/master/WORKSHOP/1_HOUR_LAB) of the GitHub repo.

2. Open up the [`vcap-local.json`](./vcap-local.json) file and replace the credentials with the ones you just created.

3. Now go ahead and install the packages we need for the hello world app

	```bash
	$ npm install
	```

	This step starts off by downloading [npm packages](npm_url) for our server app, then proceeds to download [bower packages](bower_url) that [gulp.js](gulp_url) uses to extract necessary dependencies for our front end.

4. Now let's start the app up

	```bash
	$ npm start
	```
	Check out the running local instance in your browser

## Deploying to Bluemix

1. Open up your [`manifest.yml`](./manifest.yml) file and change the `host` paramater to something unique.

  The host you choose will determinate the subdomain of your application's URL:  `<host>.mybluemix.net`

2. Log in to Bluemix using the cf command line interface and then let's deploy our app

	```bash
	$ cf login -a https://api.ng.bluemix.net
	$ cf push
	```

3. While our app is deploying, let's check the logs to make sure everything is going smoothly. We can do this in several ways:
	* Navigate to the 'Logs' section in your app's dashboard in the Bluemix UI
	* Get the logs using the CF CLI

	```bash
	$ cf logs realtime-tone --recent
	```

Once your app has deployed, hit your app's URL and make sure it's up and running.

## Adding the Tone Analyzer

At the beginning of the lab, we added and bound a service through the Bluemix UI. However, we can do the same thing quicker using the CF CLI. Let's walk through how we do this with the [Tone Analyzer service][ta_url].

1. Create the Tone Analyzer service in Bluemix

  ```bash
  $ cf create-service tone_analyzer standard rtt-tone-analyzer
  ```

2. Bind the tone analyzer service instance to the `realtime-tone` app

  ```bash
  $ cf bind-service realtime-tone rtt-tone-analyzer
  ```

3. We need to add and update some files in order to be able to use this new service. Let's run a special gulp command to do this for us.

  ```bash
  $ gulp lightspeed
  ```

4. Let's grab our app's environment variables and plug them back into [`vcap-local.json`](./vcap-local.json)

  ```bash
  $ cf env realtime-tone
  ```

5. If we check [`bower.json`](./bower.json), it looks like some new front end requirements are needed, so we'll install them and proceed to test the app locally

  ```bash
  $ npm install
  $ npm start
  ```

6. Looks good to me! Push it back up to Bluemix now

  ```bash
  $ cf push
  ```

Voila! We have finished creating our realtime-tone app and you now have your very own version running on Bluemix.

<!--Links-->
[stt_service_url]: https://console.ng.bluemix.net/catalog/services/speech-to-text
[npm_url]: https://www.npmjs.com/
[bower_url]: http://bower.io/
[gulp_url]: http://gulpjs.com/
[ta_url]: https://www.ibm.com/smarterplanet/us/en/ibmwatson/developercloud/tone-analyzer.html


text:
---
title: 'No @font-face Syntax will ever be Bulletproof, Nor Should It Be.'
author: Zach Leatherman
layout: post
permalink: /retire-bulletproof-syntax/
categories:
  - font-loading
tags:
  - font-loading
  - highlight
---

_Originally posted as [No @font-face Syntax will ever be Bulletproof, Nor Should It Be](http://calendar.perfplanet.com/2016/no-font-face-bulletproof-syntax/) on the [perfplanet.com 2016 Performance Calendar](http://calendar.perfplanet.com/2016/)._

---

When you’ve been in the web development game long enough, you see patterns repeat themselves. It wasn’t all that long ago that developers attempted the Sisyphean task of making all  experiences identical for every user independent of their web browser or device’s technical capability. We’ve since learned to shed those shackles in pursuit of something far better: reach.

But even after this shift occurred, we carried the baggage of our old ways forward with web fonts. We described our @font-face syntax with one of the heaviest-duty adjectives available: Bulletproof. This word almost became synonymous with @font-face syntax. You see it everywhere:

* [Bulletproof @font-face Syntax (2009)](https://www.paulirish.com/2009/bulletproof-font-face-implementation-syntax/)
* [The New Bulletproof @font-face Syntax (2011)](http://blog.fontspring.com/2011/02/the-new-bulletproof-font-face-syntax/)
* [Further Hardening of the Bulletproof @font-face Syntax (2011)](http://blog.fontspring.com/2011/02/further-hardening-of-the-bulletproof-syntax/), with “Extra Bulletproofiness” 😀
* [How to Bulletproof @font-face Web Fonts (2011)](http://sixrevisions.com/css/font-face-web-fonts-issues/)
* [Bulletproof Icon Fonts (2014)](https://www.filamentgroup.com/lab/bulletproof_icon_fonts.html) (eek, I wrote this one, see addendum below)

The web font world has changed. It’s time to move the chains forward. Given that web fonts for readable content fall back to system fonts when formats are not supported, it’s ok to be progressive here. Here’s the modern @font-face syntax I’d recommend:

```css/2/-1
@font-face {
  font-family: Open Sans;
  src: url(opensans.woff2) format('woff2'),
       url(opensans.woff) format('woff');
}
```

Pretty simple, right? Just two formats. Much simpler than what we were using before:

```css/-1/2,3,5,6
@font-face {
  font-family: Open Sans;
  src: url('opensans.eot');
  src: url('opensans.eot?#iefix') format('embedded-opentype'),
       url('opensans.woff') format('woff'),
       url('opensans.ttf')  format('truetype'),
       url('opensans.svg#svgFontName') format('svg');
}
```

We’ve eliminated the [Embedded OpenType (EOT) format](http://caniuse.com/#feat=eot) (supported only by Internet Explorer and is the format served to IE versions up to 11) which required a strange double `src` declaration to workaround a syntax bug. [Bram Stein](https://twitter.com/bram_stein), renowned web font performance expert, notes that while EOT formats _can_ be compressed they are often served uncompressed, which is less than optimal given that newer WOFF files include compression by default.

We’ve eliminated the standalone [TrueType/OpenType format](http://caniuse.com/#feat=ttf) because most web browsers support both WOFF and \[True\|Open\]Type. It’s also worth noting that WOFF is just a container format—it adds a wrapper around existing TrueType/OpenType files.

Most importantly, we’ve eliminated the [SVG font format](http://caniuse.com/#feat=svg-fonts). This archaic format is no longer necessary and using it over better formats like WOFF can be harmful. In fact, Chrome took the unusual step of removing SVG font format support from their web browser (with the exception of older Windows versions). How often do things get removed from the web platform? Rarely! You can read more about the history of issues with SVG fonts at [@scottjehl’s Device Bugs repository](https://github.com/scottjehl/Device-Bugs/issues/43).

So, that leaves us with only two font formats: WOFF2 and WOFF. The ordering here is very important: WOFF2 and then WOFF.

To summarize, here is a list of browsers we’ve relegated to use system fonts with this reduced format syntax:

* IE 8
* Firefox 3.5
* Chrome 4
* Safari 3 through 5
* Opera 10.1
* Mobile Safari (iOS) 3.2 through 4.3
* Android 2.2 through 4.3

Android is perhaps the most contentious on this list: as of writing these operating system versions [make up about 16.4% of Android usage](https://developer.android.com/about/dashboards/index.html). This does not count users of these operating systems that have installed Chrome on their devices manually—we’re specifically talking about users of the Android Browser here.

But don’t cry for these users—content will still be readable.

Simplified syntax is better for code health, cognitive load, and general software maintenance. Decreasing the number of formats also decreases the possibility that developers will list their font formats in the `src` attribute out of order. Remember that browsers use the first format they find that works—so if you don’t order them correctly the browser could waste resources (or render poorly) with a less-than optimal format.

Decreasing the number of font formats also simplifies the self-hosting your web fonts. Self hosting can allow more advanced and fine-grained control over how your web fonts are loaded to achieve maximum rendering performance[1]. I’ve written a slew of [web font loading articles that showcase advanced font loading techniques](https://www.zachleat.com/web/comprehensive-webfonts/), and the more advanced two-stage loading methods are easier to implement when self hosting.

*[1] Act now and buy two bottles of web font loading drink powder mix to achieve maximum rendering performance and the third bottle is free.*

## Addendum: Okay, but what about icon fonts?

I did contribute to the Bulletproof @font-face phenomenon. However, a closer read of [the icon font article I wrote](https://www.filamentgroup.com/lab/bulletproof_icon_fonts.html) reveals no discussion of @font-face syntax. Said differently: a bulletproof @font-face syntax won’t save your icon fonts. Just because the font format *can* be read and interpreted by an older web browser doesn’t mean that it won’t have loading issues, FOUT fallback inconsistencies, or that glyphs will be misread by screen readers. **Unlike content fonts, icon fonts do not use progressive enhancement by default.** They need additional care: to be paired with a font loading strategy and with default screen-reader-accessible fallback text. I’d recommend that you [read the article](https://www.filamentgroup.com/lab/bulletproof_icon_fonts.html) to learn more about the myriad of issues with icon fonts.

Or, you could look toward the future and use SVG icons instead.

## Addendum: Thank You

A big thank you to [Bram Stein](https://twitter.com/bram_stein) for reviewing and providing feedback on this post before publication.


text:
---
title:  "Mocking Angular Dependencies in Unit Tests"
date:   2016-02-29 15:12:00
category: til
tags: [angular, testing, unit-test, jasmine]
---

TIL how to properly mock angular dependencies in Unit Tests using the Jasmine test framework.

[A wise man once said...][wise]{:target="_blank"}

> Angular was written with testability in mind

This was something I have kept in the back of my head since I started working with Angular a little over a year ago, and have honestly struggled to understand... and today I was finally struck with clarity: __angular is incredibly easy to unit test__, thanks to [`dependency injection`][dependency]{:target="_blank"} and the ease with which dependencies can be `mocked`.

I won't go in depth in to `dependency injection` here (maybe another day...) but the fact that angular leverages this pattern throughout construction of its controllers and services makes mocking and testing units of code a breeze.

If a unit under test relies on a method call to an injected dependency, the [jasmine test framework makes it easy to mock and call fake methods][jasmine]{:target="_blank"} whenever the dependency is needed, allowing the tester to focus on the unit under test instead of first making sure a particular dependency is functioning as expected.

Note: testing with realistic responses from the backend should be reserved for **integration** tests, and should not be of concern at the *unit* level.

__Example:__

I just spent the last week testing changes to a controller that leverages a service to request data from a paged API endpoint for our app. The controller  makes a call to the service on initial load to request a default set of data.

Initially, my tests all looked something like this:

{%highlight javascript%}

describe('test $scope.manipulateMembers', function(){
	beforeEach(function(){
		var data = load(data_from_fixture); //takes a long time
		$httpBackend.expectGET('default/api/request').respond(200, data);
	});
	it('should update $scope.loaded to be true', function(){
		$rootScope.$digest();
		$httpBackend.flush(); //takes a while
		//assertions begin here
		...
	});
});

{%endhighlight%}

Each describe block started with an expectation for a request to the backend for the default set of data. While this is good to check in an *integration* scenario, __the interaction between the backend and the controller should be irrelevant when testing a unit of code in the controller.__ The unit should function the same whether the backend request is made or not.

Furthermore, the data we were returning each time was quite large (to emulate a realistic set of data being returned from the backend) and was re-loaded from a fixture before each test. __I was performing an integration test with the backend for each of my unit tests.__

Additionally, asserting that the backend was called correctly when the controller was loaded and flushing the backend for each unit added a TON of time to each test: __tests took upwards of 2000ms a piece__, and often would cause our karma server to disconnect in the middle of a test run because tests were running so slow.

Luckily, I realized this didn't need to be the case, as I figured out how to mock the default call to the service that interfaced with the backend by using jasmine `spys` and `mocks`.

{%highlight javascript%}
describe('test $scope.manipulateMembers', function(){

	beforeEach(function(){
		spyOn(serviceName, 'serviceMethod').and.callFake(function(){
			var deferred = $q.defer();
			deferred.resolve(['some', 'fake', 'data']);
			return deferred.promise;
		});
	});
	it('should update $scope.loaded to be true', function(){
		$scope.$digest();
		expect($scope.loaded).toBe(true);
	});
});

{%endhighlight%}

By ___mocking___ the default call to the backend service via a jasmine spy, we can forgo dealing with the backend request expectations + loading realistic data from a fixture on initial digest.

__Test execution time was reduced from over 2000ms per test, to 10ms per test.__

This type of mocking is possible with __ANY__ service that may be necessary for testing a particular unit of code in my controller.

This was a truly enlightening experience overall, and really helped solidify my understand of that timeless phrase **angular was written with testability in mind** as well as the differences between `unit` and `integration` tests on the frontEnd.

I hope you feel enlightened as well.

Happy Leap Day!

[wise]: https://docs.angularjs.org/guide/unit-testing#with-great-power-comes-great-responsibility
[dependency]: https://docs.angularjs.org/guide/di
[jasmine]: http://jasmine.github.io/2.0/introduction.html#section-Spies


text:
# uSync
`Install-Package uSync` [nuget](https://www.nuget.org/packages/uSync/)

- In developer section of Umbraco, click on the uSync backoffice and select config data. set to Manual Sync.
- Restart application.

repository: kikkoi/UmbracoSetup

repo_name: kikkoi/UmbracoSetup


text:
# How to Code: Simple Data

## Table of Contents

* [Music Technology Foundations](#how-to-code-simple-data)
  * [Disclaimer](#disclaimer)
  * [Notes](#notes)
  * [Resources](#resources)

## Disclaimer

Everything in this file is derived from going through [Music Technology Foundations](https://www.edx.org/course/music-technology-foundations) and is my own work. It is meant for revision and reference purposes and I take no responsibilities for any damaged caused by the use of it (see [LICENSE](https://github.com/honmanyau/study-notes/blob/master/LICENSE.md)).

## Notes

### 1: Introduction to sound

#### What is music technology?

* Music technology is not limited to computers and electronics—using tools to make sound for music purposes is music technology.
* The ability and ease to record music nowadays has democratised access to, and the production of, music.

#### Theremin demonstration

* Leon Theremin
* Theremin produces sound via heterodyning.

Uwah, Clara Rockmore is amazing [Youtube playlist](https://www.youtube.com/watch?list=PLEiTaey66qmD17v-oJ7aOTbfgADGd_Rgc&v=pSzTPGlNa5U).

#### Sound recording

Distortion—sound too loud for the recording device and distorts. Try different angles and/or pulling the receiver/microphone further away from the sound source.

#### Music revolutionaries: Leon Scott, Charles Cros & Thomas Edison

* Leon Scott
* Phonautograph—he didn't actually invent a way for converting them into sound

* Charles Cros
* Invented the process of colour photography and paleophone

* Thomas Edison
* Invented the phonograph

* Emile Berliner
* Invented microphone and format of the disc

* Recording became electric in the 1920s
* Emergence of hi-fi in 1960s

#### Perception of sound

* Cocktail party effect is interesting!
* Acoustic-auditory; quantity-quality

#### Audible illusion experiment

## Resources

* [Sound Cloud](https://soundcloud.com)
* Music technology timeline, WEEK 1: Introduction to sound > Music technology timeline > Music technology timeline
*

path: /Course Notes/Music Technology Foundations.md

filename: Music Technology Foundations.md


text:
# Adopticon
Prototype tooling to aid in the identification and resolution of defects in AdoptOpenJDK's build and test jobs.

## Contents
1) About
2) Setup
3) Features

## 1) About

The point of this repo is to contain a number of internal-only tools to aid in defect identification and resolution.

These tools should be stored in separate folders so they can be moved or modified easily, with the exception of shared
functionality which should be stored in the relevant file in the include directory (TODO latter).

Each tool should be linked in [index.php](./index.php) for easy access.

## 2) Setup

To set this up on a new machine, here are the linux instructions:

- apt-get install apache2
- apt-get install php libapache2-mod-php
- cd /var/www/html
- rm ./*
- git clone \<This repo\> .

## 3) Features
- [Nightly Failures Summary](./nightly_failures_summary/index.php)

repository: adamfarley/adopticon

repo_name: adamfarley/adopticon


text:
---
title: Perc Adapter Errors
date: 2016-05-21T04:59:00+00:00
author: gerryw1389
layout: single
classes: wide
permalink: /2016/05/perc-adapter-errors/
categories:
  - Hardware
  - WindowsServer
tags:
  - Monitoring
---
<!--more-->

### Description:

Inside of Dell Open Manage, you will see “Storage Drive 0: Drive slot sensor for storage” or “Bad PHY Slot 0: Connector 0 Controller 0” in the logs. You will see errors such as “E1810 HDD 0 Fault” on the physical server's LCD display as well, usually with an amber background indicating a “Warning”.

### To Resolve:

1. Get the service tag of the server. [run => cmd => ](https://automationadmin.com/2016/05/command-prompt-overview/) `wmic bios get serialnumber`. Look that up on the Dell website.

2. Once there, you need to update the drivers and firmware for the Perc Adapter. Navigate to the “SAS Raid” section and download the newest one with the word (firmware) and (driver) after it that matches that system specifically.

3. Run those and reboot. Export and clear the Dell logs through Open Manage (OM).

4. Run => `services.msc` => Restart all four DSM Services related to OM.

5. Log back in to OM, if it's still bad, call Dell. There may be battery errors from the reboot. This is because the Perc adapter does a battery test on reboot and if it's bad, then the battery will show to be bad. You will have to resolve the issue through Dell, many times replacing the perc adapter itself resolves the issue. Note that if your sever is under Basic warranty you will have to pay for this, Pro warranty doesn't need to worry.


text:
# ReTwitter Messages App

the app was built for the RoR Project and the intention is to create an app similar to Twitter.
In this app you can create an account, follow people and create message where you can talk about many topics as you wish.

## Images

![screenshot](./app/assets/images/screenshot-1-capstone.png)

## Built and tested With

- Ruby 2.7.0
- Ruby on Rails 6.1.0
- Rspec
- Postgres: >=9.5

## Live Demo of the app

[Click on this link](https://afternoon-beach-90148.herokuapp.com/)

## Video of Demostration

[Click on this link](https://www.loom.com/share/087cf731e6ce433086aa8da1720b5097)

## Setup

Download the repo with this command

`git clone https://github.com/alejandrotoledoweb/rails_capstone_retwitter.git`
`cd rails_casptone_retwitter`

Install the Gems and Dependencies

`bundle install`

Migrate the database and models

`rails db:migrate`
`rails db:seed`

## For the usage

Run the server

`rails server`

Open in the browser `http://localhost:3000/`

## Run the test

Run this command

`rspec`

## Author

👤 **Alejandro Toledo**

- GitHub: [@alejandrotoledoweb](https://github.com/alejandrotoledoweb)
- Twitter: [@alejot](https://twitter.com/alejot)
- LinkedIn: [Alejandro Toledo](https://www.linkedin.com/in/alejandro-toledo-3b444b109/)

## 🤝 Contributing

Contributions, issues and feature requests are welcome!

Feel free to check the [issues page](issues/).

## Show your support

Give a ⭐ if you like this project!

## Acknowledgments

- Project inspired by the work of [Gregoire Vella](https://www.behance.net/gallery/14286087/Twitter-Redesign-of-UI-details)

## 📝 License

This project is [MIT](https://opensource.org/licenses/MIT) licensed.

branch_name: refs/heads/development

gha_language: Ruby


text:
# 701. Insert into a Binary Search Tree

## Description:

Given the root node of a binary search tree (BST) and a value to be inserted into the tree, insert the value into the BST. Return the root node of the BST after the insertion. It is guaranteed that the new value does not exist in the original BST.

Note that there may exist multiple valid ways for the insertion, as long as the tree remains a BST after insertion. You can return any of them.

## Solution:

```c++
/**
 * Definition for a binary tree node.
 * struct TreeNode {
 *     int val;
 *     TreeNode *left;
 *     TreeNode *right;
 *     TreeNode(int x) : val(x), left(NULL), right(NULL) {}
 * };
 */
class Solution {
public:
    TreeNode* insertIntoBST(TreeNode* root, int val) {
        if (!root) {
			TreeNode *node = new TreeNode(val);
			return node;
		}

		if (val < root->val)
			root->left = insertIntoBST(root->left, val);
		else
			root->right = insertIntoBST(root->right, val);

		return root;
    }
};
```

<!-- remark：

-  -->

url: https://raw.githubusercontent.com/eatPorkAndSeePigRun/MyLeetcode/9f6b41d4980c25482a215f2ce3b680dcd5696546/Source/tree/701. Insert into a Binary Search Tree.md

repository: eatPorkAndSeePigRun/MyLeetcode

repo_name: eatPorkAndSeePigRun/MyLeetcode


text:
---
title: "Build On-Demand Videos - YAML Release Pipelines in Azure DevOps"
date: 2019-05-08T00:00:00-05:00
draft: false
---

My Microsoft Build on-demand recording of YAML Release Pipelines in Azure DevOps session, demonstrating our first release of multi-stage YAML CI/CD pipelines in Azure DevOps.

{{< youtube ORy3OeqLZlE >}}

repository: DivineOps/sasha-rosenbaum-site

repo_name: DivineOps/sasha-rosenbaum-site


text:
node-red-contrib-jsonrpc
==============================

Node-RED node for JSON-RPC 2.0 communication. Wraps node-jsonrpc2.

Install
-------

Run the following command in your Node-RED user directory - typically `~/.node-red`

        npm install node-red-contrib-jsonrpc

Example
-----

An example of communicating with ethereum.
```
[{"id":"8b5fb501.4af498","type":"jsonrpc-call","z":"838a7f87.ba911","name":"","method":"eth_sendTransaction","client":"bbdeb946.30bd18","x":330.5,"y":85,"wires":[["b3951.3b65e6b"]]},{"id":"cdef05f.e8692f8","type":"inject","z":"838a7f87.ba911","name":"","topic":"","payload":"{\"from\":\"0x627306090abaB3A6e1400e9345bC60c78a8BEf57\",\"value\":\"0x0de0b6b3a7640000\",\"to\":\"0x05eee23f682718f129719df9d0d0254542c6a10e\"}","payloadType":"json","repeat":"","crontab":"","once":false,"onceDelay":0.1,"x":119.5,"y":61,"wires":[["8b5fb501.4af498"]]},{"id":"b3951.3b65e6b","type":"debug","z":"838a7f87.ba911","name":"","active":true,"tosidebar":true,"console":false,"tostatus":false,"complete":"false","x":520.5,"y":141,"wires":[]},{"id":"bbdeb946.30bd18","type":"jsonrpc-client","z":"","name":"ganache","host":"localhost","port":"7545","connection":"http"}]
```

Acknowledgements
==============================

Uses procesar's fork of the json rpc 2.0 implementation https://github.com/pocesar/node-jsonrpc2.

license: ISC

repository: joeartsea/node-red-contrib-jsonrpc

gha_language: JavaScript

gha_license_id: NOASSERTION

repo_name: joeartsea/node-red-contrib-jsonrpc


text:
# api.python.Bonsai
An api written in python for use managing employees

to install dependencies create a .venv folder andd then run ```pipenv install```

to install the postgres driver run ```pipenv run i_pgdriver```

to start the server, run ```pipenv run start``` at the root directory

## vscode settings ##
to gain import intellisense, add the following to either your local or global settings.json

```json
{
  "python.analysis.extraPaths":["app","app/main"]
}
```

make sure to set the python interpreter in the bottom left of vscode to the virtual environment's installation of python.

repository: ayoyin/REST-API

repo_name: ayoyin/REST-API


text:
# blaseball-api-scala
library for interacting with blaseball.com

mostly isnt here

## use
`sbt publishLocal`

## actual use
```scala
import dev.taylorh.blaseball.api._
import dev.taylorh.blaseball.util._

implicit val api: BlaseballApi = new BlaseballApiCache(BlaseballApiNoCache)

val players = BlaseballUtil.getNonShadowPlayersInLeague(BlaseballConstants.internetBlaseballLeagueId)

val lowe = players.find(_.name == "Lowe Forbes").get
println(lowe)
```
```
Player(b348c037-eefc-4b81-8edd-dfa96188a97e,Lowe Forbes,PlayerAttributes(Set(TRIPLE_THREAT, ELSEWHERE),Set(),Set(),Set()),BaserunningAttributes(1.0076577795404305,0.7376708329124532,0.65778038325191,0.31668496987719963,0.6846554366890226),DefenseAttributes(0.5649882368120599,0.6646997379187309,0.46568263804703275,1.0692973515494772,0.7641772466540312),HittingAttributes(0.5575745289604013,0.5598360608235193,0.29906780048711734,1.1529624468864095,1.0645705544262631,0.7032875904768319,0.29009409249364415,0.001),PitchingAttributes(0.5340845817870057,0.4966827262567918,0.5524452849430901,1.4607113410346162,1.3875668180863707,1.1567138528908278,12),OtherAttributes(false,false,0.40039817421122226,1.0586070350960344,4,Some(Eating fans),Some(2),Some(8),73,27.10321071373309,0),TeamAttributes(a37f9158-7f82-46bc-908c-c9e2dda7c33b,None),Ratings(0.6866326251134355,0.4937555250856056,0.7677566894190615,0.7808852623437675,0,0))
```

## checklist
 - [ ] players
   - [x] stats ~~(i think they added new ones?)~~ they didnt im just forgetful
   - [ ] feed
     - [ ] metadata
     - [x] everything else
   - [ ] items
 - [ ] teams
   - [ ] probably needs restructure
 - [x] league, subleague, division
 - [ ] games
 - [ ] docs

repository: randomtestfive/blaseball-api-scala

repo_name: randomtestfive/blaseball-api-scala


text:
# Project Support
Useful links to get you started

## Text Classification
### Fake News Detection
- [Shu, Kai, et al. "Fake news detection on social media: A data mining perspective." _ACM SIGKDD Explorations Newsletter_ 19.1 (2017): 22-36.](https://dl.acm.org/doi/abs/10.1145/3137597.3137600)
- [Fake News Detection by Learning Convolution Filters through Contextualized Attention](https://github.com/ekagra-ranjan/fake-news-detection-LIAR-pytorch)
- [Yang, Kai-Chou, Timothy Niven, and Hung-Yu Kao. "Fake News Detection as Natural Language Inference." _arXiv preprint arXiv:1907.07347_ (2019).](https://arxiv.org/abs/1907.07347) [(code)](https://github.com/zake7749/WSDM-Cup-2019)

### Sentiment Analysis
- [Rosenthal, Sara, Noura Farra, and Preslav Nakov. "SemEval-2017 task 4: Sentiment analysis in Twitter." _arXiv preprint arXiv:1912.00741_ (2019).](https://arxiv.org/abs/1912.00741)
- [Nakov, Preslav, et al. "SemEval-2016 task 4: Sentiment analysis in Twitter." _arXiv preprint arXiv:1912.01973_ (2019).](https://arxiv.org/abs/1912.01973)
- [Do, Hai Ha, et al. "Deep learning for aspect-based sentiment analysis: a comparative review." _Expert Systems with Applications 118_ (2019): 272-299.](https://www.sciencedirect.com/science/article/pii/S0957417418306456)
- [Sentiment Analysis with PyTorch](https://github.com/radoslawkrolikowski/sentiment-analysis-pytorch)
- [PyTorch Sentiment Analysis](https://github.com/bentrevett/pytorch-sentiment-analysis)

## Question Answering
- [Bauer, Lisa, Yicheng Wang, and Mohit Bansal. "Commonsense for generative multi-hop question answering tasks." _arXiv preprint arXiv:1809.06309_ (2018).](https://arxiv.org/abs/1809.06309) [(code)](https://github.com/yicheng-w/CommonSenseMultiHopQA)
- [Chen, Danqi, et al. "Reading wikipedia to answer open-domain questions." _arXiv preprint arXiv:1704.00051_ (2017).](https://arxiv.org/abs/1704.00051) [(code)](https://github.com/hitvoice/DrQA)

### Chat bots
- [Chatbot Tutorial](https://pytorch.org/tutorials/beginner/chatbot_tutorial.html)
- [pytorch-chatbot](https://github.com/ywk991112/pytorch-chatbot)

### Both QA and Chat Bots
- [Radford, Alec, et al. "Language models are unsupervised multitask learners." _OpenAI Blog_ 1.8 (2019): 9.](https://www.ceid.upatras.gr/webpages/faculty/zaro/teaching/alg-ds/PRESENTATIONS/PAPERS/2019-Radford-et-al_Language-Models-Are-Unsupervised-Multitask-%20Learners.pdf) [(code)](https://github.com/openai/gpt-2)

### Evaluation
- [Zhang, Tianyi, et al. "Bertscore: Evaluating text generation with bert." _arXiv preprint arXiv:1904.09675_ (2019).](https://arxiv.org/abs/1904.09675) [(code)](https://github.com/Tiiiger/bert_score)
- [Chen, Anthony, et al. "Evaluating Question Answering Evaluation." _Proceedings of the 2nd Workshop on Machine Reading for Question Answering._ 2019.](https://www.aclweb.org/anthology/D19-5817/)
- Human evaluation is still the best option

## Sequence Tagging
- [Huang, Zhiheng, Wei Xu, and Kai Yu. "Bidirectional LSTM-CRF models for sequence tagging." _arXiv preprint arXiv:1508.01991_ (2015).](https://arxiv.org/abs/1508.01991)
- Multi-task learning can be an interesting option

## Text Generation
- [Radford, Alec, et al. "Language models are unsupervised multitask learners." _OpenAI Blog_ 1.8 (2019): 9.](https://www.ceid.upatras.gr/webpages/faculty/zaro/teaching/alg-ds/PRESENTATIONS/PAPERS/2019-Radford-et-al_Language-Models-Are-Unsupervised-Multitask-%20Learners.pdf) [(code)](https://github.com/openai/gpt-2)

### Evaluation
- Almost impossible to evaluate automatically
- Human evaluation is still the best option


text:
**Do You Want to Build a Snowman双手简谱** 和五线谱完全对应。

_
Do You Want to Build a Snowman_
是2013年美国一部以电脑动画技术制成的音乐奇幻喜剧和三维电影冰雪奇缘（英语：Frozen）的插曲。
该片取材自安徒生童话故事《冰雪女王》，是第53部迪士尼经典动画长片。克里斯滕·贝尔、伊迪娜·门泽尔、乔纳森·格罗夫和乔什·盖德为主要配音演员。2013年11月27日于美国上映。

该曲描述了安娜和艾莎两姐妹由亲密无间到无奈疏离的心路历程。在MV中，随着安娜的年龄及心境变化，MV镜头在雪地和城堡的场景中切换：纯洁无瑕的雪地象征着她们纯真无忧的童年，而后紧闭的城堡大门与电影情节遥想呼应。

### Do You Want to Build a Snowman歌词：

Anna:
Elsa?
(Knocking: Knock, knock, knock, knock, knock, knock)
Do you wanna build a snowman?
Come on lets go and play
I never see you anymore
Come out the door
It's like you've gone away-
We used to be best buddies
And now we're not
I wish you would tell me why!-
Do you wanna build a snowman?
It doesn't have to be a snowman.
Elsa:
Go away, Anna
Anna:
Okay, bye...
(Knocking)
Do you wanna build a snowman?
Or ride our bikes around the halls
I think some company is overdue
I've started talking to
the pictures on the walls-
(Hang in there, Joan!)
It gets a little lonely
All these empty rooms,
Just watching the hours tick by-
(Tic-Tock, Tic-Tock, Tic-Tock, Tic-Tock, Tic-Tock)
(Orchestral)
Anna:
(Knocking)
Elsa?

Do you wanna build a Snowman?

url: https://raw.githubusercontent.com/Emptyspirit/everyonepiano-music-database/fb8ba03dd9474f049b18d9822c40a395229b7aca/动漫/Do You Want to Build a Snowman钢琴版-冰雪奇缘插曲/README.md


text:
# Dicyclotrichium Xu, Song & Hu, 2005 GENUS

#### Status
ACCEPTED

#### According to
The Catalogue of Life, 3rd January 2011

#### Published in
Journal of the Marine Biological Association of the United Kingdom 85: -. [787-794]

#### Original name
null

### Remarks
null

repository: mdoering/backbone

repo_name: mdoering/backbone


text:
# seq-stream
[![NPM version](https://badge.fury.io/js/seq-stream.svg)](http://badge.fury.io/js/seq-stream) [![Build Status](https://travis-ci.org/villadora/seq-stream.svg?branch=master)](https://travis-ci.org/villadora/seq-stream)

<!--[![Dependency Status](https://gemnasium.com/villadora/seq-stream.svg)](https://gemnasium.com/villadora/seq-stream) -->

Create a stream pipe out a group of readable streams in sequence.

## Install

```bash
$ npm install seq-stream --save
```

## Usage

```js
var seq = require('seq-stream');

var stream = seq(stream1, fs.createReadStream('./data'));

// will pipe to stdout in the order of content in 'straem1', content in './data'
stream.pipe(process.stdout);

```

## Licence

MIT

repository: villadora/seq-stream

repo_name: villadora/seq-stream


text:
# tx.origin misuse
A `Victim` contract identifies caller by `tx.origin` instead of `msg.sender`.
This may allow an external malicious contract to act on behalf of origin user and attack the `Victim` contract.

## Attack Scenario

### Abstract

Bob using `FreeSuperSecuredWalletsFactory` provided by Danny expose funds stored in `FreeSuperSecuredWallet` to attack while using completely separate service `FakeAirdrop` created by Drake that exploits weaknes in `FreeSuperSecuredWallet` inplementation. The key point
is that malicious smart contracts (`FakeAirdrop`) in order exploit weakness in `FreeSuperSecuredWallet` must be called by victim (Bob) itself.

### Full Scenario
Some developer (not necesarily attacker, neither victim)  creates a service `FreeSuperSecuredWalletsFactory` (Danny)
which allows to create wallet just by sending ETH to factory, problem is this wallet uses `tx.origin` for authorization

Some user (future victim) uses this service, send 1 ETH (Let's call him Bob) to `FreeSuperSecuredWalletsFactory`

Now dishonest Drake spot that there is popular service `FreeSuperSecuredWalletsFactory` which has a bug
deploys FakeAirdrop contract with his address as _beneficiary, and `FreeSuperSecuredWalletsFactory` address as *_factory*
And convince Bob to attend the bounty, and contract indeed do Airdrop of some tokens but at the same time calls following code

```javascript
if(listOfWalletsToSteelFrom._wallets(msg.sender)!=address(0)){
	listOfWalletsToSteelFrom._wallets(msg.sender).sendEth(dishonestGuy);
}
```

which drain `FreeSuperSecuredWallet` of a `msg.sender` if particular sender owned one.

## How to reproduce example

Consider using [remix.ethereum.org](https://remix.ethereum.org)

- Deploy `FreeSuperSecuredWalletsFactory`
- Send Ether to `FreeSuperSecuredWalletsFactory` from Victim Account

- Deploy `FakeAirdrop` contract passing as parameters:

  - *_beneficiary*  -  address of attacker

  - *_factory* - address of  `FreeSuperSecuredWalletsFactory`

- Send transaction to `FakeAirdrop`  from Victim Account

In result funds sended to `FreeSuperSecuredWalletsFactory` will be transfered to `_beneficiary`

## Real World Example

[Mist Wallet in version 0.4.0](
https://blog.ethereum.org/2016/06/24/security-alert-smart-contract-wallets-created-in-frontier-are-vulnerable-to-phishing-attacks/)

## Mitigations
Never use `tx.origin` as source of user identity

## External Resources
As you can see unsecured wallet can be drained when you interact with completly unrelated service
For more information look at:
[Solidity: Tx Origin Attacks](https://medium.com/coinmonks/solidity-tx-origin-attacks-58211ad95514) and the [Ethereum Security Alert](https://blog.ethereum.org/2016/06/24/security-alert-smart-contract-wallets-created-in-frontier-are-vulnerable-to-phishing-attacks/).

repository: adamskrodzki/not-so-smart-contracts

repo_name: adamskrodzki/not-so-smart-contracts


text:
# HackBoy 3000
HackBoy 3000 is a solver for the terminal hacking mini-game in the Fallout series of
video games.

This repository includes a command-line version of the tool as well as a version
written for the web. The web version is hosted [here](http://hackboy.sinclairtarget.com).

### Using HackBoy 3000 on the command line
```
$ ruby terminal_hack.rb
```

Available options:
```
$ ruby terminal_hack.rb -v (verbose mode)
```

You can also feed a file containing a list of games into `test_terminal_hack.rb`:
```
$ ruby test_terminal_hack.rb games/games.txt
100 tests completed.
Median attempts to win: 2.5
Average attempts to win: 2.5
Max attempts to win: 5
```

You can also pass the `-v` flag to `test_terminal_hack.rb`.

### Building the web version
Running...
```
$ make
```
...will compile the .coffee and .scss files into .js and .css files and place them
into the `/public` directory.


text:
# Reservoir computing with single dynamical node
In a 2011 article titled ["Information processing using a single dynamical node as complex system"](https://www.nature.com/articles/ncomms1476) L. Appeltant et al. showed that a nonlinear node with delayed feedback, such as a Mackey-Glass oscillator, can be used in lieu of a complex network in the paradigm of reservoir computing. The efficacy of their approach was confirmed through the NARMA10 benchmark: Four NARMA10 samples with length 800 points each, were preprocessed and fed through the single-node reservoir and the reservoir response was used for training and testing. A Normalized Root Mean Square Error (NMRSE) down to 0.12 (with twofold cross-validation) was achieved.

The present repository reproduces this result. It contains the following scripts:
1. The `Narma10_Input.py` script generates a Narma10 file to be used as input for the single-node reservoir. This file contains the multiplexed 'masked' signals which are fed to the Mackey-Glass Oscillator(s). A `Narma10.h5` file that yields the desired cross-validation NMRSE = 0.12 is included. The `Narma10_Input.py` can be used to generate alternate Narma10 files.
2. The `MG_Oscillator.py` runs the Mackey-Glass simulation with the relevant input file. The oscillator response is saved in a file that is then used for training the network.
3. The `Training.py` script uses the Mackey-Glass oscillator response to train the network and calculate the NRMSE.
4. The `Visualization.py` script generates the figures shown here: (a) the response of the reservoir; (b) the fit on the training set and (c) the fit on the test set.
5. The `DynamicalNode_Reservoir.py` is a wrapper for the above scripts--the main program.

## Notes:

### on the Narma10 input
The binary masks used for multiplexing follow the guidance in [this (2014) paper](https://www.nature.com/articles/srep03629) by L. Appeltant et al.

### on the Mackey-Glass solver
The standard form of the Mackey-Glass equation is:

![first eq](https://latex.codecogs.com/gif.latex?\bg_white&space;\large&space;\frac{dx}{dt}&space;=&space;\beta&space;\frac{x(t-\tau)}{1+[x(t-\tau)]^p}-\gamma&space;x(t),\quad\text{with}\quad\gamma,\beta,p>0)

This equation appears in [Appeltant et al. (2011)](https://www.nature.com/articles/ncomms1476) with a different notation:

![second eq](https://latex.codecogs.com/gif.latex?\bg_white&space;\large&space;\dot{X}(t)=&space;-X(t)+\frac{\eta\cdot[X(t-\tau)+\zeta&space;J(t)]}{1+[X(t-\tau)+\zeta&space;J(t)]^p})

where clearly we recover the previous expression for:

![third_eq](https://latex.codecogs.com/gif.latex?\bg_white&space;\large&space;\gamma&space;=1,&space;\beta&space;=&space;\eta,\quad\text{and}&space;\quad&space;x(t-\tau)&space;\rightarrow&space;X(t-\tau)+\zeta&space;J(t))

For the numerical integration of this equation we use the [implicit midpoint method](https://en.wikipedia.org/wiki/Midpoint_method) as described below:

![implicit midpoint](https://latex.codecogs.com/gif.latex?\bg_white&space;\large&space;\Bigl(1+\frac{h}{2}\Bigr)X_{n+1}=&space;\Bigl(1-\frac{h}{2}\Bigr)X_n&space;+\frac{\eta\Bigl[X(t_n+\frac{h}{2}-\tau)+\zeta&space;J(t_n+\frac{h}{2})\Bigr]}{1+\Bigl[X(t_n+\frac{h}{2}-\tau)+\zeta&space;J(t_n+\frac{h}{2})\Bigr]^p})

where _h_ is the timestep. To integrate a Delay Differential Equation (DDE) we need the values of _X_ at the present time _X(t)_ as well as its delayed value _X(t-τ)_. For the implicit midpoint method we actually need _X(tn)_ and _X(tn+h/2-τ)_. Therefore, if _τ-h/2_ is an integral number _N_ of timesteps _h_, viz. if _τ-h/2 = Nh_, then the value of _X(tn+h/2-τ)_ has already been calculated and we can immediately substitute it in the equation above. We choose:

![timestep](https://latex.codecogs.com/gif.latex?\bg_white&space;\large&space;h&space;=&space;\frac{2\tau}{2N+1}\Rightarrow&space;t_n+\frac{h}{2}-\tau&space;=&space;t_n-Nh)

where _N_ represents the number of steps used to resolve the Delay Period _τ_.

### on the Mackey-Glass response

The response of the reservoir along with the input is shown for the normalized time interval [0,100]. The delay τ was chosen τ = 80 such that a transition at t = τ = 80 can be observed in the input signal from the first Narma10 value to the second. Each value from the Narma10 dataset is multiplexed through 400 virtual nodes with temporal distance	ι = τ/400 = 0.2. For an 800-long Narma10 signal the maximum normalized time is 800*80 = 64000.

![fig1](https://github.com/mtzoufras/Reservoir_computing_with_a_single_dynamical_node/blob/master/Reservoir_Response.png?raw=true)

## on training

The fit is shown on the training set (samples 0 and 1).
![fig2](https://github.com/mtzoufras/Reservoir_computing_with_a_single_dynamical_node/blob/master/Train_Dataset.png?raw=true)

The fit is shown on the test set (samples 2 and 3).
![fig3](https://github.com/mtzoufras/Reservoir_computing_with_a_single_dynamical_node/blob/master/Test_Dataset.png?raw=true)

Cross-validation is calculated by swapping the test and training datasets.


text:
Well, my godchild loves 🦄 unicorns 🦄.

So, I built something ...

<img width="320" alt="unicorns" src="https://user-images.githubusercontent.com/5558193/114394780-e0e0d800-9b9b-11eb-916e-9c75c5c803f6.png">

This is a [Next.js](https://nextjs.org/) project bootstrapped with [`create-next-app`](https://github.com/vercel/next.js/tree/canary/packages/create-next-app).

## Getting Started

First, get your API key from [Pixabay](https://pixabay.com/) and add it to your `.env.local` at the root of your project.

```
PIXABAY_API_KEY=YourSuperSecretKey
```

Then, run the development server:

```bash
npm run dev
# or
yarn dev
```

Open [http://localhost:3000](http://localhost:3000) with your browser to see the result.

## Further information

Learn more about the Pixabay API and the `.env` configuration:

- [Pixabay API Documentation](https://pixabay.com/api/docs/)
- [Next.js .env Documentation](https://nextjs.org/docs/basic-features/environment-variables)

repository: mhstrkmp/unicorns

repo_name: mhstrkmp/unicorns


text:
# Changelog
All notable changes to this project will be documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [Unreleased]
### New Features
### Fixes

## [1.5.2] - 2021-03-05
### Fixes
* Fixes Issue [#399](https://github.com/newrelic/newrelic-dotnet-agent/issues/399): site extension did not clean up after installation ([#478](https://github.com/newrelic/newrelic-dotnet-agent/pull/478))

[Unreleased]: https://github.com/newrelic/newrelic-dotnet-agent/compare/AzureSiteExtension_v1.5.2...HEAD
[1.5.2]: https://github.com/newrelic/newrelic-dotnet-agent/compare/AzureSiteExtension_v1.5.1...AzureSiteExtension_v1.5.2

repository: JoshuaColeman/newrelic-dotnet-agent

repo_name: JoshuaColeman/newrelic-dotnet-agent


text:
# Type

## [Ontology](./ontology.md)

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.

A grouping based on shared characteristics; a class.

## [Axiology](./axiology.md)

### Relation to [Category Theory](category-theory.md)

The Type is a Category. An instantiation is a morphism. The Instance is the other category.

## [Epistemology](./epistemology.md)

### [Cultural](./culture.md) Definition

type (wiktionary)

> ### Noun

> A grouping based on shared characteristics; a class. "This type of plane can handle rough weather more easily than that type of plane."

> An individual considered typical of its class, one regarded as typifying a certain profession, environment, etc.

> An individual that represents the ideal for its class; an embodiment.

> (printing, countable) A letter or character used for printing, historically a cast or engraved block.

>     (uncountable) Such types collectively, or a set of type of one font or size.
>     (chiefly uncountable) Text printed with such type, or imitating its characteristics. "The headline was set in bold type."

> (biology) An individual considered representative of members of its taxonomic group. "the type of a genus, family, etc."

> Preferred sort of person; sort of person that one is attracted to.  "He was exactly her type."

> (biology) A blood group.

> (theology) An event or person that prefigures or foreshadows a later event - commonly an Old Testament event linked to Christian times.

> (computing theory) A tag attached to variables and values used in determining which kinds of value can be used in which situations; a data type.

> (fine arts) The original object, or class of objects, scene, face, or conception, which becomes the subject of a copy; especially, the design on the face of a medal or a coin.

> (chemistry) A simple compound, used as a mode or pattern to which other compounds are conveniently regarded as being related, and from which they may be actually or theoretically derived. "The fundamental types used to express the simplest and most essential chemical relations are hydrochloric acid, water, ammonia, and methane."

> (mathematics) A part of the partition of the object domain of a logical theory (which due to the existence of such partition, would be called a typed theory). (Note: this corresponds to the notion of "data type" in computing theory.) "Categorial grammar is like a combination of context-free grammar and types."

Type–token_distinction (Wikipedia)

> In disciplines such as logic, metalogic, typography, and computer programming, the type–token distinction is a distinction that separates a concept from the objects which are particular instances of the concept. For example, the sentence "the bicycle is in the garage" refers to a token of the type of thing known as "the bicycle", while the sentence "The bicycle has become more popular recently" refers to the type.

Type Theory (Wikipedia)

> In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.

> Type theory is closely related to (and in some cases overlaps with) type systems, which are a programming language feature used to reduce bugs. The types of type theory were created to avoid paradoxes in a variety of formal logics and rewrite systems and sometimes "type theory" is used to refer to this broader application.

### [Pattern](./pattern.md) Expression

Type is a pattern that is applicable across all [abstractions](./abstraction.md) in [Existence](./existence.md).

repository: btakita/philosophy

repo_name: btakita/philosophy


text:
# Vandalism-Detection
Application of SSD Tensorflow to detect probability density for person

![alt text](img/output1.jpg)
![alt text](img/output2.jpg)

Web service
![alt text](logs/outputweb.png)

the code for this micro web service is on demos/

we also deploy on live, www.huseinhouse.com/vandalism/

# This model only able to train vandalism applications, cannot improve SSD accuracy.

## Step to train
1. Unzip both positive.zip and negative.zip in current directory. You may delete the pictures inside it and add more
2. run the script
```bash
python train.py
```
but you may check the settings.py first if got memory error on your GPU
```python
picture_dimension = 128
learning_rate = 0.001
batch_size = 32
epoch = 15
```

## Step to test
1. Complete train above or simply download pretrained model from [here](https://drive.google.com/open?id=0BxQQlrLbdunWc1hQODJMazJyaVE), simply unzip in current directory
2. Download SSD pretrained model [here](https://drive.google.com/open?id=0B0qPCUZ-3YwWT1RCLVZNN3RTVEU), create directory called 'checkpoint_ssd' and put in there
3. run the script
```bash
python test_detect.py
```

## Step to deploy own server
1. Complete all above
2. check the code at the bottom of server.py
```python
if __name__ == '__main__':
	app.run(host = '<IP_ADDRESS>', threaded = True,  port = 8010)
```
3. If you want to do multi-threading for your server, install gunicorn, and simply,
```bash
sudo pip install gunicorn
sudo gunicorn -w (NUMBER_OF_WORKER) -b (BINDING_ADDRESS:PORT) -p gunicorn.pid (FLASK_PYNAME):app
# sudo gunicorn -w 4 -b <IP_ADDRESS>:8000 -p gunicorn.pid server:app
```

Model for our vandalism detection
![alt text](logs/graph.png)


text:
---
title: "The case of Persistent CAS"
date: 2019-11-02T12:18:02-07:00
draft: true
---

There are numerous paper talking about persistent memory data structures, some of them claimed excellent performance, others support (near) instant recovery.
But some most important problems are remain unsolved, and even publicly misunderstood, for example, how to do persistent CAS correctly.

Persistent CAS is the most important primitive in building concurrent and crash-consistent data structures.
In this post, I'll cover the correct ways to build persistent CAS, and report their performance number under different contention level.

##### CAS operation

Compare and swap, will try to assign `new_v` to `addr` if `*addr == old_v`, namely, CAS.
```c++
CAS(addr, old_v, new_v);
```

In later sections, I will call this method `naive CAS`. Obvisouly `naive CAS` is not crash consistent,
because a crash can happen before the new value is evicted from cache (flushed to memory).

##### Persistent CAS (FAKE)

A lot of hand wired persistent memory data structures [^1] simply assumes "flushes around CAS" is correct:
```c++
flush();
fence();

CAS(addr, old_v, new_v);

flush(addr);
fence();
```

This assumption is incorrect, as I pointed out in a the previous [post](/posts/crash-consistency).
In later sections, I will call this method `CAS`.

##### CAS with dirty bit
This approach is proposed by [PMwCAS](https://github.com/microsoft/pmwcas), the idea is simple:
```c++
kDirtyMask = 0x8000_0000_0000_0000;

while (old_v is dirty) {
    CAS(target, old_v, old_v & (~kDirtyBitMask));
    old_v = load(addr);
}

new_v_dirty = new_v | kDirtyMask;

CAS(addr, old_v, new_v_dirty);
flush();
fence();
CAS(addr, new_v_dirty, new_v);
```

I named this method as `DirtyCAS`, while `DirtyCAS` is techniqually correct, it has some caveats:

1. It requires readers to clear the dirty bit, which might degrade the reading performance (by issuing extra `store` and polluting the pipeline).
2. It steals highest bit of the `new_v`, which can be a problem when storing non-pointer values.

##### CAS with logging
The idea is to record the CAS operations before executing them, on recovery, the not flushed CAS will be roll forwarded. A possible implementation can be found [here](https://github.com/XiangpengHao/epoch-reclaimer/blob/master/pcas.h), I call it `PCAS`:

```c++
log(addr, old_v, new_v);
CAS(addr, old_v, new_v);
```

It addresses the issues introduced by `DirtyCAS`, but have a important drawback: it  requires twice more writes than `DirtyCAS` and also issues twice the `flush()`.
The new problem is more severe especially when clwb, a.k.a `flush()`, is [not properly implemented](/posts/is-clwb-implemented).

### Benchmark
Here comes the most boring part, in an ideal world, I would hire someone to do benchmark for me.

All the experiments are performed on [this machine](/posts/new-server).
In each experiment, each thread is asked to perform 10k CAS operations on a `uint64_t` array, the array has 1k items, and each item is padded to the cache line size.

```
| uint64 ---------- | uint64 ---------- | ... 996 items | uint64 ---------- | uint64 ---------- |
  item 0, 56 bytes    item 1, 56 bytes
```
I did not do the experiment of `pure read`, because it is not a well defined scenario.

Feel free to interpret the results, here are some of mine:

1. The cost of persistency is extremely high, because it effectively bypassed the CPU cache.

2. The performance gap becomes smaller when contention goes high, because cache coherence cost dominates the time (?).

3. The `DirtyCAS` consistently has slight better performance than `PCAS`, but I believe on read-mostly workload, `PCAS` should be way better (follow up needed!).

![](/img/cas-exe.png)

![](/img/cas-suc.png)

![](/img/succ-rate.png)

##### Raw data
| exec/s/t | 1           | 2           | 4           | 8           | 16          | 24          |
|--------------|-------------|-------------|-------------|-------------|-------------|-------------|
| PCAS         | 957643.431  |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |
| DirtyCAS     | 1224292.91  |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> | 263886.36   |
| CAS          | 1928945.368 | 1608399.707 | 1301671.476 |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |
| NaiveCAS     | 17387040.74 | 5283932.091 | 2794045.331 | 1462033.191 |<PHONE_NUMBER> |<PHONE_NUMBER> |

| succ/s/t | 1           | 2           | 4           | 8           | 16          | 24          |
|--------------|-------------|-------------|-------------|-------------|-------------|-------------|
| PCAS         | 957643.431  |<PHONE_NUMBER> | 467367.648  |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |
| DirtyCAS     | 1224292.91  |<PHONE_NUMBER> | 658485.055  |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |
| CAS          | 1928945.368 | 1608319.287 | 1293015.361 |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |
| NaiveCAS     | 17387040.74 | 4839236.366 | 2041385.399 |<PHONE_NUMBER> |<PHONE_NUMBER> |<PHONE_NUMBER> |

### Closing words

Supporting persistency will slow down the performance, how much slow-down can you afford?

What if I don't care crash-consistency, what trade-off can I made?

What if I don't care **strict** crash-consistency, what trade-off can I made?

[^1]:  RECIPE, CCEH etc.


text:
#
 - libstarlight -

###
 3DS Homebrew Application Framework
---
(Pardon the dust, both the library and this readme are still a work in progress)

## What is this?
libstarlight is a fully-featured application framework for 3DS homebrew written in C++14.

Features include:
* Fully themable UI framework with rich widgets designed for the 3DS's touchscreen
* Underlying graphics framework built on citro3d, using premultiplied alpha blending

 (textures automatically converted on load)
* Streamlined, easy-to-use onscreen keyboard
* Centralized configuration system for application-specific settings and storage, complete with optional auto-saving on exit
* Filesystem helpers to streamline working with SD and romfs contents
* Various basic datatypes for convenience and interoperability

Please keep in mind that while libstarlight is still in beta (pre-1.0.0) not everything is final. Expect occasional (usually minor) breaking changes as things settle.

## Requirements
libstarlight requires devkitARM r46 or later, along with:
* reasonably up-to-date libctru
* citro3d

Additionally, libstarlight contains versions of the following bundled within:
* [lodepng](https://github.com/lvandeve/lodepng)
* [nlohmann::json (JSON For Modern C++)](https://github.com/nlohmann/json)

## Okay, so how do I use this?
(section WIP, take a look at the testbed for a slightly scattered example)

To ensure your application runs properly without themes installed to the SD card, it is recommended to include a copy of the default theme (or any theme with no fallback) at `romfs:/.fallback_theme/`.

(Themes on SD go in `sdmc:/.starlight/themes/`)

## License
* MIT (see [license.md](license.md))

Bundled dependencies (see [\_incLib](libstarlight/source/starlight/_incLib)) have their own terms and/or notices, as listed in their respective files.

repository: mothie/libstarlight

repo_name: mothie/libstarlight