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

Vim + EditorConfig Setup

mkdir -p ~/tmp
cd ~/tmp
mv editorconfig-vim-master/{autoload,doc,plugin} ~/.vim/

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 /
Created Dec 17, 2015
#!/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
\usepackage{unixode} % Need to download from
\usepackage{minted} % Need to download from
% Specify local pygments directory. Do the following in your working directory (where test.tex is located)
% hg clone && cd pygments-main && python build & cd ..
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=
// Originally written by Kyungmin Bae (
soonhokong /
Created Oct 22, 2015 — forked from ggreer/
My ag benchmark script
function benchmark_rev() {
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



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

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


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.


  1. CAPD4 gives a very good approximation [0.999, 1.0] when we integrate the function from x = -10 to x = 10.
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== 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
You can’t perform that action at this time.