Skip to content

Instantly share code, notes, and snippets.


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