Skip to content

Instantly share code, notes, and snippets.

Nickolay Kudasov fizruk

Block or report user

Report or block fizruk

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View isaprop_isaprop.v
Require Export UniMath.Foundations.Propositions.
(* A simpler definition of proposition. *)
Definition isaprop' (X : UU) : UU := ∏ (x y : X), x = y.
(* Simpler definition implies standard isaprop. *)
Definition isaprop'_to_isaprop {X : UU} :
isaprop' X → isaprop X.
Proof.
intros f x y.
View servant-token-bearer.hs
#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-server])"
-- =======================================================================
--
-- If you have have Nix installed — just run this script as an executable:
--
-- $ ./servant-token-bearer.hs
-- Starting server at http://localhost:8088
--
-- You can then check that everything works using cURL:
@fizruk
fizruk / replace-sub-api.hs
Last active Aug 9, 2018
Replace sub api to change implementation for an endpoint handler to a more efficient one.
View replace-sub-api.hs
#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-swagger servant-swagger-ui])"
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
@fizruk
fizruk / servant-overrided-as.hs
Last active Aug 9, 2018
OverridableAs combinator to enable efficient implementations for some Servant endpoints after the fact.
View servant-overrided-as.hs
#! /usr/bin/env nix-shell
#! nix-shell -i runghc -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [servant-swagger servant-swagger-ui])"
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
View stack-ghcjs-docker.yaml
resolver: lts-6.20
compiler: ghcjs-0.2.0.9006020_ghc-7.10.3
compiler-check: match-exact
packages:
- '.'
# where to get GHCJS from (you don't need it when using Docker)
setup-info:
ghcjs:
@fizruk
fizruk / config.yml
Created Mar 26, 2018
Circle CI 2.0 config for a Haskell Stack project (for LTS 11.0).
View config.yml
version: 2
jobs:
build:
docker:
- image: fpco/stack-build:lts-11.0
steps:
- checkout
- restore_cache:
@fizruk
fizruk / README.md
Last active Nov 21, 2017
Run GHCJSi for a project with static files.
View README.md
  1. Put irunner.js into your repository at ghcjs/lib/etc/irunner.js.
  2. Put static content (CSS, images, etc.) for executable at <executable name>/static.
  3. Put ghcjsiClient.html to <executable name>/static and add any headers you want.
  4. Run run.sh <package name> <executable name>.

Caveats

npm packages

In order for everything to work you need to install a few packages via npm.

@fizruk
fizruk / HasServerVerb.hs
Created May 15, 2017
Verb with multiple methods.
View HasServerVerb.hs
class AllReflectMethod methods where
reflectMethods :: Proxy methods -> [Method]
instance AllReflectMethod '[] where
reflectMethods _ = []
instance (ReflectMethod m, AllReflectMethod ms) => AllReflectMethod (m:ms) where
reflectMethods _ = reflectMethod (Proxy @m) : reflectMethods (Proxy @ms)
instance OVERLAPPING_
View servant-swagger-description.hs
data Description (sym :: Symbol)
instance (KnownSymbol sym, HasSwagger api) => HasSwagger (Description sym :> api) where
toSwagger _ = toSwagger (Proxy :: Proxy api)
& allOperations.description ?~ desc
where
desc = symbolVal (Proxy :: Proxy sym)
View ToSchemaEither.hs
{-# LANGUAGE ScopedTypeVariables #-}
import Control.Lens
import Data.Typeable
import qualified Data.Text as Text
instance {-# OVERLAPPING #-} (Typeable a, ToSchema a) => ToSchema (Either WalletError a) where
declareNamedSchema proxy = genericDeclareNamedSchema defaultSchemaOptions proxy
& mapped.name ?~ Text.pack ("Either WalletError " ++ show (typeOf (undefined :: a)))
You can’t perform that action at this time.