Skip to content

Instantly share code, notes, and snippets.

View ranjitjhala's full-sized avatar

Ranjit Jhala ranjitjhala

227 followers · 2 following
View GitHub Profile
@ranjitjhala
ranjitjhala / fresh_macros.tex
Last active January 31, 2023 19:08
Fresh Calculus Macros
\newcommand{\rnk}{\rho}
\newcommand{\rr}{\mathcal{R}}
\newcommand{\rord}{\mathcal{O}}
\newcommand{\runi}{{\mathcal{U}}}
\newcommand{\rapp}{{\mathcal{A}}}
\newcommand{\rcon}{{\mathcal{C}}}
\newcommand{\rgc}{{\mathcal{G}}}
\newcommand{\rfail}{{\mathcal{F}}}
\newcommand{\rspc}{{\mathcal{S}}}
@ranjitjhala
ranjitjhala / lh-crash.log
Created November 11, 2020 00:14
LH Server Crash
[client] run command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp"
[client] debug command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp"
[client] server cwd: undefined
haskell-language-server version: 0.5.1.0 (GHC: 8.10.2) (PATH: /Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2) (GIT hash: e3fe0e7546aa91e44cc56cfe8ec078a026cf533a)
Starting (haskell-language-server)LSP server...
with arguments: LspArguments {argLSP = True, argsCwd = Nothing, argFiles = [], argsShakeProfiling = Nothing, argsTesting = False, argsExamplePlugin = False, argsDebugOn = False, argsLogFile = Nothing, argsThreads = 0, argsProjectGhcVersion = False}
with plugins: [PluginId "brittany",PluginId "eval",PluginId "floskell",PluginId "fourmolu",PluginId "ghcide",PluginId "importLens",Plugi
@ranjitjhala
ranjitjhala / lh-crash.log
Created November 10, 2020 19:32
LH server crash
[client] run command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp"
[client] debug command: "/Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2 --lsp"
[client] server cwd: undefined
haskell-language-server version: 0.5.1.0 (GHC: 8.10.2) (PATH: /Users/rjhala/Library/Application Support/Code/User/globalStorage/haskell.haskell/haskell-language-server-0.5.1-darwin-8.10.2) (GIT hash: e3fe0e7546aa91e44cc56cfe8ec078a026cf533a)
Starting (haskell-language-server)LSP server...
with arguments: LspArguments {argLSP = True, argsCwd = Nothing, argFiles = [], argsShakeProfiling = Nothing, argsTesting = False, argsExamplePlugin = False, argsDebugOn = False, argsLogFile = Nothing, argsThreads = 0, argsProjectGhcVersion = False}
with plugins: [PluginId "brittany",PluginId "eval",PluginId "floskell",PluginId "fourmolu",PluginId "ghcide",PluginId "importLens",Plugi
@ranjitjhala
ranjitjhala / ple.rkt
Last active July 30, 2020 23:11
PLE formula for `foo 3 == 0`
(assert
(and (and (= (= (- (- 3 1) 1) 7) false)
(= (= (- 3 1) 4) false)
(=
(ite
(= (- (- (- 3 1) 1) 1) 3)
(foo (- (- (- (- 3 1) 1) 1) 1))
(ite
(= (- (- (- 3 1) 1) 1) 2)
(foo (- (- (- (- 3 1) 1) 1) 1))
@ranjitjhala
ranjitjhala / FingSimple.hs
Last active January 18, 2019 18:12
Finger Tree - Liquid Haskell
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--no-adt" @-}
{- LIQUID "--diff" @-}
{-@ LIQUID "--ple" @-}
module FingerTree where
import Language.Haskell.Liquid.ProofCombinators
@ranjitjhala
ranjitjhala / inductive.md
Last active November 7, 2015 00:53
Making Invariants Inductive
@ranjitjhala
ranjitjhala / atom-typescript error
Created September 18, 2015 02:24
0 info it worked if it ends with ok
1 verbose cli [ '/Applications/Atom.app/Contents/Resources/app/apm/bin/node',
1 verbose cli '/Applications/Atom.app/Contents/Resources/app/apm/node_modules/npm/bin/npm-cli.js',
1 verbose cli '--globalconfig',
1 verbose cli '/Users/rjhala/.atom/.apm/.apmrc',
1 verbose cli '--userconfig',
1 verbose cli '/Users/rjhala/.atom/.apmrc',
1 verbose cli 'rebuild',
1 verbose cli '--target=0.30.6',
1 verbose cli '--arch=x64' ]
@ranjitjhala
ranjitjhala / shrink-lncs.sh
Last active September 10, 2015 14:15
#!/bin/bash
pdfcrop --margins "5 10 5 20" --clip $1 crop.pdf
pdfnup --nup 2x1 crop.pdf
mv crop-nup.pdf $1
rm crop.pdf
@ranjitjhala
ranjitjhala / FizzBuzz.hs
Created March 23, 2015 17:50
Fizz-Buzz in LiquidHaskell
// Run at: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1427132944.hs
module FizzBuzz where
---------------------------------------------------------------
-- | Implementation: Top level
---------------------------------------------------------------
main :: IO ()
main = mapM_ (putStrLn . say) (take 100 $ nums 0)
@ranjitjhala
ranjitjhala / gist:171aa922204aa84c7b3d
Last active August 29, 2015 14:13 — forked from mpickering/gist:f1718fcdc4c56273ed52
{-# LANGUAGE ViewPatterns #-}
module InTex where
import Text.Pandoc.JSON
import Text.Pandoc
import Data.List
main :: IO ()
main = toJSONFilter readFootnotes