Skip to content

Instantly share code, notes, and snippets.

Soonho Kong soonhokong

Block or report user

Report or block soonhokong

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 Vim_EditorConfig.md

Vim + EditorConfig Setup

mkdir -p ~/tmp
cd ~/tmp
wget https://github.com/editorconfig/editorconfig-vim/archive/master.zip
unzip master.zip
mv editorconfig-vim-master/{autoload,doc,plugin} ~/.vim/
View loop_vectorize.md

Clang Version

Debian clang version 3.3-debian16precise1 (branches/release_33) (based on LLVM 3.3)
Target: x86_64-pc-linux-gnu
Thread model: posix

Code (test.cpp)

@soonhokong
soonhokong / leandeps.py
Created Dec 17, 2015
Python3-compatible leandeps.py
View leandeps.py
#!/usr/bin/env python
# -*- coding: utf-8 -*-
#
# Copyright (c) 2015 Microsoft Corporation. All rights reserved.
# Released under Apache 2.0 license as described in the file LICENSE.
#
# Authors: Soonho Kong, Leonardo de Moura, Ulrik Buchholtz
# Python 2/3 compatibility
from __future__ import print_function
View test.tex
\documentclass{article}
\usepackage{unixode} % Need to download from https://raw.githubusercontent.com/leanprover/tutorial/master/unixode.sty
\usepackage{minted} % Need to download from https://raw.githubusercontent.com/leanprover/tutorial/master/minted.sty
% Specify local pygments directory. Do the following in your working directory (where test.tex is located)
% hg clone https://bitbucket.org/leanprover/pygments-main && cd pygments-main && python setup.py build & cd ..
\renewcommand{\MintedPygmentize}{./pygments-main/pygmentize}
\setminted{encoding=utf-8}
\usepackage{fontspec}
\setmainfont{FreeSerif}
\setmonofont{FreeMono}
@soonhokong
soonhokong / powertrain.drh
Created Dec 7, 2015
Toyota Powertrain Control Benchmark
View powertrain.drh
// Toyota Powertrain Control Verification Benchmark:
// This is based on the following paper:
//
// Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and
// Ken Butts. 2014. Powertrain control verification benchmark. In
// Proceedings of the 17th international conference on Hybrid systems:
// computation and control (HSCC '14). ACM, New York, NY, USA,
// 253-262. DOI=http://dx.doi.org/10.1145/2562059.2562140
//
// Originally written by Kyungmin Bae (kbae@cs.cmu.edu)
@soonhokong
soonhokong / ag_bench.sh
Created Oct 22, 2015 — forked from ggreer/ag_bench.sh
My ag benchmark script
View ag_bench.sh
#!/bin/bash
function benchmark_rev() {
REV=$1
git clean -f &> /dev/null
git checkout $REV &> /dev/null
git clean -f &> /dev/null
if [ $? -ne 0 ]; then
echo "Checkout of $REV failed!"
exit 1
View lean_virtual_memory_exhausted.txt
[ 51%] [ 51%] [ 51%] [ 51%] cd /root/lean/build/library/tactic && /usr/bin/c++ -Wall -Wextra -std=c++11 -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build -o CMakeFiles/tactic.dir/contradiction_tactic.cpp.o -c /root/lean/src/library/tactic/contradiction_tactic.cpp
Building CXX object kernel/CMakeFiles/kernel.dir/equiv_manager.cpp.o
cd /root/lean/build/kernel && /usr/bin/c++ -Wall -Wextra -std=c++11 -D LEAN_MULTI_THREAD -D LEAN_CACHE_EXPRS -DLEAN_BUILD_TYPE="Release" -fPIC -D LEAN_TRACK_MEMORY -I /usr/include -D HAS_MALLOC_USABLE_SIZE -I /usr/include/lua5.2 -D LEAN_USE_LUA_NEWSTATE -O3 -DNDEBUG -I/usr/include/x86_64-linux-gnu -I/root/lean/src -I/root/lean/build -o CMakeFiles/kernel.dir/equiv_manager.cpp.o -c /root/lean/src/kernel/equiv_manager.cpp
/usr/bin/cmake -E cmake_progress_repo
View README.md

Ubuntu

OSX

cmake -DCMAKE_CXX_COMPILER=ccache-clang++ \
      -DCMAKE_C_COMPILER=ccache-clang \
@soonhokong
soonhokong / time_step_control.md
Last active Aug 29, 2015
CAPD time step control
View time_step_control.md

We want to integrate the probability density function for normal distribution:

image1

To simplify the problem, let's pick mean = 0.0, standard deviation = 1.0. In theory, integration of this fuction from x = -oo to x = oo should give P = 1.0.

image2

  1. CAPD4 gives a very good approximation [0.999, 1.0] when we integrate the function from x = -10 to x = 10.
@soonhokong
soonhokong / valgrind trace for segfault
Created Apr 23, 2015
valgrind trace for segfault
View valgrind trace for segfault
==22321== Memcheck, a memory error detector
==22321== Copyright (C) 2002-2012, and GNU GPL'd, by Julian Seward et al.
==22321== Using Valgrind-3.8.1 and LibVEX; rerun with -h for copyright info
==22321== Command: /usr0/home/soonhok/work/lean/bin/lean /usr0/home/soonhok/work/lean/hott/init/datatypes.hlean
==22321==
==22321== Syscall param set_robust_list(head) points to uninitialised byte(s)
==22321== at 0x82F8B1: __pthread_initialize_minimal (nptl-init.c:359)
==22321== by 0x8340B0: (below main) (in /usr0/home/soonhok/work/lean/bin/lean)
==22321== Address 0x4001630 is not stack'd, malloc'd or (recently) free'd
==22321==
You can’t perform that action at this time.